# HG changeset patch
# User haftmann
# Date 1184934505 -7200
# Node ID 851c74f1bb696129f28a8775066a7605150b0978
# Parent  64b9806e160b81d13cd02cc3383556163fde7d2f
moved class ord from Orderings.thy to HOL.thy

diff -r 64b9806e160b -r 851c74f1bb69 NEWS
--- a/NEWS	Fri Jul 20 14:28:05 2007 +0200
+++ b/NEWS	Fri Jul 20 14:28:25 2007 +0200
@@ -943,9 +943,10 @@
     op +   ~> HOL.plus_class.plus
     op -   ~> HOL.minus_class.minus
     uminus ~> HOL.minus_class.uminus
+    abs    ~> HOL.abs_class.abs
     op *   ~> HOL.times_class.times
-    op <   ~> Orderings.ord_class.less
-    op <=  ~> Orderings.ord_class.less_eq
+    op <   ~> HOL.ord_class.less
+    op <=  ~> HOL.ord_class.less_eq
 
 Adaptions may be required in the following cases:
 
@@ -1044,7 +1045,7 @@
 r and finally gets the theorem t = r, which is again applied to the
 subgoal. An Example is available in HOL/ex/ReflectionEx.thy.
 
-* Reflection: Automatic refification now handels binding, an example
+* Reflection: Automatic reification now handels binding, an example
 is available in HOL/ex/ReflectionEx.thy
 
 
diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Arith_Tools.thy
--- a/src/HOL/Arith_Tools.thy	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Arith_Tools.thy	Fri Jul 20 14:28:25 2007 +0200
@@ -480,14 +480,14 @@
 
  fun proc3 phi ss ct =
   (case term_of ct of
-    Const(@{const_name "Orderings.less"},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
+    Const(@{const_name HOL.less},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
       let
         val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
         val _ = map is_number [a,b,c]
         val T = ctyp_of_term c
         val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
       in SOME (mk_meta_eq th) end
-  | Const(@{const_name "Orderings.less_eq"},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
+  | Const(@{const_name HOL.less_eq},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
       let
         val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
         val _ = map is_number [a,b,c]
@@ -501,14 +501,14 @@
         val T = ctyp_of_term c
         val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
       in SOME (mk_meta_eq th) end
-  | Const(@{const_name "Orderings.less"},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
+  | Const(@{const_name HOL.less},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
     let
       val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
         val _ = map is_number [a,b,c]
         val T = ctyp_of_term c
         val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
       in SOME (mk_meta_eq th) end
-  | Const(@{const_name "Orderings.less_eq"},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
+  | Const(@{const_name HOL.less_eq},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
     let
       val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
         val _ = map is_number [a,b,c]
@@ -745,7 +745,7 @@
 fun xnormalize_conv ctxt [] ct = reflexive ct
 | xnormalize_conv ctxt (vs as (x::_)) ct =
    case term_of ct of
-   Const(@{const_name "Orderings.less"},_)$_$Const(@{const_name "HOL.zero"},_) =>
+   Const(@{const_name HOL.less},_)$_$Const(@{const_name "HOL.zero"},_) =>
     (case whatis x (Thm.dest_arg1 ct) of
     ("c*x+t",[c,t]) =>
        let
@@ -788,7 +788,7 @@
     | _ => reflexive ct)
 
 
-|  Const(@{const_name "Orderings.less_eq"},_)$_$Const(@{const_name "HOL.zero"},_) =>
+|  Const(@{const_name HOL.less_eq},_)$_$Const(@{const_name "HOL.zero"},_) =>
    (case whatis x (Thm.dest_arg1 ct) of
     ("c*x+t",[c,t]) =>
        let
@@ -877,7 +877,7 @@
   val eq_iff_diff_eq_0 = mk_meta_eq @{thm "eq_iff_diff_eq_0"}
 in
 fun field_isolate_conv phi ctxt vs ct = case term_of ct of
-  Const(@{const_name "Orderings.less"},_)$a$b =>
+  Const(@{const_name HOL.less},_)$a$b =>
    let val (ca,cb) = Thm.dest_binop ct
        val T = ctyp_of_term ca
        val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
@@ -886,7 +886,7 @@
               (Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
        val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    in rth end
-| Const(@{const_name "Orderings.less_eq"},_)$a$b =>
+| Const(@{const_name HOL.less_eq},_)$a$b =>
    let val (ca,cb) = Thm.dest_binop ct
        val T = ctyp_of_term ca
        val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
@@ -917,11 +917,11 @@
                             else Ferrante_Rackoff_Data.Nox
    | @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
                             else Ferrante_Rackoff_Data.Nox
-   | Const(@{const_name "Orderings.less"},_)$y$z =>
+   | Const(@{const_name HOL.less},_)$y$z =>
        if term_of x aconv y then Ferrante_Rackoff_Data.Lt
         else if term_of x aconv z then Ferrante_Rackoff_Data.Gt
         else Ferrante_Rackoff_Data.Nox
-   | Const (@{const_name "Orderings.less_eq"},_)$y$z =>
+   | Const (@{const_name HOL.less_eq},_)$y$z =>
          if term_of x aconv y then Ferrante_Rackoff_Data.Le
          else if term_of x aconv z then Ferrante_Rackoff_Data.Ge
          else Ferrante_Rackoff_Data.Nox
diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Complex/ex/linreif.ML
--- a/src/HOL/Complex/ex/linreif.ML	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Complex/ex/linreif.ML	Fri Jul 20 14:28:25 2007 +0200
@@ -15,41 +15,37 @@
 exception LINR;
 
 (* pseudo reification : term -> intterm *)
-val iT = HOLogic.intT;
 val rT = Type ("RealDef.real",[]);
 val bT = HOLogic.boolT;
-val realC = Const("RealDef.real",iT --> rT);
-val rzero = Const("0",rT);
+val realC = @{term "RealDef.real :: int => real"};
+val rzero = @{term "0 :: real"};
 
-fun num_of_term vs t = 
-    case t of
-	Free(xn,xT) => (case AList.lookup (op =) vs t of 
-			   NONE   => error "Variable not found in the list!"
-			 | SOME n => Bound n)
+fun num_of_term vs t = case t
+   of Free(xn,xT) => (case AList.lookup (op =) vs t of 
+           NONE   => error "Variable not found in the list!"
+         | SOME n => Bound n)
       | Const("RealDef.real",_)$ @{term "0::int"} => C 0
       | Const("RealDef.real",_)$ @{term "1::int"} => C 1
       | @{term "0::real"} => C 0
       | @{term "0::real"} => C 1
       | Term.Bound i => Bound (nat i)
-      | Const(@{const_name "HOL.uminus"},_)$t' => Neg (num_of_term vs t')
+      | Const (@{const_name "HOL.uminus"},_)$t' => Neg (num_of_term vs t')
       | Const (@{const_name "HOL.plus"},_)$t1$t2 => Add (num_of_term vs t1,num_of_term vs t2)
       | Const (@{const_name "HOL.minus"},_)$t1$t2 => Sub (num_of_term vs t1,num_of_term vs t2)
-      | Const (@{const_name "HOL.times"},_)$t1$t2 => 
-	(case (num_of_term vs t1) of C i => 
-				     Mul (i,num_of_term vs t2)
-				   | _ => error "num_of_term: unsupported Multiplication")
+      | Const (@{const_name "HOL.times"},_)$t1$t2 => (case (num_of_term vs t1) of C i => 
+          Mul (i,num_of_term vs t2)
+        | _ => error "num_of_term: unsupported Multiplication")
       | Const("RealDef.real",_) $ Const (@{const_name "Numeral.number_of"},_)$t' => C (HOLogic.dest_numeral t')
       | Const (@{const_name "Numeral.number_of"},_)$t' => C (HOLogic.dest_numeral t')
       | _ => error ("num_of_term: unknown term " ^ (Display.raw_string_of_term t));
-	
 
 (* pseudo reification : term -> fm *)
 fun fm_of_term vs t = 
     case t of 
 	Const("True",_) => T
       | Const("False",_) => F
-      | Const(@{const_name "Orderings.less"},_)$t1$t2 => Lta (Sub (num_of_term vs t1,num_of_term vs t2))
-      | Const(@{const_name "Orderings.less_eq"},_)$t1$t2 => Lea (Sub (num_of_term vs t1,num_of_term vs t2))
+      | Const(@{const_name HOL.less},_)$t1$t2 => Lta (Sub (num_of_term vs t1,num_of_term vs t2))
+      | Const(@{const_name HOL.less_eq},_)$t1$t2 => Lea (Sub (num_of_term vs t1,num_of_term vs t2))
       | Const("op =",eqT)$t1$t2 => 
 	if (domain_type eqT = rT)
 	then Eqa (Sub (num_of_term vs t1,num_of_term vs t2)) 
@@ -64,13 +60,10 @@
 	A(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p)
       | _ => error ("fm_of_term : unknown term!" ^ (Display.raw_string_of_term t));
 
-fun zip [] [] = []
-  | zip (x::xs) (y::ys) = (x,y)::(zip xs ys);
-
 
 fun start_vs t =
     let val fs = term_frees t
-    in zip fs (map nat (0 upto  (length fs - 1)))
+    in fs ~~ map nat (0 upto  (length fs - 1))
     end ;
 
 (* transform num and fm back to terms *)
@@ -84,13 +77,13 @@
 fun term_of_num vs t =
     case t of 
 	C i => realC $ (HOLogic.mk_number HOLogic.intT i)
-      | Bound n => valOf (myassoc2 vs n)
-      | Neg t' => Const(@{const_name "HOL.uminus"},rT --> rT)$(term_of_num vs t')
-      | Add(t1,t2) => Const(@{const_name "HOL.plus"},[rT,rT] ---> rT)$
+      | Bound n => the (myassoc2 vs n)
+      | Neg t' => Const(@{const_name HOL.uminus},rT --> rT)$(term_of_num vs t')
+      | Add(t1,t2) => Const(@{const_name HOL.plus},[rT,rT] ---> rT)$
 			   (term_of_num vs t1)$(term_of_num vs t2)
-      | Sub(t1,t2) => Const(@{const_name "HOL.minus"},[rT,rT] ---> rT)$
+      | Sub(t1,t2) => Const(@{const_name HOL.minus},[rT,rT] ---> rT)$
 			   (term_of_num vs t1)$(term_of_num vs t2)
-      | Mul(i,t2) => Const(@{const_name "HOL.times"},[rT,rT] ---> rT)$
+      | Mul(i,t2) => Const(@{const_name HOL.times},[rT,rT] ---> rT)$
 			   (term_of_num vs (C i))$(term_of_num vs t2)
       | Cn(n,i,t) => term_of_num vs (Add (Mul(i,Bound n),t));
 
@@ -98,13 +91,13 @@
     case t of 
 	T => HOLogic.true_const 
       | F => HOLogic.false_const
-      | Lta t => Const(@{const_name "Orderings.less"},[rT,rT] ---> bT)$
+      | Lta t => Const(@{const_name HOL.less},[rT,rT] ---> bT)$
 			   (term_of_num vs t)$ rzero
-      | Lea t => Const(@{const_name "Orderings.less_eq"},[rT,rT] ---> bT)$
+      | Lea t => Const(@{const_name HOL.less_eq},[rT,rT] ---> bT)$
 			  (term_of_num vs t)$ rzero
-      | Gta t => Const(@{const_name "Orderings.less"},[rT,rT] ---> bT)$
+      | Gta t => Const(@{const_name HOL.less},[rT,rT] ---> bT)$
 			   rzero $(term_of_num vs t)
-      | Gea t => Const(@{const_name "Orderings.less_eq"},[rT,rT] ---> bT)$
+      | Gea t => Const(@{const_name HOL.less_eq},[rT,rT] ---> bT)$
 			  rzero $(term_of_num vs t)
       | Eqa t => Const("op =",[rT,rT] ---> bT)$
 			   (term_of_num vs t)$ rzero
diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Complex/ex/mireif.ML
--- a/src/HOL/Complex/ex/mireif.ML	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Complex/ex/mireif.ML	Fri Jul 20 14:28:25 2007 +0200
@@ -42,8 +42,8 @@
     case t of 
         Const("True",_) => T
       | Const("False",_) => F
-      | Const(@{const_name "Orderings.less"},_)$t1$t2 => Lta (Sub (num_of_term vs t1,num_of_term vs t2))
-      | Const(@{const_name "Orderings.less_eq"},_)$t1$t2 => Lea (Sub (num_of_term vs t1,num_of_term vs t2))
+      | Const(@{const_name HOL.less},_)$t1$t2 => Lta (Sub (num_of_term vs t1,num_of_term vs t2))
+      | Const(@{const_name HOL.less_eq},_)$t1$t2 => Lea (Sub (num_of_term vs t1,num_of_term vs t2))
       | Const (@{const_name "MIR.rdvd"},_ )$ (Const("RealDef.real",_) $ (Const(@{const_name "Numeral.number_of"},_)$t1))$t2 => 
         Dvda (HOLogic.dest_numeral t1, num_of_term vs t2)
       | Const("op =",eqT)$t1$t2 => 
diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Hoare/hoare.ML
--- a/src/HOL/Hoare/hoare.ML	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Hoare/hoare.ML	Fri Jul 20 14:28:25 2007 +0200
@@ -65,7 +65,7 @@
 fun mk_CollectC trm = let val T as Type ("fun",[t,_]) = fastype_of trm 
                       in Collect_const t $ trm end;
 
-fun inclt ty = Const (@{const_name Orderings.less_eq}, [ty,ty] ---> boolT);
+fun inclt ty = Const (@{const_name HOL.less_eq}, [ty,ty] ---> boolT);
 
 (** Makes "Mset <= t" **)
 fun Mset_incl t = let val MsetT = fastype_of t 
diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Hoare/hoareAbort.ML
--- a/src/HOL/Hoare/hoareAbort.ML	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Hoare/hoareAbort.ML	Fri Jul 20 14:28:25 2007 +0200
@@ -66,7 +66,7 @@
 fun mk_CollectC trm = let val T as Type ("fun",[t,_]) = fastype_of trm 
                       in Collect_const t $ trm end;
 
-fun inclt ty = Const (@{const_name Orderings.less_eq}, [ty,ty] ---> boolT);
+fun inclt ty = Const (@{const_name HOL.less_eq}, [ty,ty] ---> boolT);
 
 (** Makes "Mset <= t" **)
 fun Mset_incl t = let val MsetT = fastype_of t 
diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Import/Generate-HOL/GenHOL4Base.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Fri Jul 20 14:28:25 2007 +0200
@@ -166,7 +166,7 @@
 import_theory prim_rec;
 
 const_maps
-    "<" > Orderings.ord_class.less :: "[nat,nat]=>bool";
+    "<" > HOL.ord_class.less :: "[nat,nat]=>bool";
 
 end_import;
 
@@ -181,7 +181,7 @@
   ">"          > HOL4Compat.nat_gt
   ">="         > HOL4Compat.nat_ge
   FUNPOW       > HOL4Compat.FUNPOW
-  "<="         > Orderings.ord_class.less_eq :: "[nat,nat]=>bool"
+  "<="         > HOL.ord_class.less_eq :: "[nat,nat]=>bool"
   "+"          > HOL.plus_class.plus       :: "[nat,nat]=>nat"
   "*"          > HOL.times_class.times      :: "[nat,nat]=>nat"
   "-"          > HOL.minus_class.minus      :: "[nat,nat]=>nat"
diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Import/Generate-HOL/GenHOL4Real.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Fri Jul 20 14:28:25 2007 +0200
@@ -23,7 +23,7 @@
   inv      > HOL.inverse :: "real => real"
   real_add > HOL.plus    :: "[real,real] => real"
   real_mul > HOL.times   :: "[real,real] => real"
-  real_lt  > Orderings.ord_class.less :: "[real,real] => bool";
+  real_lt  > HOL.ord_class.less :: "[real,real] => bool";
 
 ignore_thms
     real_TY_DEF
@@ -51,7 +51,7 @@
 const_maps
   real_gt     > HOL4Compat.real_gt
   real_ge     > HOL4Compat.real_ge
-  real_lte    > Orderings.ord_class.less_eq :: "[real,real] => bool"
+  real_lte    > HOL.ord_class.less_eq :: "[real,real] => bool"
   real_sub    > HOL.minus    :: "[real,real] => real"
   "/"         > HOL.divide   :: "[real,real] => real"
   pow         > Nat.power    :: "[real,nat] => real"
diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Import/HOL/arithmetic.imp
--- a/src/HOL/Import/HOL/arithmetic.imp	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Import/HOL/arithmetic.imp	Fri Jul 20 14:28:25 2007 +0200
@@ -23,7 +23,7 @@
   "ALT_ZERO" > "HOL4Compat.ALT_ZERO"
   ">=" > "HOL4Compat.nat_ge"
   ">" > "HOL4Compat.nat_gt"
-  "<=" > "Orderings.ord_class.less_eq" :: "nat => nat => bool"
+  "<=" > "HOL.ord_class.less_eq" :: "nat => nat => bool"
   "-" > "HOL.minus_class.minus" :: "nat => nat => nat"
   "+" > "HOL.plus_class.plus" :: "nat => nat => nat"
   "*" > "HOL.times_class.times" :: "nat => nat => nat"
diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Import/HOL/prim_rec.imp
--- a/src/HOL/Import/HOL/prim_rec.imp	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Import/HOL/prim_rec.imp	Fri Jul 20 14:28:25 2007 +0200
@@ -18,7 +18,7 @@
   "PRIM_REC_FUN" > "HOL4Base.prim_rec.PRIM_REC_FUN"
   "PRIM_REC" > "HOL4Base.prim_rec.PRIM_REC"
   "PRE" > "HOL4Base.prim_rec.PRE"
-  "<" > "Orderings.ord_class.less" :: "nat => nat => bool"
+  "<" > "HOL.ord_class.less" :: "nat => nat => bool"
 
 thm_maps
   "wellfounded_primdef" > "HOL4Base.prim_rec.wellfounded_primdef"
diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Import/HOL/real.imp
--- a/src/HOL/Import/HOL/real.imp	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Import/HOL/real.imp	Fri Jul 20 14:28:25 2007 +0200
@@ -12,7 +12,7 @@
   "sum" > "HOL4Real.real.sum"
   "real_sub" > "HOL.minus_class.minus" :: "real => real => real"
   "real_of_num" > "RealDef.real" :: "nat => real"
-  "real_lte" > "Orderings.ord_class.less_eq" :: "real => real => bool"
+  "real_lte" > "HOL.ord_class.less_eq" :: "real => real => bool"
   "real_gt" > "HOL4Compat.real_gt"
   "real_ge" > "HOL4Compat.real_ge"
   "pow" > "Nat.power_class.power" :: "real => nat => real"
diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Import/HOL/realax.imp
--- a/src/HOL/Import/HOL/realax.imp	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Import/HOL/realax.imp	Fri Jul 20 14:28:25 2007 +0200
@@ -29,7 +29,7 @@
   "treal_0" > "HOL4Real.realax.treal_0"
   "real_neg" > "HOL.minus_class.uminus" :: "real => real"
   "real_mul" > "HOL.times_class.times" :: "real => real => real"
-  "real_lt" > "Orderings.ord_class.less" :: "real => real => bool"
+  "real_lt" > "HOL.ord_class.less" :: "real => real => bool"
   "real_add" > "HOL.plus_class.plus" :: "real => real => real"
   "real_1" > "HOL.one_class.one" :: "real"
   "real_0" > "HOL.zero_class.zero" :: "real"
diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Library/sct.ML
--- a/src/HOL/Library/sct.ML	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Library/sct.ML	Fri Jul 20 14:28:25 2007 +0200
@@ -63,8 +63,8 @@
     in Const (nth_const, lT --> HOLogic.natT --> T) $ xs end
 
 
-val less_nat_const = Const (@{const_name Orderings.less}, HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
-val lesseq_nat_const = Const (@{const_name Orderings.less_eq}, HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
+val less_nat_const = Const (@{const_name HOL.less}, HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
+val lesseq_nat_const = Const (@{const_name HOL.less_eq}, HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
 
 val has_edge_simps = [thm "Graphs.has_edge_def", thm "Graphs.dest_graph.simps"]
 
diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Orderings.thy	Fri Jul 20 14:28:25 2007 +0200
@@ -6,88 +6,12 @@
 header {* Syntactic and abstract orders *}
 
 theory Orderings
-imports HOL
+imports Set Fun
 uses
   (*"~~/src/Provers/quasi.ML"*)
   "~~/src/Provers/order.ML"
 begin
 
-subsection {* Order syntax *}
-
-class ord = type +
-  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<sqsubseteq>" 50)
-    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<sqsubset>" 50)
-begin
-
-notation
-  less_eq  ("op \<^loc><=") and
-  less_eq  ("(_/ \<^loc><= _)" [51, 51] 50) and
-  less  ("op \<^loc><") and
-  less  ("(_/ \<^loc>< _)"  [51, 51] 50)
-  
-notation (xsymbols)
-  less_eq  ("op \<^loc>\<le>") and
-  less_eq  ("(_/ \<^loc>\<le> _)"  [51, 51] 50)
-
-notation (HTML output)
-  less_eq  ("op \<^loc>\<le>") and
-  less_eq  ("(_/ \<^loc>\<le> _)"  [51, 51] 50)
-
-abbreviation (input)
-  greater  (infix "\<^loc>>" 50) where
-  "x \<^loc>> y \<equiv> y \<^loc>< x"
-
-abbreviation (input)
-  greater_eq  (infix "\<^loc>>=" 50) where
-  "x \<^loc>>= y \<equiv> y \<^loc><= x"
-
-notation (input)
-  greater_eq  (infix "\<^loc>\<ge>" 50)
-
-text {*
-  syntactic min/max -- these definitions reach
-  their usual semantics in class linorder ahead.
-*}
-
-definition
-  min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
-  "min a b = (if a \<^loc>\<le> b then a else b)"
-
-definition
-  max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
-  "max a b = (if a \<^loc>\<le> b then b else a)"
-
-end
-
-notation
-  less_eq  ("op <=") and
-  less_eq  ("(_/ <= _)" [51, 51] 50) and
-  less  ("op <") and
-  less  ("(_/ < _)"  [51, 51] 50)
-  
-notation (xsymbols)
-  less_eq  ("op \<le>") and
-  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
-
-notation (HTML output)
-  less_eq  ("op \<le>") and
-  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
-
-abbreviation (input)
-  greater  (infix ">" 50) where
-  "x > y \<equiv> y < x"
-
-abbreviation (input)
-  greater_eq  (infix ">=" 50) where
-  "x >= y \<equiv> y <= x"
-
-notation (input)
-  greater_eq  (infix "\<ge>" 50)
-
-lemmas min_def [code func, code unfold, code inline del] = min_def [folded ord_class.min]
-lemmas max_def [code func, code unfold, code inline del] = max_def [folded ord_class.max]
-
-
 subsection {* Partial orders *}
 
 class order = ord +
@@ -265,7 +189,20 @@
   (simp add: less_le, auto intro: antisym order_trans simp add: linear)
 
 
-text {* min/max properties *}
+text {* min/max *}
+
+text {* for historic reasons, definitions are done in context ord *}
+
+definition (in ord)
+  min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
+  "min a b = (if a \<^loc>\<le> b then a else b)"
+
+definition (in ord)
+  max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
+  "max a b = (if a \<^loc>\<le> b then b else a)"
+
+lemmas (in -) min_def [code func, code unfold, code inline del] = min_def [folded ord_class.min]
+lemmas (in -) max_def [code func, code unfold, code inline del] = max_def [folded ord_class.max]
 
 lemma min_le_iff_disj:
   "min x y \<^loc>\<le> z \<longleftrightarrow> x \<^loc>\<le> z \<or> y \<^loc>\<le> z"
@@ -370,11 +307,11 @@
           if of_sort t1
           then SOME (t1, "=", t2)
           else NONE
-      | dec (Const (@{const_name Orderings.less_eq},  _) $ t1 $ t2) =
+      | dec (Const (@{const_name HOL.less_eq},  _) $ t1 $ t2) =
           if of_sort t1
           then SOME (t1, "<=", t2)
           else NONE
-      | dec (Const (@{const_name Orderings.less},  _) $ t1 $ t2) =
+      | dec (Const (@{const_name HOL.less},  _) $ t1 $ t2) =
           if of_sort t1
           then SOME (t1, "<", t2)
           else NONE
@@ -840,7 +777,81 @@
   unfolding le_bool_def less_bool_def by simp_all
 
 
-subsection {* Monotonicity, syntactic least value operator and min/max *}
+subsection {* Order on sets *}
+
+instance set :: (type) order
+  by (intro_classes,
+      (assumption | rule subset_refl subset_trans subset_antisym psubset_eq)+)
+
+lemmas basic_trans_rules [trans] =
+  order_trans_rules set_rev_mp set_mp
+
+
+subsection {* Order on functions *}
+
+instance "fun" :: (type, ord) ord
+  le_fun_def: "f \<le> g \<equiv> \<forall>x. f x \<le> g x"
+  less_fun_def: "f < g \<equiv> f \<le> g \<and> f \<noteq> g" ..
+
+lemmas [code func del] = le_fun_def less_fun_def
+
+instance "fun" :: (type, order) order
+  by default
+    (auto simp add: le_fun_def less_fun_def expand_fun_eq
+       intro: order_trans order_antisym)
+
+lemma le_funI: "(\<And>x. f x \<le> g x) \<Longrightarrow> f \<le> g"
+  unfolding le_fun_def by simp
+
+lemma le_funE: "f \<le> g \<Longrightarrow> (f x \<le> g x \<Longrightarrow> P) \<Longrightarrow> P"
+  unfolding le_fun_def by simp
+
+lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
+  unfolding le_fun_def by simp
+
+text {*
+  Handy introduction and elimination rules for @{text "\<le>"}
+  on unary and binary predicates
+*}
+
+lemma predicate1I [Pure.intro!, intro!]:
+  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
+  shows "P \<le> Q"
+  apply (rule le_funI)
+  apply (rule le_boolI)
+  apply (rule PQ)
+  apply assumption
+  done
+
+lemma predicate1D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
+  apply (erule le_funE)
+  apply (erule le_boolE)
+  apply assumption+
+  done
+
+lemma predicate2I [Pure.intro!, intro!]:
+  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
+  shows "P \<le> Q"
+  apply (rule le_funI)+
+  apply (rule le_boolI)
+  apply (rule PQ)
+  apply assumption
+  done
+
+lemma predicate2D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
+  apply (erule le_funE)+
+  apply (erule le_boolE)
+  apply assumption+
+  done
+
+lemma rev_predicate1D: "P x ==> P <= Q ==> Q x"
+  by (rule predicate1D)
+
+lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y"
+  by (rule predicate2D)
+
+
+subsection {* Monotonicity, least value operator and min/max *}
 
 locale mono =
   fixes f
@@ -849,11 +860,6 @@
 lemmas monoI [intro?] = mono.intro
   and monoD [dest?] = mono.mono
 
-constdefs
-  Least :: "('a::ord => bool) => 'a"               (binder "LEAST " 10)
-  "Least P == THE x. P x & (ALL y. P y --> x <= y)"
-    -- {* We can no longer use LeastM because the latter requires Hilbert-AC. *}
-
 lemma LeastI2_order:
   "[| P (x::'a::order);
       !!y. P y ==> x <= y;
@@ -864,6 +870,16 @@
   apply (blast intro: order_antisym)+
 done
 
+lemma Least_mono:
+  "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
+    ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
+    -- {* Courtesy of Stephan Merz *}
+  apply clarify
+  apply (erule_tac P = "%x. x : S" in LeastI2_order, fast)
+  apply (rule LeastI2_order)
+  apply (auto elim: monoD intro!: order_antisym)
+  done
+
 lemma Least_equality:
   "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"
 apply (simp add: Least_def)
diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Jul 20 14:28:25 2007 +0200
@@ -74,10 +74,10 @@
 | Const ("op =",ty)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
 | Const("Not",_) $ (Const ("op =",_)$y$_) => 
   if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
-| Const ("Orderings.ord_class.less",_)$y$z =>
+| Const (@{const_name HOL.less}, _) $ y$ z =>
    if term_of x aconv y then Lt (Thm.dest_arg ct) 
    else if term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox
-| Const ("Orderings.ord_class.less_eq",_)$y$z => 
+| Const (@{const_name HOL.less_eq}, _) $ y $ z => 
    if term_of x aconv y then Le (Thm.dest_arg ct) 
    else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
 | Const (@{const_name Divides.dvd},_)$_$(Const(@{const_name "HOL.plus"},_)$y$_) =>
@@ -222,10 +222,10 @@
   end 
  | _ => addC$(mulC$one$tm)$zero;
 
-fun lin (vs as x::_) (Const("Not",_)$(Const("Orderings.ord_class.less",T)$s$t)) = 
-    lin vs (Const("Orderings.ord_class.less_eq",T)$t$s)
-  | lin (vs as x::_) (Const("Not",_)$(Const("Orderings.ord_class.less_eq",T)$s$t)) = 
-    lin vs (Const("Orderings.ord_class.less",T)$t$s)
+fun lin (vs as x::_) (Const("Not", _) $ (Const (@{const_name HOL.less}, T) $ s $ t)) = 
+    lin vs (Const(@{const_name HOL.less_eq}, T) $ t $ s)
+  | lin (vs as x::_) (Const("Not",_) $ (Const(@{const_name HOL.less_eq}, T) $ s $ t)) = 
+    lin vs (Const(@{const_name HOL.less}, T) $ t $ s)
   | lin vs (Const ("Not",T)$t) = Const ("Not",T)$ (lin vs t)
   | lin (vs as x::_) (Const(@{const_name Divides.dvd},_)$d$t) = 
     HOLogic.mk_binrel @{const_name Divides.dvd} (numeral1 abs d, lint vs t)
@@ -298,12 +298,12 @@
   fun h (acc,dacc) t = 
    case (term_of t) of
     Const(s,_)$(Const("HOL.times_class.times",_)$c$y)$ _ => 
-    if x aconv y 
-       andalso s mem ["op =", "Orderings.ord_class.less", "Orderings.ord_class.less_eq"] 
+    if x aconv y andalso member (op =)
+      ["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s
     then (ins (dest_numeral c) acc,dacc) else (acc,dacc)
   | Const(s,_)$_$(Const("HOL.times_class.times",_)$c$y) => 
-    if x aconv y 
-       andalso s mem ["Orderings.ord_class.less", "Orderings.ord_class.less_eq"] 
+    if x aconv y andalso member (op =)
+       [@{const_name HOL.less}, @{const_name HOL.less_eq}] s 
     then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
   | Const(@{const_name Divides.dvd},_)$_$(Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c$y)$_) => 
     if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)
@@ -338,10 +338,12 @@
   | Const("op |",_)$_$_ => binop_conv unit_conv t
   | Const("Not",_)$_ => arg_conv unit_conv t
   | Const(s,_)$(Const("HOL.times_class.times",_)$c$y)$ _ => 
-    if x=y andalso s mem ["op =", "Orderings.ord_class.less", "Orderings.ord_class.less_eq"] 
+    if x=y andalso member (op =)
+      ["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s
     then cv (Integer.div l (dest_numeral c)) t else Thm.reflexive t
   | Const(s,_)$_$(Const("HOL.times_class.times",_)$c$y) => 
-    if x=y andalso s mem ["Orderings.ord_class.less", "Orderings.ord_class.less_eq"] 
+    if x=y andalso member (op =)
+      [@{const_name HOL.less}, @{const_name HOL.less_eq}] s
     then cv (Integer.div l (dest_numeral c)) t else Thm.reflexive t
   | Const(@{const_name Divides.dvd},_)$d$(r as (Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c$y)$_)) => 
     if x=y then 
@@ -559,8 +561,8 @@
 fun qf_of_term ps vs t =  case t
  of Const("True",_) => T
   | Const("False",_) => F
-  | Const(@{const_name Orderings.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
-  | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
+  | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
+  | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
   | Const(@{const_name Divides.dvd},_)$t1$t2 => 
       (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")
   | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Tools/function_package/lexicographic_order.ML
--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Jul 20 14:28:25 2007 +0200
@@ -130,13 +130,13 @@
 fun mk_cell (thy : theory) solve_tac (vars, prems, lhs, rhs) mfun =
     let
       val goals = mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
-      val less_thm = goals "Orderings.ord_class.less" |> prove thy solve_tac
+      val less_thm = goals @{const_name HOL.less} |> prove thy solve_tac
     in
       if Thm.no_prems less_thm then
         Less (Goal.finish less_thm)
       else
         let
-          val lesseq_thm = goals "Orderings.ord_class.less_eq" |> prove thy solve_tac
+          val lesseq_thm = goals @{const_name HOL.less_eq} |> prove thy solve_tac
         in
           if Thm.no_prems lesseq_thm then
             LessEq (Goal.finish lesseq_thm, less_thm)
diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Fri Jul 20 14:28:25 2007 +0200
@@ -181,7 +181,7 @@
     case concl of
       Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
     | _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
-    | _ $ (Const ("Orderings.ord_class.less_eq", _) $ _ $ _) =>
+    | _ $ (Const ("HOL.ord_class.less_eq", _) $ _ $ _) =>
       [dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
          (resolve_tac [le_funI, le_boolI'])) thm))]
     | _ => [thm]
@@ -554,7 +554,7 @@
          (make_bool_args HOLogic.mk_not I bs i)) preds));
 
     val ind_concl = HOLogic.mk_Trueprop
-      (HOLogic.mk_binrel "Orderings.ord_class.less_eq" (rec_const, ind_pred));
+      (HOLogic.mk_binrel "HOL.ord_class.less_eq" (rec_const, ind_pred));
 
     val raw_fp_induct = (mono RS (fp_def RS def_lfp_induct));
 
diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Tools/refute.ML	Fri Jul 20 14:28:25 2007 +0200
@@ -696,7 +696,7 @@
       | Const ("Finite_Set.card", _)    => t
       | Const ("Finite_Set.Finites", _) => t
       | Const ("Finite_Set.finite", _)  => t
-      | Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
+      | Const (@{const_name HOL.less}, Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t
       | Const (@{const_name HOL.plus}, Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
@@ -883,7 +883,7 @@
       | Const ("Finite_Set.card", T)    => collect_type_axioms (axs, T)
       | Const ("Finite_Set.Finites", T) => collect_type_axioms (axs, T)
       | Const ("Finite_Set.finite", T)  => collect_type_axioms (axs, T)
-      | Const (@{const_name Orderings.less}, T as Type ("fun", [Type ("nat", []),
+      | Const (@{const_name HOL.less}, T as Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
           collect_type_axioms (axs, T)
       | Const (@{const_name HOL.plus}, T as Type ("fun", [Type ("nat", []),
@@ -2602,13 +2602,13 @@
   (* theory -> model -> arguments -> Term.term ->
     (interpretation * model * arguments) option *)
 
-  (* only an optimization: 'Orderings.less' could in principle be            *)
+  (* only an optimization: 'HOL.less' could in principle be            *)
   (* interpreted with interpreters available already (using its definition), *)
   (* but the code below is more efficient                                    *)
 
   fun Nat_less_interpreter thy model args t =
     case t of
-      Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
+      Const (@{const_name HOL.less}, Type ("fun", [Type ("nat", []),
         Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
       let
         val (i_nat, _, _) = interpret thy model
diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Tools/res_clause.ML	Fri Jul 20 14:28:25 2007 +0200
@@ -89,8 +89,8 @@
 (*Provide readable names for the more common symbolic functions*)
 val const_trans_table =
       Symtab.make [("op =", "equal"),
-	  	   (@{const_name Orderings.less_eq}, "lessequals"),
-		   (@{const_name Orderings.less}, "less"),
+	  	   (@{const_name HOL.less_eq}, "lessequals"),
+		   (@{const_name HOL.less}, "less"),
 		   ("op &", "and"),
 		   ("op |", "or"),
 		   (@{const_name HOL.plus}, "plus"),
diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/arith_data.ML	Fri Jul 20 14:28:25 2007 +0200
@@ -107,8 +107,8 @@
 structure LessCancelSums = CancelSumsFun
 (struct
   open Sum;
-  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less};
-  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT;
+  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less};
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT;
   val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
 end);
 
@@ -117,8 +117,8 @@
 structure LeCancelSums = CancelSumsFun
 (struct
   open Sum;
-  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq};
-  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT;
+  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq};
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT;
   val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
 end);
 
@@ -370,8 +370,8 @@
   val (q, j) = poly (rhs, Rat.one, ([], Rat.zero))
 in
   case rel of
-    @{const_name Orderings.less}    => SOME (p, i, "<", q, j)
-  | @{const_name Orderings.less_eq} => SOME (p, i, "<=", q, j)
+    @{const_name HOL.less}    => SOME (p, i, "<", q, j)
+  | @{const_name HOL.less_eq} => SOME (p, i, "<=", q, j)
   | "op ="              => SOME (p, i, "=", q, j)
   | _                   => NONE
 end handle Zero => NONE;
@@ -523,7 +523,7 @@
         val rev_terms     = rev terms
         val terms1        = map (subst_term [(split_term, t1)]) rev_terms
         val terms2        = map (subst_term [(split_term, t2)]) rev_terms
-        val t1_leq_t2     = Const (@{const_name Orderings.less_eq},
+        val t1_leq_t2     = Const (@{const_name HOL.less_eq},
                                     split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
         val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
         val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
@@ -538,7 +538,7 @@
         val rev_terms     = rev terms
         val terms1        = map (subst_term [(split_term, t1)]) rev_terms
         val terms2        = map (subst_term [(split_term, t2)]) rev_terms
-        val t1_leq_t2     = Const (@{const_name Orderings.less_eq},
+        val t1_leq_t2     = Const (@{const_name HOL.less_eq},
                                     split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
         val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
         val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
@@ -555,9 +555,9 @@
         val terms2      = map (subst_term [(split_term, Const (@{const_name HOL.uminus},
                             split_type --> split_type) $ t1)]) rev_terms
         val zero        = Const (@{const_name HOL.zero}, split_type)
-        val zero_leq_t1 = Const (@{const_name Orderings.less_eq},
+        val zero_leq_t1 = Const (@{const_name HOL.less_eq},
                             split_type --> split_type --> HOLogic.boolT) $ zero $ t1
-        val t1_lt_zero  = Const (@{const_name Orderings.less},
+        val t1_lt_zero  = Const (@{const_name HOL.less},
                             split_type --> split_type --> HOLogic.boolT) $ t1 $ zero
         val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1    = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false]
@@ -578,7 +578,7 @@
                                 (map (incr_boundvars 1) rev_terms)
         val t1'             = incr_boundvars 1 t1
         val t2'             = incr_boundvars 1 t2
-        val t1_lt_t2        = Const (@{const_name Orderings.less},
+        val t1_lt_t2        = Const (@{const_name HOL.less},
                                 split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
         val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
                                 (Const (@{const_name HOL.plus},
@@ -602,7 +602,7 @@
         val t1'         = incr_boundvars 1 t1
         val t1_eq_int_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
                             (Const ("Nat.of_nat", HOLogic.natT --> HOLogic.intT) $ n)
-        val t1_lt_zero  = Const (@{const_name Orderings.less},
+        val t1_lt_zero  = Const (@{const_name HOL.less},
                             HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
         val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1    = (HOLogic.mk_Trueprop t1_eq_int_n) :: terms1 @ [not_false]
@@ -628,7 +628,7 @@
                                         split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
         val t2_neq_zero             = HOLogic.mk_not (Const ("op =",
                                         split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
-        val j_lt_t2                 = Const (@{const_name Orderings.less},
+        val j_lt_t2                 = Const (@{const_name HOL.less},
                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
         val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
                                        (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
@@ -660,7 +660,7 @@
                                         split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
         val t2_neq_zero             = HOLogic.mk_not (Const ("op =",
                                         split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
-        val j_lt_t2                 = Const (@{const_name Orderings.less},
+        val j_lt_t2                 = Const (@{const_name HOL.less},
                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
         val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
                                        (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
@@ -697,18 +697,18 @@
                                         (number_of $
                                           (Const (@{const_name HOL.uminus},
                                             HOLogic.intT --> HOLogic.intT) $ k'))
-        val zero_leq_j              = Const (@{const_name Orderings.less_eq},
+        val zero_leq_j              = Const (@{const_name HOL.less_eq},
                                         split_type --> split_type --> HOLogic.boolT) $ zero $ j
-        val j_lt_t2                 = Const (@{const_name Orderings.less},
+        val j_lt_t2                 = Const (@{const_name HOL.less},
                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
         val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
                                        (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
                                          (Const (@{const_name HOL.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
         val neg_t2                  = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
-        val t2_lt_j                 = Const (@{const_name Orderings.less},
+        val t2_lt_j                 = Const (@{const_name HOL.less},
                                         split_type --> split_type--> HOLogic.boolT) $ t2' $ j
-        val j_leq_zero              = Const (@{const_name Orderings.less_eq},
+        val j_leq_zero              = Const (@{const_name HOL.less_eq},
                                         split_type --> split_type --> HOLogic.boolT) $ j $ zero
         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1                = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
@@ -749,9 +749,9 @@
                                         (number_of $
                                           (Const (@{const_name HOL.uminus},
                                             HOLogic.intT --> HOLogic.intT) $ k'))
-        val zero_leq_j              = Const (@{const_name Orderings.less_eq},
+        val zero_leq_j              = Const (@{const_name HOL.less_eq},
                                         split_type --> split_type --> HOLogic.boolT) $ zero $ j
-        val j_lt_t2                 = Const (@{const_name Orderings.less},
+        val j_lt_t2                 = Const (@{const_name HOL.less},
                                         split_type --> split_type--> HOLogic.boolT) $ j $ t2'
         val t1_eq_t2_times_i_plus_j = Const ("op =",
                                         split_type --> split_type --> HOLogic.boolT) $ t1' $
@@ -759,9 +759,9 @@
                                          (Const (@{const_name HOL.times},
                                            split_type --> split_type --> split_type) $ t2' $ i) $ j)
         val neg_t2                  = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
-        val t2_lt_j                 = Const (@{const_name Orderings.less},
+        val t2_lt_j                 = Const (@{const_name HOL.less},
                                         split_type --> split_type--> HOLogic.boolT) $ t2' $ j
-        val j_leq_zero              = Const (@{const_name Orderings.less_eq},
+        val j_leq_zero              = Const (@{const_name HOL.less_eq},
                                         split_type --> split_type --> HOLogic.boolT) $ j $ zero
         val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
         val subgoal1                = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
@@ -1011,24 +1011,24 @@
     val r = #prop(rep_thm thm);
   in
     case r of
-      Tr $ ((c as Const(@{const_name Orderings.less_eq},T)) $ s $ t) =>
+      Tr $ ((c as Const(@{const_name HOL.less_eq},T)) $ s $ t) =>
         let val r' = Tr $ (c $ t $ s)
         in
           case Library.find_first (prp r') prems of
             NONE =>
-              let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name Orderings.less},T) $ s $ t))
+              let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name HOL.less},T) $ s $ t))
               in case Library.find_first (prp r') prems of
                    NONE => []
                  | SOME thm' => [(thm' RS not_lessD) RS (thm RS antisym)]
               end
           | SOME thm' => [thm' RS (thm RS antisym)]
         end
-    | Tr $ (Const("Not",_) $ (Const(@{const_name Orderings.less},T) $ s $ t)) =>
-        let val r' = Tr $ (Const(@{const_name Orderings.less_eq},T) $ s $ t)
+    | Tr $ (Const("Not",_) $ (Const(@{const_name HOL.less},T) $ s $ t)) =>
+        let val r' = Tr $ (Const(@{const_name HOL.less_eq},T) $ s $ t)
         in
           case Library.find_first (prp r') prems of
             NONE =>
-              let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name Orderings.less},T) $ t $ s))
+              let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name HOL.less},T) $ t $ s))
               in case Library.find_first (prp r') prems of
                    NONE => []
                  | SOME thm' =>
diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/ex/coopereif.ML
--- a/src/HOL/ex/coopereif.ML	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/ex/coopereif.ML	Fri Jul 20 14:28:25 2007 +0200
@@ -32,8 +32,8 @@
 fun qf_of_term ps vs t = case t
      of Const("True",_) => T
       | Const("False",_) => F
-      | Const(@{const_name "Orderings.less"},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
-      | Const(@{const_name "Orderings.less_eq"},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
+      | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
+      | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
       | Const(@{const_name "Divides.dvd"},_)$t1$t2 => 
           (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => error "qf_of_term: unsupported dvd")
       | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/ex/svc_funcs.ML
--- a/src/HOL/ex/svc_funcs.ML	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/ex/svc_funcs.ML	Fri Jul 20 14:28:25 2007 +0200
@@ -112,8 +112,8 @@
                          b1 orelse b2)
                      end
                  else (*might be numeric equality*) (t, is_intnat T)
-           | Const(@{const_name Orderings.less}, Type ("fun", [T,_]))  => (t, is_intnat T)
-           | Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) => (t, is_intnat T)
+           | Const(@{const_name HOL.less}, Type ("fun", [T,_]))  => (t, is_intnat T)
+           | Const(@{const_name HOL.less_eq}, Type ("fun", [T,_])) => (t, is_intnat T)
            | _ => (t, false)
          end
    in #1 o tag end;
@@ -216,13 +216,13 @@
                    else fail t
             end
         (*inequalities: possible types are nat, int, real*)
-      | fm pos (t as Const(@{const_name Orderings.less},  Type ("fun", [T,_])) $ x $ y) =
+      | fm pos (t as Const(@{const_name HOL.less},  Type ("fun", [T,_])) $ x $ y) =
             if not pos orelse T = HOLogic.realT then
                 Buildin("<", [tm x, tm y])
             else if is_intnat T then
                 Buildin("<=", [suc (tm x), tm y])
             else fail t
-      | fm pos (t as Const(@{const_name Orderings.less_eq},  Type ("fun", [T,_])) $ x $ y) =
+      | fm pos (t as Const(@{const_name HOL.less_eq},  Type ("fun", [T,_])) $ x $ y) =
             if pos orelse T = HOLogic.realT then
                 Buildin("<=", [tm x, tm y])
             else if is_intnat T then
diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/ex/svc_oracle.ML
--- a/src/HOL/ex/svc_oracle.ML	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/ex/svc_oracle.ML	Fri Jul 20 14:28:25 2007 +0200
@@ -78,8 +78,8 @@
       | fm ((c as Const("True", _))) = c
       | fm ((c as Const("False", _))) = c
       | fm (t as Const("op =",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
-      | fm (t as Const(@{const_name Orderings.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
-      | fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+      | fm (t as Const(@{const_name HOL.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+      | fm (t as Const(@{const_name HOL.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
       | fm t = replace t
     (*entry point, and abstraction of a meta-formula*)
     fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/int_arith1.ML
--- a/src/HOL/int_arith1.ML	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/int_arith1.ML	Fri Jul 20 14:28:25 2007 +0200
@@ -110,8 +110,8 @@
       mk_meta_eq ([f_eq, f_number_of_eq] MRS trans)
 
   (*reorientation simprules using ==, for the following simproc*)
-  val meta_zero_reorient = zero_reorient RS eq_reflection
-  val meta_one_reorient = one_reorient RS eq_reflection
+  val meta_zero_reorient = @{thm zero_reorient} RS eq_reflection
+  val meta_one_reorient = @{thm one_reorient} RS eq_reflection
   val meta_number_of_reorient = number_of_reorient RS eq_reflection
 
   (*reorientation simplification procedure: reorients (polymorphic) 
@@ -350,9 +350,9 @@
   val trans_tac         = fn _ => trans_tac
 
   val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
-    diff_simps @ minus_simps @ add_ac
+    diff_simps @ minus_simps @ @{thms add_ac}
   val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
-  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ add_ac @ mult_ac
+  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
   fun norm_tac ss =
     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
@@ -376,8 +376,8 @@
 structure LessCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
-  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
+  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
   val bal_add1 = less_add_iff1 RS trans
   val bal_add2 = less_add_iff2 RS trans
 );
@@ -385,8 +385,8 @@
 structure LeCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
-  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
+  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
   val bal_add1 = le_add_iff1 RS trans
   val bal_add2 = le_add_iff2 RS trans
 );
@@ -433,9 +433,9 @@
   val trans_tac         = fn _ => trans_tac
 
   val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
-    diff_simps @ minus_simps @ add_ac
+    diff_simps @ minus_simps @ @{thms add_ac}
   val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
-  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ add_ac @ mult_ac
+  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
   fun norm_tac ss =
     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
@@ -463,9 +463,9 @@
   val trans_tac         = fn _ => trans_tac
 
   val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
-    inverse_1s @ divide_simps @ diff_simps @ minus_simps @ add_ac
+    inverse_1s @ divide_simps @ diff_simps @ minus_simps @ @{thms add_ac}
   val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
-  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ add_ac @ mult_ac
+  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
   fun norm_tac ss =
     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
@@ -541,7 +541,7 @@
 
 structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
 struct
-  val assoc_ss = HOL_ss addsimps mult_ac
+  val assoc_ss = HOL_ss addsimps @{thms mult_ac}
   val eq_reflection = eq_reflection
 end;
 
diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/int_factor_simprocs.ML
--- a/src/HOL/int_factor_simprocs.ML	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/int_factor_simprocs.ML	Fri Jul 20 14:28:25 2007 +0200
@@ -33,7 +33,7 @@
 
   val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
   val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
-  val norm_ss3 = HOL_ss addsimps mult_ac
+  val norm_ss3 = HOL_ss addsimps @{thms mult_ac}
   fun norm_tac ss =
     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
@@ -78,8 +78,8 @@
 structure LessCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
-  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
+  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
   val cancel = @{thm mult_less_cancel_left} RS trans
   val neg_exchanges = true
 )
@@ -87,8 +87,8 @@
 structure LeCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
-  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
+  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
   val cancel = @{thm mult_le_cancel_left} RS trans
   val neg_exchanges = true
 )
@@ -216,7 +216,7 @@
 
 (** Final simplification for the CancelFactor simprocs **)
 val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq  
-  [@{thm mult_1_left}, mult_1_right, @{thm zdiv_1}, numeral_1_eq_1];
+  [@{thm mult_1_left}, @{thm mult_1_right}, @{thm zdiv_1}, numeral_1_eq_1];
 
 fun cancel_simplify_meta_eq cancel_th ss th =
     simplify_one ss (([th, cancel_th]) MRS trans);
@@ -229,7 +229,7 @@
   val dest_coeff        = dest_coeff
   val find_first        = find_first_t []
   val trans_tac         = fn _ => trans_tac
-  val norm_ss = HOL_ss addsimps mult_1s @ mult_ac
+  val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   end;
 
diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/nat_simprocs.ML
--- a/src/HOL/nat_simprocs.ML	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/nat_simprocs.ML	Fri Jul 20 14:28:25 2007 +0200
@@ -125,15 +125,15 @@
 
 
 (*Simplify 1*n and n*1 to n*)
-val add_0s  = map rename_numerals [add_0, add_0_right];
+val add_0s  = map rename_numerals [@{thm add_0}, @{thm add_0_right}];
 val mult_1s = map rename_numerals [@{thm nat_mult_1}, @{thm nat_mult_1_right}];
 
 (*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
 
 (*And these help the simproc return False when appropriate, which helps
   the arith prover.*)
-val contra_rules = [add_Suc, add_Suc_right, Zero_not_Suc, Suc_not_Zero,
-                    le_0_eq];
+val contra_rules = [@{thm add_Suc}, @{thm add_Suc_right}, @{thm Zero_not_Suc},
+  @{thm Suc_not_Zero}, @{thm le_0_eq}];
 
 val simplify_meta_eq =
     Int_Numeral_Simprocs.simplify_meta_eq
@@ -157,8 +157,8 @@
   val trans_tac         = fn _ => trans_tac
 
   val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
-    [@{thm Suc_eq_add_numeral_1_left}] @ add_ac
-  val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac
+    [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
+  val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   fun norm_tac ss = 
     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
@@ -181,8 +181,8 @@
 structure LessCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
-  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
+  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
   val bal_add1 = @{thm nat_less_add_iff1} RS trans
   val bal_add2 = @{thm nat_less_add_iff2} RS trans
 );
@@ -190,8 +190,8 @@
 structure LeCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
-  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
+  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
   val bal_add1 = @{thm nat_le_add_iff1} RS trans
   val bal_add2 = @{thm nat_le_add_iff2} RS trans
 );
@@ -245,8 +245,8 @@
   val prove_conv        = Int_Numeral_Base_Simprocs.prove_conv_nohyps
   val trans_tac         = fn _ => trans_tac
 
-  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ add_ac
-  val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac
+  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
+  val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   fun norm_tac ss =
     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
@@ -271,8 +271,8 @@
   val trans_tac         = fn _ => trans_tac
 
   val norm_ss1 = num_ss addsimps
-    numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ add_ac
-  val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac
+    numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
+  val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   fun norm_tac ss =
     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
@@ -303,8 +303,8 @@
 structure LessCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
-  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
+  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
   val cancel = @{thm nat_mult_less_cancel1} RS trans
   val neg_exchanges = true
 )
@@ -312,8 +312,8 @@
 structure LeCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
-  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
+  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
   val cancel = @{thm nat_mult_le_cancel1} RS trans
   val neg_exchanges = true
 )
@@ -363,7 +363,7 @@
   val dest_coeff        = dest_coeff
   val find_first        = find_first_t []
   val trans_tac         = fn _ => trans_tac
-  val norm_ss = HOL_ss addsimps mult_1s @ mult_ac
+  val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   end;
 
@@ -378,16 +378,16 @@
 structure LessCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
-  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
+  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
   val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_less_cancel_disj}
 );
 
 structure LeCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
-  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
-  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
+  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
   val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_le_cancel_disj}
 );