# HG changeset patch # User wenzelm # Date 1127506909 -7200 # Node ID 5156b731ebc81578a4e63ec3999020eaab6dbeb6 # Parent 77e026bef398430a134daeecfea042f79c12d443 Provers/cancel_sums.ML: Simplifier.inherit_bounds; diff -r 77e026bef398 -r 5156b731ebc8 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Fri Sep 23 21:02:13 2005 +0200 +++ b/src/HOL/Divides.thy Fri Sep 23 22:21:49 2005 +0200 @@ -201,7 +201,7 @@ val prove_eq_sums = let val simps = add_0 :: add_0_right :: add_ac - in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all simps) end + in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end; end; diff -r 77e026bef398 -r 5156b731ebc8 src/HOL/Integ/IntDiv_setup.ML --- a/src/HOL/Integ/IntDiv_setup.ML Fri Sep 23 21:02:13 2005 +0200 +++ b/src/HOL/Integ/IntDiv_setup.ML Fri Sep 23 22:21:49 2005 +0200 @@ -25,7 +25,7 @@ val prove_eq_sums = let val simps = diff_int_def :: Int_Numeral_Simprocs.add_0s @ zadd_ac - in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all simps) end + in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end; end;