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 22997 d4f3b015b50b
parent 22803 5129e02f4df2 
--- a/src/HOL/Integ/presburger.ML	Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Integ/presburger.ML	Thu May 17 19:49:40 2007 +0200
@@ -131,46 +131,46 @@
    ("op =", bT --> bT --> bT),
    ("Not", bT --> bT),
 
-   ("Orderings.less_eq", iT --> iT --> bT),
+   (@{const_name Orderings.less_eq}, iT --> iT --> bT),
    ("op =", iT --> iT --> bT),
-   ("Orderings.less", iT --> iT --> bT),
-   ("Divides.dvd", iT --> iT --> bT),
-   ("Divides.div", iT --> iT --> iT),
-   ("Divides.mod", iT --> iT --> iT),
-   ("HOL.plus", iT --> iT --> iT),
-   ("HOL.minus", iT --> iT --> iT),
-   ("HOL.times", iT --> iT --> iT),
-   ("HOL.abs", iT --> iT),
-   ("HOL.uminus", iT --> iT),
-   ("HOL.max", iT --> iT --> iT),
-   ("HOL.min", iT --> iT --> iT),
+   (@{const_name Orderings.less}, iT --> iT --> bT),
+   (@{const_name Divides.dvd}, iT --> iT --> bT),
+   (@{const_name Divides.div}, iT --> iT --> iT),
+   (@{const_name Divides.mod}, iT --> iT --> iT),
+   (@{const_name HOL.plus}, iT --> iT --> iT),
+   (@{const_name HOL.minus}, iT --> iT --> iT),
+   (@{const_name HOL.times}, iT --> iT --> iT),
+   (@{const_name HOL.abs}, iT --> iT),
+   (@{const_name HOL.uminus}, iT --> iT),
+   (@{const_name Orderings.max}, iT --> iT --> iT),
+   (@{const_name Orderings.min}, iT --> iT --> iT),
 
-   ("Orderings.less_eq", nT --> nT --> bT),
+   (@{const_name Orderings.less_eq}, nT --> nT --> bT),
    ("op =", nT --> nT --> bT),
-   ("Orderings.less", nT --> nT --> bT),
-   ("Divides.dvd", nT --> nT --> bT),
-   ("Divides.div", nT --> nT --> nT),
-   ("Divides.mod", 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),
+   (@{const_name Orderings.less}, nT --> nT --> bT),
+   (@{const_name Divides.dvd}, nT --> nT --> bT),
+   (@{const_name Divides.div}, nT --> nT --> nT),
+   (@{const_name Divides.mod}, nT --> nT --> nT),
+   (@{const_name HOL.plus}, nT --> nT --> nT),
+   (@{const_name HOL.minus}, nT --> nT --> nT),
+   (@{const_name HOL.times}, nT --> nT --> nT),
+   (@{const_name Suc}, nT --> nT),
+   (@{const_name Orderings.max}, nT --> nT --> nT),
+   (@{const_name Orderings.min}, nT --> nT --> nT),
 
-   ("Numeral.bit.B0", bitT),
-   ("Numeral.bit.B1", bitT),
-   ("Numeral.Bit", iT --> bitT --> iT),
-   ("Numeral.Pls", iT),
-   ("Numeral.Min", iT),
-   ("Numeral.number_of", iT --> iT),
-   ("Numeral.number_of", iT --> nT),
-   ("HOL.zero", nT),
-   ("HOL.zero", iT),
-   ("HOL.one", nT),
-   ("HOL.one", iT),
-   ("False", bT),
-   ("True", bT)];
+   (@{const_name Numeral.bit.B0}, bitT),
+   (@{const_name Numeral.bit.B1}, bitT),
+   (@{const_name Numeral.Bit}, iT --> bitT --> iT),
+   (@{const_name Numeral.Pls}, iT),
+   (@{const_name Numeral.Min}, iT),
+   (@{const_name Numeral.number_of}, iT --> iT),
+   (@{const_name Numeral.number_of}, iT --> nT),
+   (@{const_name HOL.zero}, nT),
+   (@{const_name HOL.zero}, iT),
+   (@{const_name HOL.one}, nT),
+   (@{const_name HOL.one}, iT),
+   (@{const_name False}, bT),
+   (@{const_name True}, bT)];
 
 (* Preparation of the formula to be sent to the Integer quantifier *)
 (* elimination procedure                                           *)
isabelle