Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Provers/cancel_sums.ML: Simplifier.inherit_bounds;
authorwenzelm
Fri, 23 Sep 2005 22:21:49 +0200
changeset 17609 5156b731ebc8
parent 17608 77e026bef398
child 17610 58778df33e2f
Provers/cancel_sums.ML: Simplifier.inherit_bounds;
src/HOL/Divides.thy file | annotate | diff | comparison | revisions
src/HOL/Integ/IntDiv_setup.ML file | annotate | diff | comparison | revisions 
--- 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;
 
--- 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;
isabelle