diff -r e2b876cd9e29 -r 89d2758ecddf src/FOL/FOL.thy
--- 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