Time Nick Message
01:27 ezyang I'm reading some Isabelle code which makes liberal use of things like \. 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: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))