Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/HOL.thy
changeset 22467 c9357ef01168
parent 22445 e4fd2d02391d
child 22473 753123c89d72 
--- a/src/HOL/HOL.thy	Fri Mar 16 21:35:30 2007 +0100
+++ b/src/HOL/HOL.thy	Sun Mar 18 01:50:05 2007 +0100
@@ -728,7 +728,7 @@
 lemma TrueE: "True ==> P ==> P" .
 lemma notFalseE: "~ False ==> P ==> P" .
 
-lemmas [Pure.elim!] = disjE iffE FalseE conjE exE 
+lemmas [Pure.elim!] = disjE iffE FalseE conjE exE TrueE notFalseE
   and [Pure.intro!] = iffI conjI impI TrueI notI allI refl
   and [Pure.elim 2] = allE notE' impE'
   and [Pure.intro] = exI disjI2 disjI1
isabelle