# HG changeset patch
# User paulson
# Date 938084845 -7200
# Node ID dca904d4ce4c387763e3257b801db644218fd86d
# Parent  5be4bb8e4e3ff0b58f2e3c620c9bdbb97b63cfc8
Sets new component "restrict_to_left"

diff -r 5be4bb8e4e3f -r dca904d4ce4c src/HOL/Integ/simproc.ML
--- a/src/HOL/Integ/simproc.ML	Thu Sep 23 13:06:31 1999 +0200
+++ b/src/HOL/Integ/simproc.ML	Thu Sep 23 13:07:25 1999 +0200
@@ -7,22 +7,24 @@
 *)
 
 
-(*** Two lemmas needed for the simprocs ***)
+(*** Lemmas needed for the simprocs ***)
 
 (*Deletion of other terms in the formula, seeking the -x at the front of z*)
-val zadd_cancel_21 = prove_goal IntDef.thy
-    "((x::int) + (y + z) = y + u) = ((x + z) = u)"
-  (fn _ => [stac zadd_left_commute 1,
-	    rtac zadd_left_cancel 1]);
+Goal "((x::int) + (y + z) = y + u) = ((x + z) = u)";
+by (stac zadd_left_commute 1);
+by (rtac zadd_left_cancel 1);
+qed "zadd_cancel_21";
 
 (*A further rule to deal with the case that
   everything gets cancelled on the right.*)
-val zadd_cancel_end = prove_goal IntDef.thy
-    "((x::int) + (y + z) = y) = (x = -z)"
-  (fn _ => [stac zadd_left_commute 1,
-	    res_inst_tac [("t", "y")] (zadd_int0_right RS subst) 1,
-	    stac zadd_left_cancel 1,
-	    simp_tac (simpset() addsimps [eq_zdiff_eq RS sym]) 1]);
+Goal "((x::int) + (y + z) = y) = (x = -z)";
+by (stac zadd_left_commute 1);
+by (res_inst_tac [("t", "y")] (zadd_int0_right RS subst) 1
+    THEN stac zadd_left_cancel 1);
+by (simp_tac (simpset() addsimps [eq_zdiff_eq RS sym]) 1);
+qed "zadd_cancel_end";
+
+
 
 
 structure Int_Cancel_Data =
@@ -33,6 +35,7 @@
   val thy	= IntDef.thy
   val T		= HOLogic.intT
   val zero	= Const ("IntDef.int", HOLogic.natT --> T) $ HOLogic.zero
+  val restrict_to_left  = restrict_to_left
   val add_cancel_21	= zadd_cancel_21
   val add_cancel_end	= zadd_cancel_end
   val add_left_cancel	= zadd_left_cancel
diff -r 5be4bb8e4e3f -r dca904d4ce4c src/HOL/Real/simproc.ML
--- a/src/HOL/Real/simproc.ML	Thu Sep 23 13:06:31 1999 +0200
+++ b/src/HOL/Real/simproc.ML	Thu Sep 23 13:07:25 1999 +0200
@@ -9,19 +9,19 @@
 (*** Two lemmas needed for the simprocs ***)
 
 (*Deletion of other terms in the formula, seeking the -x at the front of z*)
-val real_add_cancel_21 = prove_goal RealDef.thy
-    "((x::real) + (y + z) = y + u) = ((x + z) = u)"
-  (fn _ => [stac real_add_left_commute 1,
-	    rtac real_add_left_cancel 1]);
+Goal "((x::real) + (y + z) = y + u) = ((x + z) = u)";
+by (stac real_add_left_commute 1);
+by (rtac real_add_left_cancel 1);
+qed "real_add_cancel_21";
 
 (*A further rule to deal with the case that
   everything gets cancelled on the right.*)
-val real_add_cancel_end = prove_goal RealDef.thy
-    "((x::real) + (y + z) = y) = (x = -z)"
-  (fn _ => [stac real_add_left_commute 1,
-	    res_inst_tac [("t", "y")] (real_add_zero_right RS subst) 1,
-	    stac real_add_left_cancel 1,
-	    simp_tac (simpset() addsimps [real_eq_diff_eq RS sym]) 1]);
+Goal "((x::real) + (y + z) = y) = (x = -z)";
+by (stac real_add_left_commute 1);
+by (res_inst_tac [("t", "y")] (real_add_zero_right RS subst) 1
+    THEN stac real_add_left_cancel 1);
+by (simp_tac (simpset() addsimps [real_eq_diff_eq RS sym]) 1);
+qed "real_add_cancel_end";
 
 
 structure Real_Cancel_Data =
@@ -32,6 +32,7 @@
   val thy		= RealDef.thy
   val T			= Type ("RealDef.real", [])
   val zero		= Const ("RealDef.0r", T)
+  val restrict_to_left  = restrict_to_left
   val add_cancel_21	= real_add_cancel_21
   val add_cancel_end	= real_add_cancel_end
   val add_left_cancel	= real_add_left_cancel