# HG changeset patch
# User paulson
# Date 957797924 -7200
# Node ID 074503906abfbfd8405bd9c02a14c1a9d94f6392
# Parent  d6122f13b8a6f8f3bd0de35aecc6c9cd3a73dd22
better simplification of the result of simprocs

diff -r d6122f13b8a6 -r 074503906abf src/HOL/Integ/IntArith.ML
--- a/src/HOL/Integ/IntArith.ML	Mon May 08 16:58:18 2000 +0200
+++ b/src/HOL/Integ/IntArith.ML	Mon May 08 16:58:44 2000 +0200
@@ -77,7 +77,7 @@
 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')";
+Goal "u = u' ==> (t==u) == (t==u')";
 by Auto_tac;
 qed "eq_cong2";
 
@@ -200,7 +200,7 @@
 
 fun simplify_meta_eq rules =
     mk_meta_eq o
-    simplify (HOL_basic_ss addcongs[eq_cong2] addsimps rules)
+    simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
 
 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
 fun prep_pat s = Thm.read_cterm (Theory.sign_of Int.thy) (s, HOLogic.termT);