--- a/src/HOL/Integ/int_arith1.ML Thu Feb 28 17:21:48 2002 +0100
+++ b/src/HOL/Integ/int_arith1.ML Thu Feb 28 17:46:46 2002 +0100
@@ -70,11 +70,6 @@
@zadd_ac@rel_iff_rel_0_rls) 1);
qed "le_add_iff2";
-(*To tidy up the result of a simproc. Only the RHS will be simplified.*)
-Goal "u = u' ==> (t==u) == (t==u')";
-by Auto_tac;
-qed "eq_cong2";
-
structure Int_Numeral_Simprocs =
struct
@@ -206,8 +201,8 @@
| trans_tac (Some th) = ALLGOALS (rtac (th RS trans));
fun simplify_meta_eq rules =
- mk_meta_eq o
simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
+ o mk_meta_eq;
structure CancelNumeralsCommon =
struct