Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Integ/presburger.ML
changeset 21708 45e7491bea47
parent 21588 cd0dc678a205
child 22548 6ce4bddf3bcb 
--- a/src/HOL/Integ/presburger.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/src/HOL/Integ/presburger.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -56,7 +56,7 @@
 val powerarith =
     (map thm ["nat_number_of", "zpower_number_of_even",
               "zpower_Pls", "zpower_Min"]) @
-    [(Tactic.simplify true [thm "zero_eq_Numeral0_nring",
+    [(MetaSimplifier.simplify true [thm "zero_eq_Numeral0_nring",
                            thm "one_eq_Numeral1_nring"]
   (thm "zpower_number_of_odd"))]
isabelle