# IRC log for #isabelle, 2014-04-16

All times shown according to UTC.

Time Nick Message
01:26 ezyang joined #isabelle
01:27 ezyang I'm reading some Isabelle code which makes liberal use of things like \<Gamma>. Is there some reading mode which converts these into the Unicode?
01:32 ezyang Unicode tokens, apparently.
01:42 Jafet isabelle jedit?
01:45 Jafet proofgeneral doesn't convert to unicode, but for visual purposes it also displays symbols
01:47 ilbot3 joined #isabelle
01:47 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
01:49 ezyang I have some lemma lemmaname [rule_format] : "some expression" "another expression"
01:49 ezyang what does it mean if there are multiple quoted string things?
01:53 Jafet applybot: lemma "True" "False" "P ==> P"
01:53 applybot *** Unrecognized command
01:53 Jafet Hmm, I need to fix the grammar
01:53 Jafet Each string is one theorem.
01:54 ezyang so, are they proving multiple theorems at once?
01:54 Jafet Multiple theorems, then each one is transformed with rule_format and then all stored with one name.
01:55 ezyang ah, and isabelle is able to automatically select the "right one"?
01:55 Jafet It is just treated as a list of theorems
01:55 ezyang ok.
01:57 Jafet applybot: thm HOL.all_simps -- extreme example
01:57 applybot (∀x. ?P x ∧ ?Q) = ((∀x. ?P x) ∧ ?Q)  \  (∀x. ?P ∧ ?Q x) = (?P ∧ (∀x. ?Q x))  \  (∀x. ?P x ∨ ?Q) = ((∀x. ?P x) ∨ ?Q)  \  (∀x. ?P ∨ ?Q x) = (?P ∨ (∀x. ?Q x))  \  (∀x. ?P x ⟶ ?Q) = ((∃x. ?P x) ⟶ ?Q)  \  (∀x. ?P ⟶ ?Q x) = (?P ⟶ (∀x. ?Q x))
17:36 tpsinnem joined #isabelle
19:46 tpsinnem joined #isabelle
20:08 wignode joined #isabelle
20:37 leonweber joined #isabelle