# HG changeset patch
# User wenzelm
# Date 1006539658 -3600
# Node ID 75103ba03035e590929ed9abd0ed5407c1b2ae0f
# Parent  2b28d7dd91f5bfda119900fe01d1c595facbf03c
tuned;

diff -r 2b28d7dd91f5 -r 75103ba03035 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Fri Nov 23 19:20:06 2001 +0100
+++ b/src/HOL/simpdata.ML	Fri Nov 23 19:20:58 2001 +0100
@@ -20,30 +20,6 @@
 
 fun prover s = prove_goal (the_context ()) s (fn _ => [(Blast_tac 1)]);
 
-(*Make meta-equalities.  The operator below is Trueprop*)
-
-fun mk_meta_eq r = r RS eq_reflection;
-fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r;
-
-bind_thm ("Eq_TrueI", mk_meta_eq (prover  "P --> (P = True)"  RS mp));
-bind_thm ("Eq_FalseI", mk_meta_eq(prover "~P --> (P = False)" RS mp));
-
-fun mk_eq th = case concl_of th of
-        Const("==",_)$_$_       => th
-    |   _$(Const("op =",_)$_$_) => mk_meta_eq th
-    |   _$(Const("Not",_)$_)    => th RS Eq_FalseI
-    |   _                       => th RS Eq_TrueI;
-(* last 2 lines requires all formulae to be of the from Trueprop(.) *)
-
-fun mk_eq_True r =
-  Some (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => None;
-
-(*Congruence rules for = (instead of ==)*)
-fun mk_meta_cong rl =
-  standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
-  handle THM _ =>
-  error("Premises and conclusion of congruence rules must be =-equalities");
-
 bind_thm ("not_not", prover "(~ ~ P) = P");
 
 bind_thms ("simp_thms", [not_not] @ map prover
@@ -94,14 +70,6 @@
   "(ALL x. P --> Q x) = (P --> (ALL x. Q x))"]);
 
 
-(* Elimination of True from asumptions: *)
-
-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)]);
 
 prove "eq_commute" "(a=b) = (b=a)";
@@ -291,6 +259,39 @@
 
 (*** Case splitting ***)
 
+(*Make meta-equalities.  The operator below is Trueprop*)
+
+fun mk_meta_eq r = r RS eq_reflection;
+fun safe_mk_meta_eq r = mk_meta_eq r handle Thm.THM _ => r;
+
+bind_thm ("Eq_TrueI", mk_meta_eq (prover  "P --> (P = True)"  RS mp));
+bind_thm ("Eq_FalseI", mk_meta_eq(prover "~P --> (P = False)" RS mp));
+
+fun mk_eq th = case concl_of th of
+        Const("==",_)$_$_       => th
+    |   _$(Const("op =",_)$_$_) => mk_meta_eq th
+    |   _$(Const("Not",_)$_)    => th RS Eq_FalseI
+    |   _                       => th RS Eq_TrueI;
+(* last 2 lines requires all formulae to be of the from Trueprop(.) *)
+
+fun mk_eq_True r =
+  Some (r RS meta_eq_to_obj_eq RS Eq_TrueI) handle Thm.THM _ => None;
+
+(*Congruence rules for = (instead of ==)*)
+fun mk_meta_cong rl =
+  standard(mk_meta_eq(replicate (nprems_of rl) meta_eq_to_obj_eq MRS rl))
+  handle THM _ =>
+  error("Premises and conclusion of congruence rules must be =-equalities");
+
+(* Elimination of True from asumptions: *)
+
+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;
+
+
 structure SplitterData =
   struct
   structure Simplifier = Simplifier