# HG changeset patch
# User berghofe
# Date 999268158 -7200
# Node ID 0494d0347f18d57fe48eac64ec24a81364d5129d
# Parent  0c0d2332e8f0fc868ce63e5c7771a4f3a3eceebb
Proof of True_implies_equals is stored with "open" derivation to
facilitate simplification of proof terms.

diff -r 0c0d2332e8f0 -r 0494d0347f18 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Fri Aug 31 16:28:26 2001 +0200
+++ b/src/HOL/simpdata.ML	Fri Aug 31 16:29:18 2001 +0200
@@ -105,11 +105,11 @@
 
 (* Elimination of True from asumptions: *)
 
-val True_implies_equals = prove_goal (the_context ())
- "(True ==> PROP P) == PROP P"
-(fn _ => [rtac equal_intr_rule 1, atac 2,
-          METAHYPS (fn prems => resolve_tac prems 1) 1,
-          rtac TrueI 1]);
+local fun rd s = read_cterm (sign_of (the_context())) (s, propT);
+in val True_implies_equals = standard' (equal_intr
+  (implies_intr_hyps (implies_elim (assume (rd "True ==> PROP P")) TrueI))
+  (implies_intr_hyps (implies_intr (rd "True") (assume (rd "PROP P")))));
+end;
 
 fun prove nm thm  = qed_goal nm (the_context ()) thm (fn _ => [(Blast_tac 1)]);