moved class ord from Orderings.thy to HOL.thy
authorhaftmann
Fri Jul 20 14:28:25 2007 +0200 (2007-07-20)
changeset 23881851c74f1bb69
parent 23880 64b9806e160b
child 23882 83b0f2518380
moved class ord from Orderings.thy to HOL.thy
NEWS
src/HOL/Arith_Tools.thy
src/HOL/Complex/ex/linreif.ML
src/HOL/Complex/ex/mireif.ML
src/HOL/Hoare/hoare.ML
src/HOL/Hoare/hoareAbort.ML
src/HOL/Import/Generate-HOL/GenHOL4Base.thy
src/HOL/Import/Generate-HOL/GenHOL4Real.thy
src/HOL/Import/HOL/arithmetic.imp
src/HOL/Import/HOL/prim_rec.imp
src/HOL/Import/HOL/real.imp
src/HOL/Import/HOL/realax.imp
src/HOL/Library/sct.ML
src/HOL/Orderings.thy
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/function_package/lexicographic_order.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/res_clause.ML
src/HOL/arith_data.ML
src/HOL/ex/coopereif.ML
src/HOL/ex/svc_funcs.ML
src/HOL/ex/svc_oracle.ML
src/HOL/int_arith1.ML
src/HOL/int_factor_simprocs.ML
src/HOL/nat_simprocs.ML
     1.1 --- a/NEWS	Fri Jul 20 14:28:05 2007 +0200
     1.2 +++ b/NEWS	Fri Jul 20 14:28:25 2007 +0200
     1.3 @@ -943,9 +943,10 @@
     1.4      op +   ~> HOL.plus_class.plus
     1.5      op -   ~> HOL.minus_class.minus
     1.6      uminus ~> HOL.minus_class.uminus
     1.7 +    abs    ~> HOL.abs_class.abs
     1.8      op *   ~> HOL.times_class.times
     1.9 -    op <   ~> Orderings.ord_class.less
    1.10 -    op <=  ~> Orderings.ord_class.less_eq
    1.11 +    op <   ~> HOL.ord_class.less
    1.12 +    op <=  ~> HOL.ord_class.less_eq
    1.13  
    1.14  Adaptions may be required in the following cases:
    1.15  
    1.16 @@ -1044,7 +1045,7 @@
    1.17  r and finally gets the theorem t = r, which is again applied to the
    1.18  subgoal. An Example is available in HOL/ex/ReflectionEx.thy.
    1.19  
    1.20 -* Reflection: Automatic refification now handels binding, an example
    1.21 +* Reflection: Automatic reification now handels binding, an example
    1.22  is available in HOL/ex/ReflectionEx.thy
    1.23  
    1.24  
     2.1 --- a/src/HOL/Arith_Tools.thy	Fri Jul 20 14:28:05 2007 +0200
     2.2 +++ b/src/HOL/Arith_Tools.thy	Fri Jul 20 14:28:25 2007 +0200
     2.3 @@ -480,14 +480,14 @@
     2.4  
     2.5   fun proc3 phi ss ct =
     2.6    (case term_of ct of
     2.7 -    Const(@{const_name "Orderings.less"},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
     2.8 +    Const(@{const_name HOL.less},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
     2.9        let
    2.10          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
    2.11          val _ = map is_number [a,b,c]
    2.12          val T = ctyp_of_term c
    2.13          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
    2.14        in SOME (mk_meta_eq th) end
    2.15 -  | Const(@{const_name "Orderings.less_eq"},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
    2.16 +  | Const(@{const_name HOL.less_eq},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
    2.17        let
    2.18          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
    2.19          val _ = map is_number [a,b,c]
    2.20 @@ -501,14 +501,14 @@
    2.21          val T = ctyp_of_term c
    2.22          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
    2.23        in SOME (mk_meta_eq th) end
    2.24 -  | Const(@{const_name "Orderings.less"},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
    2.25 +  | Const(@{const_name HOL.less},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
    2.26      let
    2.27        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
    2.28          val _ = map is_number [a,b,c]
    2.29          val T = ctyp_of_term c
    2.30          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
    2.31        in SOME (mk_meta_eq th) end
    2.32 -  | Const(@{const_name "Orderings.less_eq"},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
    2.33 +  | Const(@{const_name HOL.less_eq},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
    2.34      let
    2.35        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
    2.36          val _ = map is_number [a,b,c]
    2.37 @@ -745,7 +745,7 @@
    2.38  fun xnormalize_conv ctxt [] ct = reflexive ct
    2.39  | xnormalize_conv ctxt (vs as (x::_)) ct =
    2.40     case term_of ct of
    2.41 -   Const(@{const_name "Orderings.less"},_)$_$Const(@{const_name "HOL.zero"},_) =>
    2.42 +   Const(@{const_name HOL.less},_)$_$Const(@{const_name "HOL.zero"},_) =>
    2.43      (case whatis x (Thm.dest_arg1 ct) of
    2.44      ("c*x+t",[c,t]) =>
    2.45         let
    2.46 @@ -788,7 +788,7 @@
    2.47      | _ => reflexive ct)
    2.48  
    2.49  
    2.50 -|  Const(@{const_name "Orderings.less_eq"},_)$_$Const(@{const_name "HOL.zero"},_) =>
    2.51 +|  Const(@{const_name HOL.less_eq},_)$_$Const(@{const_name "HOL.zero"},_) =>
    2.52     (case whatis x (Thm.dest_arg1 ct) of
    2.53      ("c*x+t",[c,t]) =>
    2.54         let
    2.55 @@ -877,7 +877,7 @@
    2.56    val eq_iff_diff_eq_0 = mk_meta_eq @{thm "eq_iff_diff_eq_0"}
    2.57  in
    2.58  fun field_isolate_conv phi ctxt vs ct = case term_of ct of
    2.59 -  Const(@{const_name "Orderings.less"},_)$a$b =>
    2.60 +  Const(@{const_name HOL.less},_)$a$b =>
    2.61     let val (ca,cb) = Thm.dest_binop ct
    2.62         val T = ctyp_of_term ca
    2.63         val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
    2.64 @@ -886,7 +886,7 @@
    2.65                (Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
    2.66         val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    2.67     in rth end
    2.68 -| Const(@{const_name "Orderings.less_eq"},_)$a$b =>
    2.69 +| Const(@{const_name HOL.less_eq},_)$a$b =>
    2.70     let val (ca,cb) = Thm.dest_binop ct
    2.71         val T = ctyp_of_term ca
    2.72         val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
    2.73 @@ -917,11 +917,11 @@
    2.74                              else Ferrante_Rackoff_Data.Nox
    2.75     | @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
    2.76                              else Ferrante_Rackoff_Data.Nox
    2.77 -   | Const(@{const_name "Orderings.less"},_)$y$z =>
    2.78 +   | Const(@{const_name HOL.less},_)$y$z =>
    2.79         if term_of x aconv y then Ferrante_Rackoff_Data.Lt
    2.80          else if term_of x aconv z then Ferrante_Rackoff_Data.Gt
    2.81          else Ferrante_Rackoff_Data.Nox
    2.82 -   | Const (@{const_name "Orderings.less_eq"},_)$y$z =>
    2.83 +   | Const (@{const_name HOL.less_eq},_)$y$z =>
    2.84           if term_of x aconv y then Ferrante_Rackoff_Data.Le
    2.85           else if term_of x aconv z then Ferrante_Rackoff_Data.Ge
    2.86           else Ferrante_Rackoff_Data.Nox
     3.1 --- a/src/HOL/Complex/ex/linreif.ML	Fri Jul 20 14:28:05 2007 +0200
     3.2 +++ b/src/HOL/Complex/ex/linreif.ML	Fri Jul 20 14:28:25 2007 +0200
     3.3 @@ -15,41 +15,37 @@
     3.4  exception LINR;
     3.5  
     3.6  (* pseudo reification : term -> intterm *)
     3.7 -val iT = HOLogic.intT;
     3.8  val rT = Type ("RealDef.real",[]);
     3.9  val bT = HOLogic.boolT;
    3.10 -val realC = Const("RealDef.real",iT --> rT);
    3.11 -val rzero = Const("0",rT);
    3.12 +val realC = @{term "RealDef.real :: int => real"};
    3.13 +val rzero = @{term "0 :: real"};
    3.14  
    3.15 -fun num_of_term vs t = 
    3.16 -    case t of
    3.17 -	Free(xn,xT) => (case AList.lookup (op =) vs t of 
    3.18 -			   NONE   => error "Variable not found in the list!"
    3.19 -			 | SOME n => Bound n)
    3.20 +fun num_of_term vs t = case t
    3.21 +   of Free(xn,xT) => (case AList.lookup (op =) vs t of 
    3.22 +           NONE   => error "Variable not found in the list!"
    3.23 +         | SOME n => Bound n)
    3.24        | Const("RealDef.real",_)$ @{term "0::int"} => C 0
    3.25        | Const("RealDef.real",_)$ @{term "1::int"} => C 1
    3.26        | @{term "0::real"} => C 0
    3.27        | @{term "0::real"} => C 1
    3.28        | Term.Bound i => Bound (nat i)
    3.29 -      | Const(@{const_name "HOL.uminus"},_)$t' => Neg (num_of_term vs t')
    3.30 +      | Const (@{const_name "HOL.uminus"},_)$t' => Neg (num_of_term vs t')
    3.31        | Const (@{const_name "HOL.plus"},_)$t1$t2 => Add (num_of_term vs t1,num_of_term vs t2)
    3.32        | Const (@{const_name "HOL.minus"},_)$t1$t2 => Sub (num_of_term vs t1,num_of_term vs t2)
    3.33 -      | Const (@{const_name "HOL.times"},_)$t1$t2 => 
    3.34 -	(case (num_of_term vs t1) of C i => 
    3.35 -				     Mul (i,num_of_term vs t2)
    3.36 -				   | _ => error "num_of_term: unsupported Multiplication")
    3.37 +      | Const (@{const_name "HOL.times"},_)$t1$t2 => (case (num_of_term vs t1) of C i => 
    3.38 +          Mul (i,num_of_term vs t2)
    3.39 +        | _ => error "num_of_term: unsupported Multiplication")
    3.40        | Const("RealDef.real",_) $ Const (@{const_name "Numeral.number_of"},_)$t' => C (HOLogic.dest_numeral t')
    3.41        | Const (@{const_name "Numeral.number_of"},_)$t' => C (HOLogic.dest_numeral t')
    3.42        | _ => error ("num_of_term: unknown term " ^ (Display.raw_string_of_term t));
    3.43 -	
    3.44  
    3.45  (* pseudo reification : term -> fm *)
    3.46  fun fm_of_term vs t = 
    3.47      case t of 
    3.48  	Const("True",_) => T
    3.49        | Const("False",_) => F
    3.50 -      | Const(@{const_name "Orderings.less"},_)$t1$t2 => Lta (Sub (num_of_term vs t1,num_of_term vs t2))
    3.51 -      | Const(@{const_name "Orderings.less_eq"},_)$t1$t2 => Lea (Sub (num_of_term vs t1,num_of_term vs t2))
    3.52 +      | Const(@{const_name HOL.less},_)$t1$t2 => Lta (Sub (num_of_term vs t1,num_of_term vs t2))
    3.53 +      | Const(@{const_name HOL.less_eq},_)$t1$t2 => Lea (Sub (num_of_term vs t1,num_of_term vs t2))
    3.54        | Const("op =",eqT)$t1$t2 => 
    3.55  	if (domain_type eqT = rT)
    3.56  	then Eqa (Sub (num_of_term vs t1,num_of_term vs t2)) 
    3.57 @@ -64,13 +60,10 @@
    3.58  	A(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p)
    3.59        | _ => error ("fm_of_term : unknown term!" ^ (Display.raw_string_of_term t));
    3.60  
    3.61 -fun zip [] [] = []
    3.62 -  | zip (x::xs) (y::ys) = (x,y)::(zip xs ys);
    3.63 -
    3.64  
    3.65  fun start_vs t =
    3.66      let val fs = term_frees t
    3.67 -    in zip fs (map nat (0 upto  (length fs - 1)))
    3.68 +    in fs ~~ map nat (0 upto  (length fs - 1))
    3.69      end ;
    3.70  
    3.71  (* transform num and fm back to terms *)
    3.72 @@ -84,13 +77,13 @@
    3.73  fun term_of_num vs t =
    3.74      case t of 
    3.75  	C i => realC $ (HOLogic.mk_number HOLogic.intT i)
    3.76 -      | Bound n => valOf (myassoc2 vs n)
    3.77 -      | Neg t' => Const(@{const_name "HOL.uminus"},rT --> rT)$(term_of_num vs t')
    3.78 -      | Add(t1,t2) => Const(@{const_name "HOL.plus"},[rT,rT] ---> rT)$
    3.79 +      | Bound n => the (myassoc2 vs n)
    3.80 +      | Neg t' => Const(@{const_name HOL.uminus},rT --> rT)$(term_of_num vs t')
    3.81 +      | Add(t1,t2) => Const(@{const_name HOL.plus},[rT,rT] ---> rT)$
    3.82  			   (term_of_num vs t1)$(term_of_num vs t2)
    3.83 -      | Sub(t1,t2) => Const(@{const_name "HOL.minus"},[rT,rT] ---> rT)$
    3.84 +      | Sub(t1,t2) => Const(@{const_name HOL.minus},[rT,rT] ---> rT)$
    3.85  			   (term_of_num vs t1)$(term_of_num vs t2)
    3.86 -      | Mul(i,t2) => Const(@{const_name "HOL.times"},[rT,rT] ---> rT)$
    3.87 +      | Mul(i,t2) => Const(@{const_name HOL.times},[rT,rT] ---> rT)$
    3.88  			   (term_of_num vs (C i))$(term_of_num vs t2)
    3.89        | Cn(n,i,t) => term_of_num vs (Add (Mul(i,Bound n),t));
    3.90  
    3.91 @@ -98,13 +91,13 @@
    3.92      case t of 
    3.93  	T => HOLogic.true_const 
    3.94        | F => HOLogic.false_const
    3.95 -      | Lta t => Const(@{const_name "Orderings.less"},[rT,rT] ---> bT)$
    3.96 +      | Lta t => Const(@{const_name HOL.less},[rT,rT] ---> bT)$
    3.97  			   (term_of_num vs t)$ rzero
    3.98 -      | Lea t => Const(@{const_name "Orderings.less_eq"},[rT,rT] ---> bT)$
    3.99 +      | Lea t => Const(@{const_name HOL.less_eq},[rT,rT] ---> bT)$
   3.100  			  (term_of_num vs t)$ rzero
   3.101 -      | Gta t => Const(@{const_name "Orderings.less"},[rT,rT] ---> bT)$
   3.102 +      | Gta t => Const(@{const_name HOL.less},[rT,rT] ---> bT)$
   3.103  			   rzero $(term_of_num vs t)
   3.104 -      | Gea t => Const(@{const_name "Orderings.less_eq"},[rT,rT] ---> bT)$
   3.105 +      | Gea t => Const(@{const_name HOL.less_eq},[rT,rT] ---> bT)$
   3.106  			  rzero $(term_of_num vs t)
   3.107        | Eqa t => Const("op =",[rT,rT] ---> bT)$
   3.108  			   (term_of_num vs t)$ rzero
     4.1 --- a/src/HOL/Complex/ex/mireif.ML	Fri Jul 20 14:28:05 2007 +0200
     4.2 +++ b/src/HOL/Complex/ex/mireif.ML	Fri Jul 20 14:28:25 2007 +0200
     4.3 @@ -42,8 +42,8 @@
     4.4      case t of 
     4.5          Const("True",_) => T
     4.6        | Const("False",_) => F
     4.7 -      | Const(@{const_name "Orderings.less"},_)$t1$t2 => Lta (Sub (num_of_term vs t1,num_of_term vs t2))
     4.8 -      | Const(@{const_name "Orderings.less_eq"},_)$t1$t2 => Lea (Sub (num_of_term vs t1,num_of_term vs t2))
     4.9 +      | Const(@{const_name HOL.less},_)$t1$t2 => Lta (Sub (num_of_term vs t1,num_of_term vs t2))
    4.10 +      | Const(@{const_name HOL.less_eq},_)$t1$t2 => Lea (Sub (num_of_term vs t1,num_of_term vs t2))
    4.11        | Const (@{const_name "MIR.rdvd"},_ )$ (Const("RealDef.real",_) $ (Const(@{const_name "Numeral.number_of"},_)$t1))$t2 => 
    4.12          Dvda (HOLogic.dest_numeral t1, num_of_term vs t2)
    4.13        | Const("op =",eqT)$t1$t2 => 
     5.1 --- a/src/HOL/Hoare/hoare.ML	Fri Jul 20 14:28:05 2007 +0200
     5.2 +++ b/src/HOL/Hoare/hoare.ML	Fri Jul 20 14:28:25 2007 +0200
     5.3 @@ -65,7 +65,7 @@
     5.4  fun mk_CollectC trm = let val T as Type ("fun",[t,_]) = fastype_of trm 
     5.5                        in Collect_const t $ trm end;
     5.6  
     5.7 -fun inclt ty = Const (@{const_name Orderings.less_eq}, [ty,ty] ---> boolT);
     5.8 +fun inclt ty = Const (@{const_name HOL.less_eq}, [ty,ty] ---> boolT);
     5.9  
    5.10  (** Makes "Mset <= t" **)
    5.11  fun Mset_incl t = let val MsetT = fastype_of t 
     6.1 --- a/src/HOL/Hoare/hoareAbort.ML	Fri Jul 20 14:28:05 2007 +0200
     6.2 +++ b/src/HOL/Hoare/hoareAbort.ML	Fri Jul 20 14:28:25 2007 +0200
     6.3 @@ -66,7 +66,7 @@
     6.4  fun mk_CollectC trm = let val T as Type ("fun",[t,_]) = fastype_of trm 
     6.5                        in Collect_const t $ trm end;
     6.6  
     6.7 -fun inclt ty = Const (@{const_name Orderings.less_eq}, [ty,ty] ---> boolT);
     6.8 +fun inclt ty = Const (@{const_name HOL.less_eq}, [ty,ty] ---> boolT);
     6.9  
    6.10  (** Makes "Mset <= t" **)
    6.11  fun Mset_incl t = let val MsetT = fastype_of t 
     7.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Fri Jul 20 14:28:05 2007 +0200
     7.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Fri Jul 20 14:28:25 2007 +0200
     7.3 @@ -166,7 +166,7 @@
     7.4  import_theory prim_rec;
     7.5  
     7.6  const_maps
     7.7 -    "<" > Orderings.ord_class.less :: "[nat,nat]=>bool";
     7.8 +    "<" > HOL.ord_class.less :: "[nat,nat]=>bool";
     7.9  
    7.10  end_import;
    7.11  
    7.12 @@ -181,7 +181,7 @@
    7.13    ">"          > HOL4Compat.nat_gt
    7.14    ">="         > HOL4Compat.nat_ge
    7.15    FUNPOW       > HOL4Compat.FUNPOW
    7.16 -  "<="         > Orderings.ord_class.less_eq :: "[nat,nat]=>bool"
    7.17 +  "<="         > HOL.ord_class.less_eq :: "[nat,nat]=>bool"
    7.18    "+"          > HOL.plus_class.plus       :: "[nat,nat]=>nat"
    7.19    "*"          > HOL.times_class.times      :: "[nat,nat]=>nat"
    7.20    "-"          > HOL.minus_class.minus      :: "[nat,nat]=>nat"
     8.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Fri Jul 20 14:28:05 2007 +0200
     8.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Fri Jul 20 14:28:25 2007 +0200
     8.3 @@ -23,7 +23,7 @@
     8.4    inv      > HOL.inverse :: "real => real"
     8.5    real_add > HOL.plus    :: "[real,real] => real"
     8.6    real_mul > HOL.times   :: "[real,real] => real"
     8.7 -  real_lt  > Orderings.ord_class.less :: "[real,real] => bool";
     8.8 +  real_lt  > HOL.ord_class.less :: "[real,real] => bool";
     8.9  
    8.10  ignore_thms
    8.11      real_TY_DEF
    8.12 @@ -51,7 +51,7 @@
    8.13  const_maps
    8.14    real_gt     > HOL4Compat.real_gt
    8.15    real_ge     > HOL4Compat.real_ge
    8.16 -  real_lte    > Orderings.ord_class.less_eq :: "[real,real] => bool"
    8.17 +  real_lte    > HOL.ord_class.less_eq :: "[real,real] => bool"
    8.18    real_sub    > HOL.minus    :: "[real,real] => real"
    8.19    "/"         > HOL.divide   :: "[real,real] => real"
    8.20    pow         > Nat.power    :: "[real,nat] => real"
     9.1 --- a/src/HOL/Import/HOL/arithmetic.imp	Fri Jul 20 14:28:05 2007 +0200
     9.2 +++ b/src/HOL/Import/HOL/arithmetic.imp	Fri Jul 20 14:28:25 2007 +0200
     9.3 @@ -23,7 +23,7 @@
     9.4    "ALT_ZERO" > "HOL4Compat.ALT_ZERO"
     9.5    ">=" > "HOL4Compat.nat_ge"
     9.6    ">" > "HOL4Compat.nat_gt"
     9.7 -  "<=" > "Orderings.ord_class.less_eq" :: "nat => nat => bool"
     9.8 +  "<=" > "HOL.ord_class.less_eq" :: "nat => nat => bool"
     9.9    "-" > "HOL.minus_class.minus" :: "nat => nat => nat"
    9.10    "+" > "HOL.plus_class.plus" :: "nat => nat => nat"
    9.11    "*" > "HOL.times_class.times" :: "nat => nat => nat"
    10.1 --- a/src/HOL/Import/HOL/prim_rec.imp	Fri Jul 20 14:28:05 2007 +0200
    10.2 +++ b/src/HOL/Import/HOL/prim_rec.imp	Fri Jul 20 14:28:25 2007 +0200
    10.3 @@ -18,7 +18,7 @@
    10.4    "PRIM_REC_FUN" > "HOL4Base.prim_rec.PRIM_REC_FUN"
    10.5    "PRIM_REC" > "HOL4Base.prim_rec.PRIM_REC"
    10.6    "PRE" > "HOL4Base.prim_rec.PRE"
    10.7 -  "<" > "Orderings.ord_class.less" :: "nat => nat => bool"
    10.8 +  "<" > "HOL.ord_class.less" :: "nat => nat => bool"
    10.9  
   10.10  thm_maps
   10.11    "wellfounded_primdef" > "HOL4Base.prim_rec.wellfounded_primdef"
    11.1 --- a/src/HOL/Import/HOL/real.imp	Fri Jul 20 14:28:05 2007 +0200
    11.2 +++ b/src/HOL/Import/HOL/real.imp	Fri Jul 20 14:28:25 2007 +0200
    11.3 @@ -12,7 +12,7 @@
    11.4    "sum" > "HOL4Real.real.sum"
    11.5    "real_sub" > "HOL.minus_class.minus" :: "real => real => real"
    11.6    "real_of_num" > "RealDef.real" :: "nat => real"
    11.7 -  "real_lte" > "Orderings.ord_class.less_eq" :: "real => real => bool"
    11.8 +  "real_lte" > "HOL.ord_class.less_eq" :: "real => real => bool"
    11.9    "real_gt" > "HOL4Compat.real_gt"
   11.10    "real_ge" > "HOL4Compat.real_ge"
   11.11    "pow" > "Nat.power_class.power" :: "real => nat => real"
    12.1 --- a/src/HOL/Import/HOL/realax.imp	Fri Jul 20 14:28:05 2007 +0200
    12.2 +++ b/src/HOL/Import/HOL/realax.imp	Fri Jul 20 14:28:25 2007 +0200
    12.3 @@ -29,7 +29,7 @@
    12.4    "treal_0" > "HOL4Real.realax.treal_0"
    12.5    "real_neg" > "HOL.minus_class.uminus" :: "real => real"
    12.6    "real_mul" > "HOL.times_class.times" :: "real => real => real"
    12.7 -  "real_lt" > "Orderings.ord_class.less" :: "real => real => bool"
    12.8 +  "real_lt" > "HOL.ord_class.less" :: "real => real => bool"
    12.9    "real_add" > "HOL.plus_class.plus" :: "real => real => real"
   12.10    "real_1" > "HOL.one_class.one" :: "real"
   12.11    "real_0" > "HOL.zero_class.zero" :: "real"
    13.1 --- a/src/HOL/Library/sct.ML	Fri Jul 20 14:28:05 2007 +0200
    13.2 +++ b/src/HOL/Library/sct.ML	Fri Jul 20 14:28:25 2007 +0200
    13.3 @@ -63,8 +63,8 @@
    13.4      in Const (nth_const, lT --> HOLogic.natT --> T) $ xs end
    13.5  
    13.6  
    13.7 -val less_nat_const = Const (@{const_name Orderings.less}, HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
    13.8 -val lesseq_nat_const = Const (@{const_name Orderings.less_eq}, HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
    13.9 +val less_nat_const = Const (@{const_name HOL.less}, HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
   13.10 +val lesseq_nat_const = Const (@{const_name HOL.less_eq}, HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
   13.11  
   13.12  val has_edge_simps = [thm "Graphs.has_edge_def", thm "Graphs.dest_graph.simps"]
   13.13  
    14.1 --- a/src/HOL/Orderings.thy	Fri Jul 20 14:28:05 2007 +0200
    14.2 +++ b/src/HOL/Orderings.thy	Fri Jul 20 14:28:25 2007 +0200
    14.3 @@ -6,88 +6,12 @@
    14.4  header {* Syntactic and abstract orders *}
    14.5  
    14.6  theory Orderings
    14.7 -imports HOL
    14.8 +imports Set Fun
    14.9  uses
   14.10    (*"~~/src/Provers/quasi.ML"*)
   14.11    "~~/src/Provers/order.ML"
   14.12  begin
   14.13  
   14.14 -subsection {* Order syntax *}
   14.15 -
   14.16 -class ord = type +
   14.17 -  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<sqsubseteq>" 50)
   14.18 -    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<sqsubset>" 50)
   14.19 -begin
   14.20 -
   14.21 -notation
   14.22 -  less_eq  ("op \<^loc><=") and
   14.23 -  less_eq  ("(_/ \<^loc><= _)" [51, 51] 50) and
   14.24 -  less  ("op \<^loc><") and
   14.25 -  less  ("(_/ \<^loc>< _)"  [51, 51] 50)
   14.26 -  
   14.27 -notation (xsymbols)
   14.28 -  less_eq  ("op \<^loc>\<le>") and
   14.29 -  less_eq  ("(_/ \<^loc>\<le> _)"  [51, 51] 50)
   14.30 -
   14.31 -notation (HTML output)
   14.32 -  less_eq  ("op \<^loc>\<le>") and
   14.33 -  less_eq  ("(_/ \<^loc>\<le> _)"  [51, 51] 50)
   14.34 -
   14.35 -abbreviation (input)
   14.36 -  greater  (infix "\<^loc>>" 50) where
   14.37 -  "x \<^loc>> y \<equiv> y \<^loc>< x"
   14.38 -
   14.39 -abbreviation (input)
   14.40 -  greater_eq  (infix "\<^loc>>=" 50) where
   14.41 -  "x \<^loc>>= y \<equiv> y \<^loc><= x"
   14.42 -
   14.43 -notation (input)
   14.44 -  greater_eq  (infix "\<^loc>\<ge>" 50)
   14.45 -
   14.46 -text {*
   14.47 -  syntactic min/max -- these definitions reach
   14.48 -  their usual semantics in class linorder ahead.
   14.49 -*}
   14.50 -
   14.51 -definition
   14.52 -  min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
   14.53 -  "min a b = (if a \<^loc>\<le> b then a else b)"
   14.54 -
   14.55 -definition
   14.56 -  max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
   14.57 -  "max a b = (if a \<^loc>\<le> b then b else a)"
   14.58 -
   14.59 -end
   14.60 -
   14.61 -notation
   14.62 -  less_eq  ("op <=") and
   14.63 -  less_eq  ("(_/ <= _)" [51, 51] 50) and
   14.64 -  less  ("op <") and
   14.65 -  less  ("(_/ < _)"  [51, 51] 50)
   14.66 -  
   14.67 -notation (xsymbols)
   14.68 -  less_eq  ("op \<le>") and
   14.69 -  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
   14.70 -
   14.71 -notation (HTML output)
   14.72 -  less_eq  ("op \<le>") and
   14.73 -  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
   14.74 -
   14.75 -abbreviation (input)
   14.76 -  greater  (infix ">" 50) where
   14.77 -  "x > y \<equiv> y < x"
   14.78 -
   14.79 -abbreviation (input)
   14.80 -  greater_eq  (infix ">=" 50) where
   14.81 -  "x >= y \<equiv> y <= x"
   14.82 -
   14.83 -notation (input)
   14.84 -  greater_eq  (infix "\<ge>" 50)
   14.85 -
   14.86 -lemmas min_def [code func, code unfold, code inline del] = min_def [folded ord_class.min]
   14.87 -lemmas max_def [code func, code unfold, code inline del] = max_def [folded ord_class.max]
   14.88 -
   14.89 -
   14.90  subsection {* Partial orders *}
   14.91  
   14.92  class order = ord +
   14.93 @@ -265,7 +189,20 @@
   14.94    (simp add: less_le, auto intro: antisym order_trans simp add: linear)
   14.95  
   14.96  
   14.97 -text {* min/max properties *}
   14.98 +text {* min/max *}
   14.99 +
  14.100 +text {* for historic reasons, definitions are done in context ord *}
  14.101 +
  14.102 +definition (in ord)
  14.103 +  min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
  14.104 +  "min a b = (if a \<^loc>\<le> b then a else b)"
  14.105 +
  14.106 +definition (in ord)
  14.107 +  max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
  14.108 +  "max a b = (if a \<^loc>\<le> b then b else a)"
  14.109 +
  14.110 +lemmas (in -) min_def [code func, code unfold, code inline del] = min_def [folded ord_class.min]
  14.111 +lemmas (in -) max_def [code func, code unfold, code inline del] = max_def [folded ord_class.max]
  14.112  
  14.113  lemma min_le_iff_disj:
  14.114    "min x y \<^loc>\<le> z \<longleftrightarrow> x \<^loc>\<le> z \<or> y \<^loc>\<le> z"
  14.115 @@ -370,11 +307,11 @@
  14.116            if of_sort t1
  14.117            then SOME (t1, "=", t2)
  14.118            else NONE
  14.119 -      | dec (Const (@{const_name Orderings.less_eq},  _) $ t1 $ t2) =
  14.120 +      | dec (Const (@{const_name HOL.less_eq},  _) $ t1 $ t2) =
  14.121            if of_sort t1
  14.122            then SOME (t1, "<=", t2)
  14.123            else NONE
  14.124 -      | dec (Const (@{const_name Orderings.less},  _) $ t1 $ t2) =
  14.125 +      | dec (Const (@{const_name HOL.less},  _) $ t1 $ t2) =
  14.126            if of_sort t1
  14.127            then SOME (t1, "<", t2)
  14.128            else NONE
  14.129 @@ -840,7 +777,81 @@
  14.130    unfolding le_bool_def less_bool_def by simp_all
  14.131  
  14.132  
  14.133 -subsection {* Monotonicity, syntactic least value operator and min/max *}
  14.134 +subsection {* Order on sets *}
  14.135 +
  14.136 +instance set :: (type) order
  14.137 +  by (intro_classes,
  14.138 +      (assumption | rule subset_refl subset_trans subset_antisym psubset_eq)+)
  14.139 +
  14.140 +lemmas basic_trans_rules [trans] =
  14.141 +  order_trans_rules set_rev_mp set_mp
  14.142 +
  14.143 +
  14.144 +subsection {* Order on functions *}
  14.145 +
  14.146 +instance "fun" :: (type, ord) ord
  14.147 +  le_fun_def: "f \<le> g \<equiv> \<forall>x. f x \<le> g x"
  14.148 +  less_fun_def: "f < g \<equiv> f \<le> g \<and> f \<noteq> g" ..
  14.149 +
  14.150 +lemmas [code func del] = le_fun_def less_fun_def
  14.151 +
  14.152 +instance "fun" :: (type, order) order
  14.153 +  by default
  14.154 +    (auto simp add: le_fun_def less_fun_def expand_fun_eq
  14.155 +       intro: order_trans order_antisym)
  14.156 +
  14.157 +lemma le_funI: "(\<And>x. f x \<le> g x) \<Longrightarrow> f \<le> g"
  14.158 +  unfolding le_fun_def by simp
  14.159 +
  14.160 +lemma le_funE: "f \<le> g \<Longrightarrow> (f x \<le> g x \<Longrightarrow> P) \<Longrightarrow> P"
  14.161 +  unfolding le_fun_def by simp
  14.162 +
  14.163 +lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
  14.164 +  unfolding le_fun_def by simp
  14.165 +
  14.166 +text {*
  14.167 +  Handy introduction and elimination rules for @{text "\<le>"}
  14.168 +  on unary and binary predicates
  14.169 +*}
  14.170 +
  14.171 +lemma predicate1I [Pure.intro!, intro!]:
  14.172 +  assumes PQ: "\<And>x. P x \<Longrightarrow> Q x"
  14.173 +  shows "P \<le> Q"
  14.174 +  apply (rule le_funI)
  14.175 +  apply (rule le_boolI)
  14.176 +  apply (rule PQ)
  14.177 +  apply assumption
  14.178 +  done
  14.179 +
  14.180 +lemma predicate1D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x \<Longrightarrow> Q x"
  14.181 +  apply (erule le_funE)
  14.182 +  apply (erule le_boolE)
  14.183 +  apply assumption+
  14.184 +  done
  14.185 +
  14.186 +lemma predicate2I [Pure.intro!, intro!]:
  14.187 +  assumes PQ: "\<And>x y. P x y \<Longrightarrow> Q x y"
  14.188 +  shows "P \<le> Q"
  14.189 +  apply (rule le_funI)+
  14.190 +  apply (rule le_boolI)
  14.191 +  apply (rule PQ)
  14.192 +  apply assumption
  14.193 +  done
  14.194 +
  14.195 +lemma predicate2D [Pure.dest, dest]: "P \<le> Q \<Longrightarrow> P x y \<Longrightarrow> Q x y"
  14.196 +  apply (erule le_funE)+
  14.197 +  apply (erule le_boolE)
  14.198 +  apply assumption+
  14.199 +  done
  14.200 +
  14.201 +lemma rev_predicate1D: "P x ==> P <= Q ==> Q x"
  14.202 +  by (rule predicate1D)
  14.203 +
  14.204 +lemma rev_predicate2D: "P x y ==> P <= Q ==> Q x y"
  14.205 +  by (rule predicate2D)
  14.206 +
  14.207 +
  14.208 +subsection {* Monotonicity, least value operator and min/max *}
  14.209  
  14.210  locale mono =
  14.211    fixes f
  14.212 @@ -849,11 +860,6 @@
  14.213  lemmas monoI [intro?] = mono.intro
  14.214    and monoD [dest?] = mono.mono
  14.215  
  14.216 -constdefs
  14.217 -  Least :: "('a::ord => bool) => 'a"               (binder "LEAST " 10)
  14.218 -  "Least P == THE x. P x & (ALL y. P y --> x <= y)"
  14.219 -    -- {* We can no longer use LeastM because the latter requires Hilbert-AC. *}
  14.220 -
  14.221  lemma LeastI2_order:
  14.222    "[| P (x::'a::order);
  14.223        !!y. P y ==> x <= y;
  14.224 @@ -864,6 +870,16 @@
  14.225    apply (blast intro: order_antisym)+
  14.226  done
  14.227  
  14.228 +lemma Least_mono:
  14.229 +  "mono (f::'a::order => 'b::order) ==> EX x:S. ALL y:S. x <= y
  14.230 +    ==> (LEAST y. y : f ` S) = f (LEAST x. x : S)"
  14.231 +    -- {* Courtesy of Stephan Merz *}
  14.232 +  apply clarify
  14.233 +  apply (erule_tac P = "%x. x : S" in LeastI2_order, fast)
  14.234 +  apply (rule LeastI2_order)
  14.235 +  apply (auto elim: monoD intro!: order_antisym)
  14.236 +  done
  14.237 +
  14.238  lemma Least_equality:
  14.239    "[| P (k::'a::order); !!x. P x ==> k <= x |] ==> (LEAST x. P x) = k"
  14.240  apply (simp add: Least_def)
    15.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Fri Jul 20 14:28:05 2007 +0200
    15.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Jul 20 14:28:25 2007 +0200
    15.3 @@ -74,10 +74,10 @@
    15.4  | Const ("op =",ty)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
    15.5  | Const("Not",_) $ (Const ("op =",_)$y$_) => 
    15.6    if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
    15.7 -| Const ("Orderings.ord_class.less",_)$y$z =>
    15.8 +| Const (@{const_name HOL.less}, _) $ y$ z =>
    15.9     if term_of x aconv y then Lt (Thm.dest_arg ct) 
   15.10     else if term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox
   15.11 -| Const ("Orderings.ord_class.less_eq",_)$y$z => 
   15.12 +| Const (@{const_name HOL.less_eq}, _) $ y $ z => 
   15.13     if term_of x aconv y then Le (Thm.dest_arg ct) 
   15.14     else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
   15.15  | Const (@{const_name Divides.dvd},_)$_$(Const(@{const_name "HOL.plus"},_)$y$_) =>
   15.16 @@ -222,10 +222,10 @@
   15.17    end 
   15.18   | _ => addC$(mulC$one$tm)$zero;
   15.19  
   15.20 -fun lin (vs as x::_) (Const("Not",_)$(Const("Orderings.ord_class.less",T)$s$t)) = 
   15.21 -    lin vs (Const("Orderings.ord_class.less_eq",T)$t$s)
   15.22 -  | lin (vs as x::_) (Const("Not",_)$(Const("Orderings.ord_class.less_eq",T)$s$t)) = 
   15.23 -    lin vs (Const("Orderings.ord_class.less",T)$t$s)
   15.24 +fun lin (vs as x::_) (Const("Not", _) $ (Const (@{const_name HOL.less}, T) $ s $ t)) = 
   15.25 +    lin vs (Const(@{const_name HOL.less_eq}, T) $ t $ s)
   15.26 +  | lin (vs as x::_) (Const("Not",_) $ (Const(@{const_name HOL.less_eq}, T) $ s $ t)) = 
   15.27 +    lin vs (Const(@{const_name HOL.less}, T) $ t $ s)
   15.28    | lin vs (Const ("Not",T)$t) = Const ("Not",T)$ (lin vs t)
   15.29    | lin (vs as x::_) (Const(@{const_name Divides.dvd},_)$d$t) = 
   15.30      HOLogic.mk_binrel @{const_name Divides.dvd} (numeral1 abs d, lint vs t)
   15.31 @@ -298,12 +298,12 @@
   15.32    fun h (acc,dacc) t = 
   15.33     case (term_of t) of
   15.34      Const(s,_)$(Const("HOL.times_class.times",_)$c$y)$ _ => 
   15.35 -    if x aconv y 
   15.36 -       andalso s mem ["op =", "Orderings.ord_class.less", "Orderings.ord_class.less_eq"] 
   15.37 +    if x aconv y andalso member (op =)
   15.38 +      ["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s
   15.39      then (ins (dest_numeral c) acc,dacc) else (acc,dacc)
   15.40    | Const(s,_)$_$(Const("HOL.times_class.times",_)$c$y) => 
   15.41 -    if x aconv y 
   15.42 -       andalso s mem ["Orderings.ord_class.less", "Orderings.ord_class.less_eq"] 
   15.43 +    if x aconv y andalso member (op =)
   15.44 +       [@{const_name HOL.less}, @{const_name HOL.less_eq}] s 
   15.45      then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
   15.46    | Const(@{const_name Divides.dvd},_)$_$(Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c$y)$_) => 
   15.47      if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)
   15.48 @@ -338,10 +338,12 @@
   15.49    | Const("op |",_)$_$_ => binop_conv unit_conv t
   15.50    | Const("Not",_)$_ => arg_conv unit_conv t
   15.51    | Const(s,_)$(Const("HOL.times_class.times",_)$c$y)$ _ => 
   15.52 -    if x=y andalso s mem ["op =", "Orderings.ord_class.less", "Orderings.ord_class.less_eq"] 
   15.53 +    if x=y andalso member (op =)
   15.54 +      ["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s
   15.55      then cv (Integer.div l (dest_numeral c)) t else Thm.reflexive t
   15.56    | Const(s,_)$_$(Const("HOL.times_class.times",_)$c$y) => 
   15.57 -    if x=y andalso s mem ["Orderings.ord_class.less", "Orderings.ord_class.less_eq"] 
   15.58 +    if x=y andalso member (op =)
   15.59 +      [@{const_name HOL.less}, @{const_name HOL.less_eq}] s
   15.60      then cv (Integer.div l (dest_numeral c)) t else Thm.reflexive t
   15.61    | Const(@{const_name Divides.dvd},_)$d$(r as (Const("HOL.plus_class.plus",_)$(Const("HOL.times_class.times",_)$c$y)$_)) => 
   15.62      if x=y then 
   15.63 @@ -559,8 +561,8 @@
   15.64  fun qf_of_term ps vs t =  case t
   15.65   of Const("True",_) => T
   15.66    | Const("False",_) => F
   15.67 -  | Const(@{const_name Orderings.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
   15.68 -  | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
   15.69 +  | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
   15.70 +  | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
   15.71    | Const(@{const_name Divides.dvd},_)$t1$t2 => 
   15.72        (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")
   15.73    | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
    16.1 --- a/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Jul 20 14:28:05 2007 +0200
    16.2 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Fri Jul 20 14:28:25 2007 +0200
    16.3 @@ -130,13 +130,13 @@
    16.4  fun mk_cell (thy : theory) solve_tac (vars, prems, lhs, rhs) mfun =
    16.5      let
    16.6        val goals = mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
    16.7 -      val less_thm = goals "Orderings.ord_class.less" |> prove thy solve_tac
    16.8 +      val less_thm = goals @{const_name HOL.less} |> prove thy solve_tac
    16.9      in
   16.10        if Thm.no_prems less_thm then
   16.11          Less (Goal.finish less_thm)
   16.12        else
   16.13          let
   16.14 -          val lesseq_thm = goals "Orderings.ord_class.less_eq" |> prove thy solve_tac
   16.15 +          val lesseq_thm = goals @{const_name HOL.less_eq} |> prove thy solve_tac
   16.16          in
   16.17            if Thm.no_prems lesseq_thm then
   16.18              LessEq (Goal.finish lesseq_thm, less_thm)
    17.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Jul 20 14:28:05 2007 +0200
    17.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Jul 20 14:28:25 2007 +0200
    17.3 @@ -181,7 +181,7 @@
    17.4      case concl of
    17.5        Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
    17.6      | _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
    17.7 -    | _ $ (Const ("Orderings.ord_class.less_eq", _) $ _ $ _) =>
    17.8 +    | _ $ (Const ("HOL.ord_class.less_eq", _) $ _ $ _) =>
    17.9        [dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
   17.10           (resolve_tac [le_funI, le_boolI'])) thm))]
   17.11      | _ => [thm]
   17.12 @@ -554,7 +554,7 @@
   17.13           (make_bool_args HOLogic.mk_not I bs i)) preds));
   17.14  
   17.15      val ind_concl = HOLogic.mk_Trueprop
   17.16 -      (HOLogic.mk_binrel "Orderings.ord_class.less_eq" (rec_const, ind_pred));
   17.17 +      (HOLogic.mk_binrel "HOL.ord_class.less_eq" (rec_const, ind_pred));
   17.18  
   17.19      val raw_fp_induct = (mono RS (fp_def RS def_lfp_induct));
   17.20  
    18.1 --- a/src/HOL/Tools/refute.ML	Fri Jul 20 14:28:05 2007 +0200
    18.2 +++ b/src/HOL/Tools/refute.ML	Fri Jul 20 14:28:25 2007 +0200
    18.3 @@ -696,7 +696,7 @@
    18.4        | Const ("Finite_Set.card", _)    => t
    18.5        | Const ("Finite_Set.Finites", _) => t
    18.6        | Const ("Finite_Set.finite", _)  => t
    18.7 -      | Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
    18.8 +      | Const (@{const_name HOL.less}, Type ("fun", [Type ("nat", []),
    18.9          Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t
   18.10        | Const (@{const_name HOL.plus}, Type ("fun", [Type ("nat", []),
   18.11          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
   18.12 @@ -883,7 +883,7 @@
   18.13        | Const ("Finite_Set.card", T)    => collect_type_axioms (axs, T)
   18.14        | Const ("Finite_Set.Finites", T) => collect_type_axioms (axs, T)
   18.15        | Const ("Finite_Set.finite", T)  => collect_type_axioms (axs, T)
   18.16 -      | Const (@{const_name Orderings.less}, T as Type ("fun", [Type ("nat", []),
   18.17 +      | Const (@{const_name HOL.less}, T as Type ("fun", [Type ("nat", []),
   18.18          Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
   18.19            collect_type_axioms (axs, T)
   18.20        | Const (@{const_name HOL.plus}, T as Type ("fun", [Type ("nat", []),
   18.21 @@ -2602,13 +2602,13 @@
   18.22    (* theory -> model -> arguments -> Term.term ->
   18.23      (interpretation * model * arguments) option *)
   18.24  
   18.25 -  (* only an optimization: 'Orderings.less' could in principle be            *)
   18.26 +  (* only an optimization: 'HOL.less' could in principle be            *)
   18.27    (* interpreted with interpreters available already (using its definition), *)
   18.28    (* but the code below is more efficient                                    *)
   18.29  
   18.30    fun Nat_less_interpreter thy model args t =
   18.31      case t of
   18.32 -      Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
   18.33 +      Const (@{const_name HOL.less}, Type ("fun", [Type ("nat", []),
   18.34          Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
   18.35        let
   18.36          val (i_nat, _, _) = interpret thy model
    19.1 --- a/src/HOL/Tools/res_clause.ML	Fri Jul 20 14:28:05 2007 +0200
    19.2 +++ b/src/HOL/Tools/res_clause.ML	Fri Jul 20 14:28:25 2007 +0200
    19.3 @@ -89,8 +89,8 @@
    19.4  (*Provide readable names for the more common symbolic functions*)
    19.5  val const_trans_table =
    19.6        Symtab.make [("op =", "equal"),
    19.7 -	  	   (@{const_name Orderings.less_eq}, "lessequals"),
    19.8 -		   (@{const_name Orderings.less}, "less"),
    19.9 +	  	   (@{const_name HOL.less_eq}, "lessequals"),
   19.10 +		   (@{const_name HOL.less}, "less"),
   19.11  		   ("op &", "and"),
   19.12  		   ("op |", "or"),
   19.13  		   (@{const_name HOL.plus}, "plus"),
    20.1 --- a/src/HOL/arith_data.ML	Fri Jul 20 14:28:05 2007 +0200
    20.2 +++ b/src/HOL/arith_data.ML	Fri Jul 20 14:28:25 2007 +0200
    20.3 @@ -107,8 +107,8 @@
    20.4  structure LessCancelSums = CancelSumsFun
    20.5  (struct
    20.6    open Sum;
    20.7 -  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less};
    20.8 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT;
    20.9 +  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less};
   20.10 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT;
   20.11    val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
   20.12  end);
   20.13  
   20.14 @@ -117,8 +117,8 @@
   20.15  structure LeCancelSums = CancelSumsFun
   20.16  (struct
   20.17    open Sum;
   20.18 -  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq};
   20.19 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT;
   20.20 +  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq};
   20.21 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT;
   20.22    val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
   20.23  end);
   20.24  
   20.25 @@ -370,8 +370,8 @@
   20.26    val (q, j) = poly (rhs, Rat.one, ([], Rat.zero))
   20.27  in
   20.28    case rel of
   20.29 -    @{const_name Orderings.less}    => SOME (p, i, "<", q, j)
   20.30 -  | @{const_name Orderings.less_eq} => SOME (p, i, "<=", q, j)
   20.31 +    @{const_name HOL.less}    => SOME (p, i, "<", q, j)
   20.32 +  | @{const_name HOL.less_eq} => SOME (p, i, "<=", q, j)
   20.33    | "op ="              => SOME (p, i, "=", q, j)
   20.34    | _                   => NONE
   20.35  end handle Zero => NONE;
   20.36 @@ -523,7 +523,7 @@
   20.37          val rev_terms     = rev terms
   20.38          val terms1        = map (subst_term [(split_term, t1)]) rev_terms
   20.39          val terms2        = map (subst_term [(split_term, t2)]) rev_terms
   20.40 -        val t1_leq_t2     = Const (@{const_name Orderings.less_eq},
   20.41 +        val t1_leq_t2     = Const (@{const_name HOL.less_eq},
   20.42                                      split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
   20.43          val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
   20.44          val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   20.45 @@ -538,7 +538,7 @@
   20.46          val rev_terms     = rev terms
   20.47          val terms1        = map (subst_term [(split_term, t1)]) rev_terms
   20.48          val terms2        = map (subst_term [(split_term, t2)]) rev_terms
   20.49 -        val t1_leq_t2     = Const (@{const_name Orderings.less_eq},
   20.50 +        val t1_leq_t2     = Const (@{const_name HOL.less_eq},
   20.51                                      split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
   20.52          val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
   20.53          val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   20.54 @@ -555,9 +555,9 @@
   20.55          val terms2      = map (subst_term [(split_term, Const (@{const_name HOL.uminus},
   20.56                              split_type --> split_type) $ t1)]) rev_terms
   20.57          val zero        = Const (@{const_name HOL.zero}, split_type)
   20.58 -        val zero_leq_t1 = Const (@{const_name Orderings.less_eq},
   20.59 +        val zero_leq_t1 = Const (@{const_name HOL.less_eq},
   20.60                              split_type --> split_type --> HOLogic.boolT) $ zero $ t1
   20.61 -        val t1_lt_zero  = Const (@{const_name Orderings.less},
   20.62 +        val t1_lt_zero  = Const (@{const_name HOL.less},
   20.63                              split_type --> split_type --> HOLogic.boolT) $ t1 $ zero
   20.64          val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   20.65          val subgoal1    = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false]
   20.66 @@ -578,7 +578,7 @@
   20.67                                  (map (incr_boundvars 1) rev_terms)
   20.68          val t1'             = incr_boundvars 1 t1
   20.69          val t2'             = incr_boundvars 1 t2
   20.70 -        val t1_lt_t2        = Const (@{const_name Orderings.less},
   20.71 +        val t1_lt_t2        = Const (@{const_name HOL.less},
   20.72                                  split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
   20.73          val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
   20.74                                  (Const (@{const_name HOL.plus},
   20.75 @@ -602,7 +602,7 @@
   20.76          val t1'         = incr_boundvars 1 t1
   20.77          val t1_eq_int_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
   20.78                              (Const ("Nat.of_nat", HOLogic.natT --> HOLogic.intT) $ n)
   20.79 -        val t1_lt_zero  = Const (@{const_name Orderings.less},
   20.80 +        val t1_lt_zero  = Const (@{const_name HOL.less},
   20.81                              HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
   20.82          val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   20.83          val subgoal1    = (HOLogic.mk_Trueprop t1_eq_int_n) :: terms1 @ [not_false]
   20.84 @@ -628,7 +628,7 @@
   20.85                                          split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
   20.86          val t2_neq_zero             = HOLogic.mk_not (Const ("op =",
   20.87                                          split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
   20.88 -        val j_lt_t2                 = Const (@{const_name Orderings.less},
   20.89 +        val j_lt_t2                 = Const (@{const_name HOL.less},
   20.90                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
   20.91          val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
   20.92                                         (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
   20.93 @@ -660,7 +660,7 @@
   20.94                                          split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
   20.95          val t2_neq_zero             = HOLogic.mk_not (Const ("op =",
   20.96                                          split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
   20.97 -        val j_lt_t2                 = Const (@{const_name Orderings.less},
   20.98 +        val j_lt_t2                 = Const (@{const_name HOL.less},
   20.99                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
  20.100          val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
  20.101                                         (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
  20.102 @@ -697,18 +697,18 @@
  20.103                                          (number_of $
  20.104                                            (Const (@{const_name HOL.uminus},
  20.105                                              HOLogic.intT --> HOLogic.intT) $ k'))
  20.106 -        val zero_leq_j              = Const (@{const_name Orderings.less_eq},
  20.107 +        val zero_leq_j              = Const (@{const_name HOL.less_eq},
  20.108                                          split_type --> split_type --> HOLogic.boolT) $ zero $ j
  20.109 -        val j_lt_t2                 = Const (@{const_name Orderings.less},
  20.110 +        val j_lt_t2                 = Const (@{const_name HOL.less},
  20.111                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
  20.112          val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
  20.113                                         (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
  20.114                                           (Const (@{const_name HOL.times},
  20.115                                             split_type --> split_type --> split_type) $ t2' $ i) $ j)
  20.116          val neg_t2                  = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
  20.117 -        val t2_lt_j                 = Const (@{const_name Orderings.less},
  20.118 +        val t2_lt_j                 = Const (@{const_name HOL.less},
  20.119                                          split_type --> split_type--> HOLogic.boolT) $ t2' $ j
  20.120 -        val j_leq_zero              = Const (@{const_name Orderings.less_eq},
  20.121 +        val j_leq_zero              = Const (@{const_name HOL.less_eq},
  20.122                                          split_type --> split_type --> HOLogic.boolT) $ j $ zero
  20.123          val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
  20.124          val subgoal1                = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
  20.125 @@ -749,9 +749,9 @@
  20.126                                          (number_of $
  20.127                                            (Const (@{const_name HOL.uminus},
  20.128                                              HOLogic.intT --> HOLogic.intT) $ k'))
  20.129 -        val zero_leq_j              = Const (@{const_name Orderings.less_eq},
  20.130 +        val zero_leq_j              = Const (@{const_name HOL.less_eq},
  20.131                                          split_type --> split_type --> HOLogic.boolT) $ zero $ j
  20.132 -        val j_lt_t2                 = Const (@{const_name Orderings.less},
  20.133 +        val j_lt_t2                 = Const (@{const_name HOL.less},
  20.134                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
  20.135          val t1_eq_t2_times_i_plus_j = Const ("op =",
  20.136                                          split_type --> split_type --> HOLogic.boolT) $ t1' $
  20.137 @@ -759,9 +759,9 @@
  20.138                                           (Const (@{const_name HOL.times},
  20.139                                             split_type --> split_type --> split_type) $ t2' $ i) $ j)
  20.140          val neg_t2                  = Const ("IntDef.neg", split_type --> HOLogic.boolT) $ t2'
  20.141 -        val t2_lt_j                 = Const (@{const_name Orderings.less},
  20.142 +        val t2_lt_j                 = Const (@{const_name HOL.less},
  20.143                                          split_type --> split_type--> HOLogic.boolT) $ t2' $ j
  20.144 -        val j_leq_zero              = Const (@{const_name Orderings.less_eq},
  20.145 +        val j_leq_zero              = Const (@{const_name HOL.less_eq},
  20.146                                          split_type --> split_type --> HOLogic.boolT) $ j $ zero
  20.147          val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
  20.148          val subgoal1                = (HOLogic.mk_Trueprop iszero_t2) :: terms1 @ [not_false]
  20.149 @@ -1011,24 +1011,24 @@
  20.150      val r = #prop(rep_thm thm);
  20.151    in
  20.152      case r of
  20.153 -      Tr $ ((c as Const(@{const_name Orderings.less_eq},T)) $ s $ t) =>
  20.154 +      Tr $ ((c as Const(@{const_name HOL.less_eq},T)) $ s $ t) =>
  20.155          let val r' = Tr $ (c $ t $ s)
  20.156          in
  20.157            case Library.find_first (prp r') prems of
  20.158              NONE =>
  20.159 -              let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name Orderings.less},T) $ s $ t))
  20.160 +              let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name HOL.less},T) $ s $ t))
  20.161                in case Library.find_first (prp r') prems of
  20.162                     NONE => []
  20.163                   | SOME thm' => [(thm' RS not_lessD) RS (thm RS antisym)]
  20.164                end
  20.165            | SOME thm' => [thm' RS (thm RS antisym)]
  20.166          end
  20.167 -    | Tr $ (Const("Not",_) $ (Const(@{const_name Orderings.less},T) $ s $ t)) =>
  20.168 -        let val r' = Tr $ (Const(@{const_name Orderings.less_eq},T) $ s $ t)
  20.169 +    | Tr $ (Const("Not",_) $ (Const(@{const_name HOL.less},T) $ s $ t)) =>
  20.170 +        let val r' = Tr $ (Const(@{const_name HOL.less_eq},T) $ s $ t)
  20.171          in
  20.172            case Library.find_first (prp r') prems of
  20.173              NONE =>
  20.174 -              let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name Orderings.less},T) $ t $ s))
  20.175 +              let val r' = Tr $ (HOLogic.Not $ (Const(@{const_name HOL.less},T) $ t $ s))
  20.176                in case Library.find_first (prp r') prems of
  20.177                     NONE => []
  20.178                   | SOME thm' =>
    21.1 --- a/src/HOL/ex/coopereif.ML	Fri Jul 20 14:28:05 2007 +0200
    21.2 +++ b/src/HOL/ex/coopereif.ML	Fri Jul 20 14:28:25 2007 +0200
    21.3 @@ -32,8 +32,8 @@
    21.4  fun qf_of_term ps vs t = case t
    21.5       of Const("True",_) => T
    21.6        | Const("False",_) => F
    21.7 -      | Const(@{const_name "Orderings.less"},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
    21.8 -      | Const(@{const_name "Orderings.less_eq"},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
    21.9 +      | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
   21.10 +      | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
   21.11        | Const(@{const_name "Divides.dvd"},_)$t1$t2 => 
   21.12            (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => error "qf_of_term: unsupported dvd")
   21.13        | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
    22.1 --- a/src/HOL/ex/svc_funcs.ML	Fri Jul 20 14:28:05 2007 +0200
    22.2 +++ b/src/HOL/ex/svc_funcs.ML	Fri Jul 20 14:28:25 2007 +0200
    22.3 @@ -112,8 +112,8 @@
    22.4                           b1 orelse b2)
    22.5                       end
    22.6                   else (*might be numeric equality*) (t, is_intnat T)
    22.7 -           | Const(@{const_name Orderings.less}, Type ("fun", [T,_]))  => (t, is_intnat T)
    22.8 -           | Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) => (t, is_intnat T)
    22.9 +           | Const(@{const_name HOL.less}, Type ("fun", [T,_]))  => (t, is_intnat T)
   22.10 +           | Const(@{const_name HOL.less_eq}, Type ("fun", [T,_])) => (t, is_intnat T)
   22.11             | _ => (t, false)
   22.12           end
   22.13     in #1 o tag end;
   22.14 @@ -216,13 +216,13 @@
   22.15                     else fail t
   22.16              end
   22.17          (*inequalities: possible types are nat, int, real*)
   22.18 -      | fm pos (t as Const(@{const_name Orderings.less},  Type ("fun", [T,_])) $ x $ y) =
   22.19 +      | fm pos (t as Const(@{const_name HOL.less},  Type ("fun", [T,_])) $ x $ y) =
   22.20              if not pos orelse T = HOLogic.realT then
   22.21                  Buildin("<", [tm x, tm y])
   22.22              else if is_intnat T then
   22.23                  Buildin("<=", [suc (tm x), tm y])
   22.24              else fail t
   22.25 -      | fm pos (t as Const(@{const_name Orderings.less_eq},  Type ("fun", [T,_])) $ x $ y) =
   22.26 +      | fm pos (t as Const(@{const_name HOL.less_eq},  Type ("fun", [T,_])) $ x $ y) =
   22.27              if pos orelse T = HOLogic.realT then
   22.28                  Buildin("<=", [tm x, tm y])
   22.29              else if is_intnat T then
    23.1 --- a/src/HOL/ex/svc_oracle.ML	Fri Jul 20 14:28:05 2007 +0200
    23.2 +++ b/src/HOL/ex/svc_oracle.ML	Fri Jul 20 14:28:25 2007 +0200
    23.3 @@ -78,8 +78,8 @@
    23.4        | fm ((c as Const("True", _))) = c
    23.5        | fm ((c as Const("False", _))) = c
    23.6        | fm (t as Const("op =",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    23.7 -      | fm (t as Const(@{const_name Orderings.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    23.8 -      | fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    23.9 +      | fm (t as Const(@{const_name HOL.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
   23.10 +      | fm (t as Const(@{const_name HOL.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
   23.11        | fm t = replace t
   23.12      (*entry point, and abstraction of a meta-formula*)
   23.13      fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
    24.1 --- a/src/HOL/int_arith1.ML	Fri Jul 20 14:28:05 2007 +0200
    24.2 +++ b/src/HOL/int_arith1.ML	Fri Jul 20 14:28:25 2007 +0200
    24.3 @@ -110,8 +110,8 @@
    24.4        mk_meta_eq ([f_eq, f_number_of_eq] MRS trans)
    24.5  
    24.6    (*reorientation simprules using ==, for the following simproc*)
    24.7 -  val meta_zero_reorient = zero_reorient RS eq_reflection
    24.8 -  val meta_one_reorient = one_reorient RS eq_reflection
    24.9 +  val meta_zero_reorient = @{thm zero_reorient} RS eq_reflection
   24.10 +  val meta_one_reorient = @{thm one_reorient} RS eq_reflection
   24.11    val meta_number_of_reorient = number_of_reorient RS eq_reflection
   24.12  
   24.13    (*reorientation simplification procedure: reorients (polymorphic) 
   24.14 @@ -350,9 +350,9 @@
   24.15    val trans_tac         = fn _ => trans_tac
   24.16  
   24.17    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
   24.18 -    diff_simps @ minus_simps @ add_ac
   24.19 +    diff_simps @ minus_simps @ @{thms add_ac}
   24.20    val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
   24.21 -  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ add_ac @ mult_ac
   24.22 +  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
   24.23    fun norm_tac ss =
   24.24      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   24.25      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   24.26 @@ -376,8 +376,8 @@
   24.27  structure LessCancelNumerals = CancelNumeralsFun
   24.28   (open CancelNumeralsCommon
   24.29    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   24.30 -  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   24.31 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
   24.32 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   24.33 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
   24.34    val bal_add1 = less_add_iff1 RS trans
   24.35    val bal_add2 = less_add_iff2 RS trans
   24.36  );
   24.37 @@ -385,8 +385,8 @@
   24.38  structure LeCancelNumerals = CancelNumeralsFun
   24.39   (open CancelNumeralsCommon
   24.40    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   24.41 -  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   24.42 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
   24.43 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   24.44 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
   24.45    val bal_add1 = le_add_iff1 RS trans
   24.46    val bal_add2 = le_add_iff2 RS trans
   24.47  );
   24.48 @@ -433,9 +433,9 @@
   24.49    val trans_tac         = fn _ => trans_tac
   24.50  
   24.51    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
   24.52 -    diff_simps @ minus_simps @ add_ac
   24.53 +    diff_simps @ minus_simps @ @{thms add_ac}
   24.54    val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
   24.55 -  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ add_ac @ mult_ac
   24.56 +  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
   24.57    fun norm_tac ss =
   24.58      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   24.59      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   24.60 @@ -463,9 +463,9 @@
   24.61    val trans_tac         = fn _ => trans_tac
   24.62  
   24.63    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
   24.64 -    inverse_1s @ divide_simps @ diff_simps @ minus_simps @ add_ac
   24.65 +    inverse_1s @ divide_simps @ diff_simps @ minus_simps @ @{thms add_ac}
   24.66    val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
   24.67 -  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ add_ac @ mult_ac
   24.68 +  val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac}
   24.69    fun norm_tac ss =
   24.70      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   24.71      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   24.72 @@ -541,7 +541,7 @@
   24.73  
   24.74  structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
   24.75  struct
   24.76 -  val assoc_ss = HOL_ss addsimps mult_ac
   24.77 +  val assoc_ss = HOL_ss addsimps @{thms mult_ac}
   24.78    val eq_reflection = eq_reflection
   24.79  end;
   24.80  
    25.1 --- a/src/HOL/int_factor_simprocs.ML	Fri Jul 20 14:28:05 2007 +0200
    25.2 +++ b/src/HOL/int_factor_simprocs.ML	Fri Jul 20 14:28:25 2007 +0200
    25.3 @@ -33,7 +33,7 @@
    25.4  
    25.5    val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
    25.6    val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
    25.7 -  val norm_ss3 = HOL_ss addsimps mult_ac
    25.8 +  val norm_ss3 = HOL_ss addsimps @{thms mult_ac}
    25.9    fun norm_tac ss =
   25.10      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   25.11      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   25.12 @@ -78,8 +78,8 @@
   25.13  structure LessCancelNumeralFactor = CancelNumeralFactorFun
   25.14   (open CancelNumeralFactorCommon
   25.15    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   25.16 -  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   25.17 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
   25.18 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   25.19 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
   25.20    val cancel = @{thm mult_less_cancel_left} RS trans
   25.21    val neg_exchanges = true
   25.22  )
   25.23 @@ -87,8 +87,8 @@
   25.24  structure LeCancelNumeralFactor = CancelNumeralFactorFun
   25.25   (open CancelNumeralFactorCommon
   25.26    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   25.27 -  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   25.28 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
   25.29 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   25.30 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
   25.31    val cancel = @{thm mult_le_cancel_left} RS trans
   25.32    val neg_exchanges = true
   25.33  )
   25.34 @@ -216,7 +216,7 @@
   25.35  
   25.36  (** Final simplification for the CancelFactor simprocs **)
   25.37  val simplify_one = Int_Numeral_Simprocs.simplify_meta_eq  
   25.38 -  [@{thm mult_1_left}, mult_1_right, @{thm zdiv_1}, numeral_1_eq_1];
   25.39 +  [@{thm mult_1_left}, @{thm mult_1_right}, @{thm zdiv_1}, numeral_1_eq_1];
   25.40  
   25.41  fun cancel_simplify_meta_eq cancel_th ss th =
   25.42      simplify_one ss (([th, cancel_th]) MRS trans);
   25.43 @@ -229,7 +229,7 @@
   25.44    val dest_coeff        = dest_coeff
   25.45    val find_first        = find_first_t []
   25.46    val trans_tac         = fn _ => trans_tac
   25.47 -  val norm_ss = HOL_ss addsimps mult_1s @ mult_ac
   25.48 +  val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   25.49    fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   25.50    end;
   25.51  
    26.1 --- a/src/HOL/nat_simprocs.ML	Fri Jul 20 14:28:05 2007 +0200
    26.2 +++ b/src/HOL/nat_simprocs.ML	Fri Jul 20 14:28:25 2007 +0200
    26.3 @@ -125,15 +125,15 @@
    26.4  
    26.5  
    26.6  (*Simplify 1*n and n*1 to n*)
    26.7 -val add_0s  = map rename_numerals [add_0, add_0_right];
    26.8 +val add_0s  = map rename_numerals [@{thm add_0}, @{thm add_0_right}];
    26.9  val mult_1s = map rename_numerals [@{thm nat_mult_1}, @{thm nat_mult_1_right}];
   26.10  
   26.11  (*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
   26.12  
   26.13  (*And these help the simproc return False when appropriate, which helps
   26.14    the arith prover.*)
   26.15 -val contra_rules = [add_Suc, add_Suc_right, Zero_not_Suc, Suc_not_Zero,
   26.16 -                    le_0_eq];
   26.17 +val contra_rules = [@{thm add_Suc}, @{thm add_Suc_right}, @{thm Zero_not_Suc},
   26.18 +  @{thm Suc_not_Zero}, @{thm le_0_eq}];
   26.19  
   26.20  val simplify_meta_eq =
   26.21      Int_Numeral_Simprocs.simplify_meta_eq
   26.22 @@ -157,8 +157,8 @@
   26.23    val trans_tac         = fn _ => trans_tac
   26.24  
   26.25    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
   26.26 -    [@{thm Suc_eq_add_numeral_1_left}] @ add_ac
   26.27 -  val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac
   26.28 +    [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
   26.29 +  val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   26.30    fun norm_tac ss = 
   26.31      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   26.32      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   26.33 @@ -181,8 +181,8 @@
   26.34  structure LessCancelNumerals = CancelNumeralsFun
   26.35   (open CancelNumeralsCommon
   26.36    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   26.37 -  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   26.38 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
   26.39 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   26.40 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
   26.41    val bal_add1 = @{thm nat_less_add_iff1} RS trans
   26.42    val bal_add2 = @{thm nat_less_add_iff2} RS trans
   26.43  );
   26.44 @@ -190,8 +190,8 @@
   26.45  structure LeCancelNumerals = CancelNumeralsFun
   26.46   (open CancelNumeralsCommon
   26.47    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   26.48 -  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   26.49 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
   26.50 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   26.51 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
   26.52    val bal_add1 = @{thm nat_le_add_iff1} RS trans
   26.53    val bal_add2 = @{thm nat_le_add_iff2} RS trans
   26.54  );
   26.55 @@ -245,8 +245,8 @@
   26.56    val prove_conv        = Int_Numeral_Base_Simprocs.prove_conv_nohyps
   26.57    val trans_tac         = fn _ => trans_tac
   26.58  
   26.59 -  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ add_ac
   26.60 -  val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac
   26.61 +  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
   26.62 +  val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   26.63    fun norm_tac ss =
   26.64      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   26.65      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   26.66 @@ -271,8 +271,8 @@
   26.67    val trans_tac         = fn _ => trans_tac
   26.68  
   26.69    val norm_ss1 = num_ss addsimps
   26.70 -    numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ add_ac
   26.71 -  val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac
   26.72 +    numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
   26.73 +  val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   26.74    fun norm_tac ss =
   26.75      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   26.76      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   26.77 @@ -303,8 +303,8 @@
   26.78  structure LessCancelNumeralFactor = CancelNumeralFactorFun
   26.79   (open CancelNumeralFactorCommon
   26.80    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   26.81 -  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   26.82 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
   26.83 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   26.84 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
   26.85    val cancel = @{thm nat_mult_less_cancel1} RS trans
   26.86    val neg_exchanges = true
   26.87  )
   26.88 @@ -312,8 +312,8 @@
   26.89  structure LeCancelNumeralFactor = CancelNumeralFactorFun
   26.90   (open CancelNumeralFactorCommon
   26.91    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   26.92 -  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   26.93 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
   26.94 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   26.95 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
   26.96    val cancel = @{thm nat_mult_le_cancel1} RS trans
   26.97    val neg_exchanges = true
   26.98  )
   26.99 @@ -363,7 +363,7 @@
  26.100    val dest_coeff        = dest_coeff
  26.101    val find_first        = find_first_t []
  26.102    val trans_tac         = fn _ => trans_tac
  26.103 -  val norm_ss = HOL_ss addsimps mult_1s @ mult_ac
  26.104 +  val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
  26.105    fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
  26.106    end;
  26.107  
  26.108 @@ -378,16 +378,16 @@
  26.109  structure LessCancelFactor = ExtractCommonTermFun
  26.110   (open CancelFactorCommon
  26.111    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  26.112 -  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
  26.113 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
  26.114 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
  26.115 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
  26.116    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_less_cancel_disj}
  26.117  );
  26.118  
  26.119  structure LeCancelFactor = ExtractCommonTermFun
  26.120   (open CancelFactorCommon
  26.121    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  26.122 -  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
  26.123 -  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
  26.124 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
  26.125 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
  26.126    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_le_cancel_disj}
  26.127  );
  26.128