# HG changeset patch
# User nipkow
# Date 1149770908 -7200
# Node ID 4499a73efb1c12e1189ac2b1bc481dba54446f78
# Parent  bb53575366217e261fe2286de53f232953b83622
less_equal -> less_eq (someone had screwd up here)

diff -r bb5357536621 -r 4499a73efb1c src/HOL/Integ/reflected_cooper.ML
--- 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)
diff -r bb5357536621 -r 4499a73efb1c src/HOL/Tools/Presburger/reflected_cooper.ML
--- 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)