# HG changeset patch
# User dixon
# Date 1174059472 -3600
# Node ID fb80fedd192d9d5d638258455ad8aa452150394d
# Parent  346729a55460113102e82a248507364be1091c2d
added safe intro rules for removing "True" subgoals as well as "~ False" ones.

diff -r 346729a55460 -r fb80fedd192d src/HOL/HOL.thy
--- 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