# HG changeset patch
# User paulson
# Date 938084791 -7200
# Node ID 5be4bb8e4e3ff0b58f2e3c620c9bdbb97b63cfc8
# Parent  d1b40e0464b12b2a9b702c7d6bfad14baaf172fe
tidied; added lemma restrict_to_left

diff -r d1b40e0464b1 -r 5be4bb8e4e3f src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu Sep 23 09:05:44 1999 +0200
+++ b/src/HOL/simpdata.ML	Thu Sep 23 13:06:31 1999 +0200
@@ -480,12 +480,11 @@
 by (simp_tac (HOL_ss setloop (split_tac [split_if])) 1);
 qed "if_distrib";
 
-
 (*For expand_case_tac*)
-val prems = goal (the_context ()) "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
+val prems = Goal "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)";
 by (case_tac "P" 1);
 by (ALLGOALS (asm_simp_tac (HOL_ss addsimps prems)));
-val expand_case = result();
+qed "expand_case";
 
 (*Used in Auth proofs.  Typically P contains Vars that become instantiated
   during unification.*)
@@ -494,9 +493,16 @@
     Simp_tac (i+1) THEN 
     Simp_tac i;
 
+(*This lemma restricts the effect of the rewrite rule u=v to the left-hand
+  side of an equality.  Used in {Integ,Real}/simproc.ML*)
+Goal "x=y ==> (x=z) = (y=z)";
+by (asm_simp_tac HOL_ss 1);
+qed "restrict_to_left";
 
 (* default simpset *)
-val simpsetup = [fn thy => (simpset_ref_of thy := HOL_ss addcongs [if_weak_cong]; thy)];
+val simpsetup = 
+    [fn thy => (simpset_ref_of thy := HOL_ss addcongs [if_weak_cong]; 
+		thy)];
 
 
 (*** integration of simplifier with classical reasoner ***)