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.
less_equal -> less_eq (someone had screwd up here)
authornipkow
Thu, 08 Jun 2006 14:48:28 +0200
changeset 19826 4499a73efb1c
parent 19825 bb5357536621
child 19827 e9e9be6111bb
less_equal -> less_eq (someone had screwd up here)
src/HOL/Integ/reflected_cooper.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Presburger/reflected_cooper.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Integ/reflected_cooper.ML	Thu Jun 08 14:08:43 2006 +0200
+++ b/src/HOL/Integ/reflected_cooper.ML	Thu Jun 08 14:48:28 2006 +0200
@@ -91,11 +91,11 @@
       | F => HOLogic.false_const
       | Lt(t1,t2) => Const("Orderings.less",[iT,iT] ---> bT)$
 			   (term_of_i vs t1)$(term_of_i vs t2)
-      | Le(t1,t2) => Const("Orderings.less_equal",[iT,iT] ---> bT)$
+      | Le(t1,t2) => Const("Orderings.less_eq",[iT,iT] ---> bT)$
 			  (term_of_i vs t1)$(term_of_i vs t2)
       | Gt(t1,t2) => Const("Orderings.less",[iT,iT] ---> bT)$
 			   (term_of_i vs t2)$(term_of_i vs t1)
-      | Ge(t1,t2) => Const("Orderings.less_equal",[iT,iT] ---> bT)$
+      | Ge(t1,t2) => Const("Orderings.less_eq",[iT,iT] ---> bT)$
 			  (term_of_i vs t2)$(term_of_i vs t1)
       | Eq(t1,t2) => Const("op =",[iT,iT] ---> bT)$
 			   (term_of_i vs t1)$(term_of_i vs t2)
--- a/src/HOL/Tools/Presburger/reflected_cooper.ML	Thu Jun 08 14:08:43 2006 +0200
+++ b/src/HOL/Tools/Presburger/reflected_cooper.ML	Thu Jun 08 14:48:28 2006 +0200
@@ -91,11 +91,11 @@
       | F => HOLogic.false_const
       | Lt(t1,t2) => Const("Orderings.less",[iT,iT] ---> bT)$
 			   (term_of_i vs t1)$(term_of_i vs t2)
-      | Le(t1,t2) => Const("Orderings.less_equal",[iT,iT] ---> bT)$
+      | Le(t1,t2) => Const("Orderings.less_eq",[iT,iT] ---> bT)$
 			  (term_of_i vs t1)$(term_of_i vs t2)
       | Gt(t1,t2) => Const("Orderings.less",[iT,iT] ---> bT)$
 			   (term_of_i vs t2)$(term_of_i vs t1)
-      | Ge(t1,t2) => Const("Orderings.less_equal",[iT,iT] ---> bT)$
+      | Ge(t1,t2) => Const("Orderings.less_eq",[iT,iT] ---> bT)$
 			  (term_of_i vs t2)$(term_of_i vs t1)
       | Eq(t1,t2) => Const("op =",[iT,iT] ---> bT)$
 			   (term_of_i vs t1)$(term_of_i vs t2)
isabelle