# HG changeset patch
# User paulson
# Date 960372427 -7200
# Node ID 4d4521cbbcca2ef61cdd92071f51c5bfee364636
# Parent  3730ae0f513a28a1e475eb44050d685e8c4457ea
Real/simproc.ML now removed

diff -r 3730ae0f513a -r 4d4521cbbcca src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Jun 07 12:06:36 2000 +0200
+++ b/src/HOL/IsaMakefile	Wed Jun 07 12:07:07 2000 +0200
@@ -79,7 +79,7 @@
   Real/PNat.thy Real/PRat.ML Real/PRat.thy Real/PReal.ML \
   Real/PReal.thy Real/RComplete.ML Real/RComplete.thy Real/Real.thy \
   Real/RealDef.ML Real/RealDef.thy Real/RealOrd.ML Real/RealOrd.thy \
-  Real/simproc.ML Real/RealAbs.ML Real/RealAbs.thy Real/ROOT.ML \
+  Real/RealAbs.ML Real/RealAbs.thy Real/ROOT.ML \
   Real/RealBin.ML Real/RealBin.thy Real/RealInt.ML Real/RealInt.thy \
   Real/RealPow.ML Real/RealPow.thy Real/Hyperreal/Filter.ML \
   Real/Hyperreal/Filter.thy Real/Hyperreal/fuf.ML \
diff -r 3730ae0f513a -r 4d4521cbbcca src/HOL/Real/simproc.ML
--- a/src/HOL/Real/simproc.ML	Wed Jun 07 12:06:36 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,62 +0,0 @@
-(*  Title:      HOL/Real/simproc.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1998  University of Cambridge
-
-Apply Abel_Cancel to the reals
-*)
-
-(*** Two lemmas needed for the simprocs ***)
-
-(*Deletion of other terms in the formula, seeking the -x at the front of z*)
-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.*)
-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 =
-struct
-  val ss		= HOL_ss
-  val eq_reflection	= eq_reflection
-
-  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
-  val add_assoc		= real_add_assoc
-  val add_commute	= real_add_commute
-  val add_left_commute	= real_add_left_commute
-  val add_0		= real_add_zero_left
-  val add_0_right	= real_add_zero_right
-
-  val eq_diff_eq	= real_eq_diff_eq
-  val eqI_rules		= [real_less_eqI, real_eq_eqI, real_le_eqI]
-  fun dest_eqI th = 
-      #1 (HOLogic.dest_bin "op =" HOLogic.boolT 
-	      (HOLogic.dest_Trueprop (concl_of th)))
-
-  val diff_def		= real_diff_def
-  val minus_add_distrib	= real_minus_add_distrib
-  val minus_minus	= real_minus_minus
-  val minus_0		= real_minus_zero
-  val add_inverses	= [real_add_minus, real_add_minus_left];
-  val cancel_simps	= [real_add_minus_cancel, real_minus_add_cancel]
-end;
-
-structure Real_Cancel = Abel_Cancel (Real_Cancel_Data);
-
-Addsimprocs [Real_Cancel.sum_conv, Real_Cancel.rel_conv];
-