# HG changeset patch
# User nipkow
# Date 873212522 -7200
# Node ID ebad042c0bba26dc120e98a8d993e9430b65616e
# Parent  6d5b3d5ff1325ae0e8cc72bb3e8964f8d851a32a
Added True_implies_equals

diff -r 6d5b3d5ff132 -r ebad042c0bba src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Tue Sep 02 16:10:26 1997 +0200
+++ b/src/HOL/simpdata.ML	Tue Sep 02 17:02:02 1997 +0200
@@ -199,6 +199,14 @@
 
 end;
 
+(* Elimination of True from asumptions: *)
+
+val True_implies_equals = prove_goal HOL.thy
+ "(True ==> PROP P) == PROP P"
+(fn _ => [rtac equal_intr_rule 1, atac 2,
+          METAHYPS (fn prems => resolve_tac prems 1) 1,
+          rtac TrueI 1]);
+
 fun prove nm thm  = qed_goal nm HOL.thy thm (fn _ => [blast_tac HOL_cs 1]);
 
 prove "conj_commute" "(P&Q) = (Q&P)";
@@ -355,6 +363,7 @@
 val HOL_ss = 
     HOL_basic_ss addsimps 
      ([triv_forall_equality, (* prunes params *)
+       True_implies_equals, (* prune asms `True' *)
        if_True, if_False, if_cancel,
        o_apply, imp_disjL, conj_assoc, disj_assoc,
        de_Morgan_conj, de_Morgan_disj, not_imp,