changeset 22444 | fb80fedd192d |
parent 22377 | 61610b1beedf |
child 22445 | e4fd2d02391d |
--- a/src/HOL/HOL.thy Wed Mar 14 21:52:26 2007 +0100 +++ b/src/HOL/HOL.thy Fri Mar 16 16:37:52 2007 +0100 @@ -725,7 +725,10 @@ with 1 show R by (rule notE) qed -lemmas [Pure.elim!] = disjE iffE FalseE conjE exE +lemma TrueE: "True ==> P ==> P" . +lemma notFalseE: "~ False ==> P ==> P" . + +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