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 