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/Tools/Presburger/presburger.ML
changeset 19233 77ca20b0ed77
parent 18708 4b3dadb4fe33
child 19277 f7602e74d948 
--- a/src/HOL/Tools/Presburger/presburger.ML	Fri Mar 10 12:28:38 2006 +0100
+++ b/src/HOL/Tools/Presburger/presburger.ML	Fri Mar 10 15:33:48 2006 +0100
@@ -139,11 +139,11 @@
    ("Divides.op dvd", iT --> iT --> bT),
    ("Divides.op div", iT --> iT --> iT),
    ("Divides.op mod", iT --> iT --> iT),
-   ("op +", iT --> iT --> iT),
-   ("op -", iT --> iT --> iT),
-   ("op *", iT --> iT --> iT), 
+   ("HOL.plus", iT --> iT --> iT),
+   ("HOL.minus", iT --> iT --> iT),
+   ("HOL.times", iT --> iT --> iT), 
    ("HOL.abs", iT --> iT),
-   ("uminus", iT --> iT),
+   ("HOL.uminus", iT --> iT),
    ("HOL.max", iT --> iT --> iT),
    ("HOL.min", iT --> iT --> iT),
 
@@ -153,9 +153,9 @@
    ("Divides.op dvd", nT --> nT --> bT),
    ("Divides.op div", nT --> nT --> nT),
    ("Divides.op mod", nT --> nT --> nT),
-   ("op +", nT --> nT --> nT),
-   ("op -", nT --> nT --> nT),
-   ("op *", nT --> nT --> nT), 
+   ("HOL.plus", nT --> nT --> nT),
+   ("HOL.minus", nT --> nT --> nT),
+   ("HOL.times", nT --> nT --> nT), 
    ("Suc", nT --> nT),
    ("HOL.max", nT --> nT --> nT),
    ("HOL.min", nT --> nT --> nT),
isabelle