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 19277 f7602e74d948
parent 19233 77ca20b0ed77
child 20053 7f32ce6354d6 
--- a/src/HOL/Tools/Presburger/presburger.ML	Thu Mar 16 20:19:25 2006 +0100
+++ b/src/HOL/Tools/Presburger/presburger.ML	Fri Mar 17 09:34:23 2006 +0100
@@ -133,9 +133,9 @@
    ("op =", bT --> bT --> bT),
    ("Not", bT --> bT),
 
-   ("op <=", iT --> iT --> bT),
+   ("Orderings.less_eq", iT --> iT --> bT),
    ("op =", iT --> iT --> bT),
-   ("op <", iT --> iT --> bT),
+   ("Orderings.less", iT --> iT --> bT),
    ("Divides.op dvd", iT --> iT --> bT),
    ("Divides.op div", iT --> iT --> iT),
    ("Divides.op mod", iT --> iT --> iT),
@@ -147,9 +147,9 @@
    ("HOL.max", iT --> iT --> iT),
    ("HOL.min", iT --> iT --> iT),
 
-   ("op <=", nT --> nT --> bT),
+   ("Orderings.less_eq", nT --> nT --> bT),
    ("op =", nT --> nT --> bT),
-   ("op <", nT --> nT --> bT),
+   ("Orderings.less", nT --> nT --> bT),
    ("Divides.op dvd", nT --> nT --> bT),
    ("Divides.op div", nT --> nT --> nT),
    ("Divides.op mod", nT --> nT --> nT),
isabelle