# HG changeset patch
# User dixon
# Date 1174179005 -3600
# Node ID c9357ef0116837e3b3f3eda5f08fed8fab6dc8f6
# Parent  4f2f48b1bad4adbea1065cc7365c1577a62ed58e
TrueElim and notTrueElim tested and added as safe elim rules.

diff -r 4f2f48b1bad4 -r c9357ef01168 src/HOL/HOL.thy
--- 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