TrueElim and notTrueElim tested and added as safe elim rules.
--- 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