# HG changeset patch
# User dixon
# Date 1174059649 -3600
# Node ID e4fd2d02391de171f7839dbaa31dfae9eb34562f
# Parent  fb80fedd192d9d5d638258455ad8aa452150394d
removed safe elim flag of trueElim and notFalseElim for testing.

diff -r fb80fedd192d -r e4fd2d02391d src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Mar 16 16:37:52 2007 +0100
+++ b/src/HOL/HOL.thy	Fri Mar 16 16:40:49 2007 +0100
@@ -728,7 +728,7 @@
 lemma TrueE: "True ==> P ==> P" .
 lemma notFalseE: "~ False ==> P ==> P" .
 
-lemmas [Pure.elim!] = disjE iffE FalseE conjE exE TrueE notFalseE
+lemmas [Pure.elim!] = disjE iffE FalseE conjE exE 
   and [Pure.intro!] = iffI conjI impI TrueI notI allI refl
   and [Pure.elim 2] = allE notE' impE'
   and [Pure.intro] = exI disjI2 disjI1