--- a/src/FOL/FOL.thy Thu Jul 27 13:42:59 2006 +0200
+++ b/src/FOL/FOL.thy Thu Jul 27 13:43:00 2006 +0200
@@ -34,9 +34,17 @@
lemma ex1_functional: "[| EX! z. P(a,z); P(a,b); P(a,c) |] ==> b = c"
by blast
-ML {*
-val ex1_functional = thm "ex1_functional";
-*}
+ML {* val ex1_functional = thm "ex1_functional" *}
+
+(* Elimination of True from asumptions: *)
+lemma True_implies_equals: "(True ==> PROP P) == PROP P"
+proof
+ assume "True \<Longrightarrow> PROP P"
+ from this and TrueI show "PROP P" .
+next
+ assume "PROP P"
+ then show "PROP P" .
+qed
use "simpdata.ML"
setup simpsetup