merged
authorhaftmann
Wed Feb 10 14:12:40 2010 +0100 (2010-02-10)
changeset 35094a0e89e47b083
parent 35089 17b7940f43e4
parent 35093 5acba118b02a
child 35095 6cdf9bbd0342
merged
src/HOL/Library/Structure_Syntax.thy
     1.1 --- a/NEWS	Wed Feb 10 12:04:57 2010 +0100
     1.2 +++ b/NEWS	Wed Feb 10 14:12:40 2010 +0100
     1.3 @@ -22,6 +22,8 @@
     1.4  
     1.5  * Some generic constants have been put to appropriate theories:
     1.6  
     1.7 +    less_eq, less: Orderings
     1.8 +    abs, sgn: Groups
     1.9      inverse, divide: Rings
    1.10  
    1.11  INCOMPATIBILITY.
    1.12 @@ -80,13 +82,9 @@
    1.13  
    1.14  INCOMPATIBILITY.
    1.15  
    1.16 -* Index syntax for structures must be imported explicitly from library
    1.17 -theory Structure_Syntax.  INCOMPATIBILITY.
    1.18 -
    1.19  * New theory Algebras contains generic algebraic structures and
    1.20  generic algebraic operations.  INCOMPATIBILTY: constants zero, one,
    1.21 -plus, minus, uminus, times, abs, sgn, less_eq and
    1.22 -less have been moved from HOL.thy to Algebras.thy.
    1.23 +plus, minus, uminus and times have been moved from HOL.thy to Algebras.thy.
    1.24  
    1.25  * HOLogic.strip_psplit: types are returned in syntactic order, similar
    1.26  to other strip and tuple operations.  INCOMPATIBILITY.
     2.1 --- a/src/HOL/Algebras.thy	Wed Feb 10 12:04:57 2010 +0100
     2.2 +++ b/src/HOL/Algebras.thy	Wed Feb 10 14:12:40 2010 +0100
     2.3 @@ -55,7 +55,7 @@
     2.4  end
     2.5  
     2.6  
     2.7 -subsection {* Generic algebraic operations *}
     2.8 +subsection {* Generic syntactic operations *}
     2.9  
    2.10  class zero = 
    2.11    fixes zero :: 'a  ("0")
    2.12 @@ -63,6 +63,13 @@
    2.13  class one =
    2.14    fixes one  :: 'a  ("1")
    2.15  
    2.16 +hide (open) const zero one
    2.17 +
    2.18 +syntax
    2.19 +  "_index1"  :: index    ("\<^sub>1")
    2.20 +translations
    2.21 +  (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
    2.22 +
    2.23  lemma Let_0 [simp]: "Let 0 f = f 0"
    2.24    unfolding Let_def ..
    2.25  
    2.26 @@ -89,8 +96,6 @@
    2.27  in map tr' [@{const_syntax Algebras.one}, @{const_syntax Algebras.zero}] end;
    2.28  *} -- {* show types that are presumably too general *}
    2.29  
    2.30 -hide (open) const zero one
    2.31 -
    2.32  class plus =
    2.33    fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
    2.34  
    2.35 @@ -103,51 +108,4 @@
    2.36  class times =
    2.37    fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
    2.38  
    2.39 -class abs =
    2.40 -  fixes abs :: "'a \<Rightarrow> 'a"
    2.41 -begin
    2.42 -
    2.43 -notation (xsymbols)
    2.44 -  abs  ("\<bar>_\<bar>")
    2.45 -
    2.46 -notation (HTML output)
    2.47 -  abs  ("\<bar>_\<bar>")
    2.48 -
    2.49 -end
    2.50 -
    2.51 -class sgn =
    2.52 -  fixes sgn :: "'a \<Rightarrow> 'a"
    2.53 -
    2.54 -class ord =
    2.55 -  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    2.56 -    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    2.57 -begin
    2.58 -
    2.59 -notation
    2.60 -  less_eq  ("op <=") and
    2.61 -  less_eq  ("(_/ <= _)" [51, 51] 50) and
    2.62 -  less  ("op <") and
    2.63 -  less  ("(_/ < _)"  [51, 51] 50)
    2.64 -  
    2.65 -notation (xsymbols)
    2.66 -  less_eq  ("op \<le>") and
    2.67 -  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
    2.68 -
    2.69 -notation (HTML output)
    2.70 -  less_eq  ("op \<le>") and
    2.71 -  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
    2.72 -
    2.73 -abbreviation (input)
    2.74 -  greater_eq  (infix ">=" 50) where
    2.75 -  "x >= y \<equiv> y <= x"
    2.76 -
    2.77 -notation (input)
    2.78 -  greater_eq  (infix "\<ge>" 50)
    2.79 -
    2.80 -abbreviation (input)
    2.81 -  greater  (infix ">" 50) where
    2.82 -  "x > y \<equiv> y < x"
    2.83 -
    2.84 -end
    2.85 -
    2.86  end
    2.87 \ No newline at end of file
     3.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Feb 10 12:04:57 2010 +0100
     3.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Feb 10 14:12:40 2010 +0100
     3.3 @@ -684,7 +684,7 @@
     3.4  fun xnormalize_conv ctxt [] ct = reflexive ct
     3.5  | xnormalize_conv ctxt (vs as (x::_)) ct =
     3.6     case term_of ct of
     3.7 -   Const(@{const_name Algebras.less},_)$_$Const(@{const_name Algebras.zero},_) =>
     3.8 +   Const(@{const_name Orderings.less},_)$_$Const(@{const_name Algebras.zero},_) =>
     3.9      (case whatis x (Thm.dest_arg1 ct) of
    3.10      ("c*x+t",[c,t]) =>
    3.11         let
    3.12 @@ -727,7 +727,7 @@
    3.13      | _ => reflexive ct)
    3.14  
    3.15  
    3.16 -|  Const(@{const_name Algebras.less_eq},_)$_$Const(@{const_name Algebras.zero},_) =>
    3.17 +|  Const(@{const_name Orderings.less_eq},_)$_$Const(@{const_name Algebras.zero},_) =>
    3.18     (case whatis x (Thm.dest_arg1 ct) of
    3.19      ("c*x+t",[c,t]) =>
    3.20         let
    3.21 @@ -816,7 +816,7 @@
    3.22    val eq_iff_diff_eq_0 = mk_meta_eq @{thm "eq_iff_diff_eq_0"}
    3.23  in
    3.24  fun field_isolate_conv phi ctxt vs ct = case term_of ct of
    3.25 -  Const(@{const_name Algebras.less},_)$a$b =>
    3.26 +  Const(@{const_name Orderings.less},_)$a$b =>
    3.27     let val (ca,cb) = Thm.dest_binop ct
    3.28         val T = ctyp_of_term ca
    3.29         val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
    3.30 @@ -825,7 +825,7 @@
    3.31                (Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
    3.32         val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    3.33     in rth end
    3.34 -| Const(@{const_name Algebras.less_eq},_)$a$b =>
    3.35 +| Const(@{const_name Orderings.less_eq},_)$a$b =>
    3.36     let val (ca,cb) = Thm.dest_binop ct
    3.37         val T = ctyp_of_term ca
    3.38         val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
    3.39 @@ -856,11 +856,11 @@
    3.40                              else Ferrante_Rackoff_Data.Nox
    3.41     | @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
    3.42                              else Ferrante_Rackoff_Data.Nox
    3.43 -   | Const(@{const_name Algebras.less},_)$y$z =>
    3.44 +   | Const(@{const_name Orderings.less},_)$y$z =>
    3.45         if term_of x aconv y then Ferrante_Rackoff_Data.Lt
    3.46          else if term_of x aconv z then Ferrante_Rackoff_Data.Gt
    3.47          else Ferrante_Rackoff_Data.Nox
    3.48 -   | Const (@{const_name Algebras.less_eq},_)$y$z =>
    3.49 +   | Const (@{const_name Orderings.less_eq},_)$y$z =>
    3.50           if term_of x aconv y then Ferrante_Rackoff_Data.Le
    3.51           else if term_of x aconv z then Ferrante_Rackoff_Data.Ge
    3.52           else Ferrante_Rackoff_Data.Nox
     4.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 10 12:04:57 2010 +0100
     4.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 10 14:12:40 2010 +0100
     4.3 @@ -2958,8 +2958,8 @@
     4.4  val disjt = @{term "op |"};
     4.5  val impt = @{term "op -->"};
     4.6  val ifft = @{term "op = :: bool => _"}
     4.7 -fun llt rT = Const(@{const_name Algebras.less},rrT rT);
     4.8 -fun lle rT = Const(@{const_name Algebras.less},rrT rT);
     4.9 +fun llt rT = Const(@{const_name Orderings.less},rrT rT);
    4.10 +fun lle rT = Const(@{const_name Orderings.less},rrT rT);
    4.11  fun eqt rT = Const("op =",rrT rT);
    4.12  fun rz rT = Const(@{const_name Algebras.zero},rT);
    4.13  
    4.14 @@ -3024,9 +3024,9 @@
    4.15    | Const("op =",ty)$p$q => 
    4.16         if domain_type ty = bT then @{code Iff} (fm_of_term m m' p, fm_of_term m m' q)
    4.17         else @{code Eq} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
    4.18 -  | Const(@{const_name Algebras.less},_)$p$q => 
    4.19 +  | Const(@{const_name Orderings.less},_)$p$q => 
    4.20          @{code Lt} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
    4.21 -  | Const(@{const_name Algebras.less_eq},_)$p$q => 
    4.22 +  | Const(@{const_name Orderings.less_eq},_)$p$q => 
    4.23          @{code Le} (@{code Sub} (tm_of_term m m' p, tm_of_term m m' q))
    4.24    | Const("Ex",_)$Abs(xn,xT,p) => 
    4.25       let val (xn', p') =  variant_abs (xn,xT,p)
     5.1 --- a/src/HOL/Fields.thy	Wed Feb 10 12:04:57 2010 +0100
     5.2 +++ b/src/HOL/Fields.thy	Wed Feb 10 14:12:40 2010 +0100
     5.3 @@ -1035,6 +1035,31 @@
     5.4    apply (simp add: order_less_imp_le)
     5.5  done
     5.6  
     5.7 +
     5.8 +lemma field_le_epsilon:
     5.9 +  fixes x y :: "'a :: {division_by_zero,linordered_field}"
    5.10 +  assumes e: "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e"
    5.11 +  shows "x \<le> y"
    5.12 +proof (rule ccontr)
    5.13 +  obtain two :: 'a where two: "two = 1 + 1" by simp
    5.14 +  assume "\<not> x \<le> y"
    5.15 +  then have yx: "y < x" by simp
    5.16 +  then have "y + - y < x + - y" by (rule add_strict_right_mono)
    5.17 +  then have "x - y > 0" by (simp add: diff_minus)
    5.18 +  then have "(x - y) / two > 0"
    5.19 +    by (rule divide_pos_pos) (simp add: two)
    5.20 +  then have "x \<le> y + (x - y) / two" by (rule e)
    5.21 +  also have "... = (x - y + two * y) / two"
    5.22 +    by (simp add: add_divide_distrib two)
    5.23 +  also have "... = (x + y) / two" 
    5.24 +    by (simp add: two algebra_simps)
    5.25 +  also have "... < x" using yx
    5.26 +    by (simp add: two pos_divide_less_eq algebra_simps)
    5.27 +  finally have "x < x" .
    5.28 +  then show False ..
    5.29 +qed
    5.30 +
    5.31 +
    5.32  code_modulename SML
    5.33    Fields Arith
    5.34  
     6.1 --- a/src/HOL/Groebner_Basis.thy	Wed Feb 10 12:04:57 2010 +0100
     6.2 +++ b/src/HOL/Groebner_Basis.thy	Wed Feb 10 14:12:40 2010 +0100
     6.3 @@ -556,14 +556,14 @@
     6.4  
     6.5   fun proc3 phi ss ct =
     6.6    (case term_of ct of
     6.7 -    Const(@{const_name Algebras.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
     6.8 +    Const(@{const_name Orderings.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
     6.9        let
    6.10          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
    6.11          val _ = map is_number [a,b,c]
    6.12          val T = ctyp_of_term c
    6.13          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
    6.14        in SOME (mk_meta_eq th) end
    6.15 -  | Const(@{const_name Algebras.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
    6.16 +  | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
    6.17        let
    6.18          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
    6.19          val _ = map is_number [a,b,c]
    6.20 @@ -577,14 +577,14 @@
    6.21          val T = ctyp_of_term c
    6.22          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
    6.23        in SOME (mk_meta_eq th) end
    6.24 -  | Const(@{const_name Algebras.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
    6.25 +  | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
    6.26      let
    6.27        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
    6.28          val _ = map is_number [a,b,c]
    6.29          val T = ctyp_of_term c
    6.30          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
    6.31        in SOME (mk_meta_eq th) end
    6.32 -  | Const(@{const_name Algebras.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
    6.33 +  | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
    6.34      let
    6.35        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
    6.36          val _ = map is_number [a,b,c]
     7.1 --- a/src/HOL/Groups.thy	Wed Feb 10 12:04:57 2010 +0100
     7.2 +++ b/src/HOL/Groups.thy	Wed Feb 10 14:12:40 2010 +0100
     7.3 @@ -5,7 +5,7 @@
     7.4  header {* Groups, also combined with orderings *}
     7.5  
     7.6  theory Groups
     7.7 -imports Lattices
     7.8 +imports Orderings
     7.9  uses "~~/src/Provers/Arith/abel_cancel.ML"
    7.10  begin
    7.11  
    7.12 @@ -40,6 +40,7 @@
    7.13  Of course it also works for fields, but it knows nothing about multiplicative
    7.14  inverses or division. This is catered for by @{text field_simps}. *}
    7.15  
    7.16 +
    7.17  subsection {* Semigroups and Monoids *}
    7.18  
    7.19  class semigroup_add = plus +
    7.20 @@ -884,6 +885,32 @@
    7.21    shows "[|0\<le>a; b<c|] ==> b < a + c"
    7.22  by (insert add_le_less_mono [of 0 a b c], simp)
    7.23  
    7.24 +class abs =
    7.25 +  fixes abs :: "'a \<Rightarrow> 'a"
    7.26 +begin
    7.27 +
    7.28 +notation (xsymbols)
    7.29 +  abs  ("\<bar>_\<bar>")
    7.30 +
    7.31 +notation (HTML output)
    7.32 +  abs  ("\<bar>_\<bar>")
    7.33 +
    7.34 +end
    7.35 +
    7.36 +class sgn =
    7.37 +  fixes sgn :: "'a \<Rightarrow> 'a"
    7.38 +
    7.39 +class abs_if = minus + uminus + ord + zero + abs +
    7.40 +  assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
    7.41 +
    7.42 +class sgn_if = minus + uminus + zero + one + ord + sgn +
    7.43 +  assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
    7.44 +begin
    7.45 +
    7.46 +lemma sgn0 [simp]: "sgn 0 = 0"
    7.47 +  by (simp add:sgn_if)
    7.48 +
    7.49 +end
    7.50  
    7.51  class ordered_ab_group_add_abs = ordered_ab_group_add + abs +
    7.52    assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0"
     8.1 --- a/src/HOL/Hoare/hoare_tac.ML	Wed Feb 10 12:04:57 2010 +0100
     8.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Wed Feb 10 14:12:40 2010 +0100
     8.3 @@ -58,7 +58,7 @@
     8.4    let val T as Type ("fun",[t,_]) = fastype_of trm
     8.5    in Collect_const t $ trm end;
     8.6  
     8.7 -fun inclt ty = Const (@{const_name Algebras.less_eq}, [ty,ty] ---> boolT);
     8.8 +fun inclt ty = Const (@{const_name Orderings.less_eq}, [ty,ty] ---> boolT);
     8.9  
    8.10  
    8.11  fun Mset ctxt prop =
     9.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Wed Feb 10 12:04:57 2010 +0100
     9.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Wed Feb 10 14:12:40 2010 +0100
     9.3 @@ -166,7 +166,7 @@
     9.4  import_theory prim_rec;
     9.5  
     9.6  const_maps
     9.7 -    "<" > Algebras.less :: "[nat,nat]=>bool";
     9.8 +    "<" > Orderings.less :: "[nat,nat]=>bool";
     9.9  
    9.10  end_import;
    9.11  
    9.12 @@ -181,7 +181,7 @@
    9.13    ">"          > HOL4Compat.nat_gt
    9.14    ">="         > HOL4Compat.nat_ge
    9.15    FUNPOW       > HOL4Compat.FUNPOW
    9.16 -  "<="         > Algebras.less_eq :: "[nat,nat]=>bool"
    9.17 +  "<="         > Orderings.less_eq :: "[nat,nat]=>bool"
    9.18    "+"          > Algebras.plus :: "[nat,nat]=>nat"
    9.19    "*"          > Algebras.times :: "[nat,nat]=>nat"
    9.20    "-"          > Algebras.minus :: "[nat,nat]=>nat"
    10.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Wed Feb 10 12:04:57 2010 +0100
    10.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Wed Feb 10 14:12:40 2010 +0100
    10.3 @@ -22,7 +22,7 @@
    10.4    inv      > Algebras.inverse   :: "real => real"
    10.5    real_add > Algebras.plus      :: "[real,real] => real"
    10.6    real_mul > Algebras.times     :: "[real,real] => real"
    10.7 -  real_lt  > Algebras.less      :: "[real,real] => bool";
    10.8 +  real_lt  > Orderings.less      :: "[real,real] => bool";
    10.9  
   10.10  ignore_thms
   10.11      real_TY_DEF
   10.12 @@ -50,11 +50,11 @@
   10.13  const_maps
   10.14    real_gt     > HOL4Compat.real_gt
   10.15    real_ge     > HOL4Compat.real_ge
   10.16 -  real_lte    > Algebras.less_eq :: "[real,real] => bool"
   10.17 +  real_lte    > Orderings.less_eq :: "[real,real] => bool"
   10.18    real_sub    > Algebras.minus :: "[real,real] => real"
   10.19    "/"         > Algebras.divide :: "[real,real] => real"
   10.20    pow         > Power.power :: "[real,nat] => real"
   10.21 -  abs         > Algebras.abs :: "real => real"
   10.22 +  abs         > Groups.abs :: "real => real"
   10.23    real_of_num > RealDef.real :: "nat => real";
   10.24  
   10.25  end_import;
    11.1 --- a/src/HOL/Import/HOL/arithmetic.imp	Wed Feb 10 12:04:57 2010 +0100
    11.2 +++ b/src/HOL/Import/HOL/arithmetic.imp	Wed Feb 10 14:12:40 2010 +0100
    11.3 @@ -23,7 +23,7 @@
    11.4    "ALT_ZERO" > "HOL4Compat.ALT_ZERO"
    11.5    ">=" > "HOL4Compat.nat_ge"
    11.6    ">" > "HOL4Compat.nat_gt"
    11.7 -  "<=" > "Algebras.ord_class.less_eq" :: "nat => nat => bool"
    11.8 +  "<=" > "Orderings.less_eq" :: "nat => nat => bool"
    11.9    "-" > "Algebras.minus_class.minus" :: "nat => nat => nat"
   11.10    "+" > "Algebras.plus_class.plus" :: "nat => nat => nat"
   11.11    "*" > "Algebras.times_class.times" :: "nat => nat => nat"
    12.1 --- a/src/HOL/Import/HOL/prim_rec.imp	Wed Feb 10 12:04:57 2010 +0100
    12.2 +++ b/src/HOL/Import/HOL/prim_rec.imp	Wed Feb 10 14:12:40 2010 +0100
    12.3 @@ -18,7 +18,7 @@
    12.4    "PRIM_REC_FUN" > "HOL4Base.prim_rec.PRIM_REC_FUN"
    12.5    "PRIM_REC" > "HOL4Base.prim_rec.PRIM_REC"
    12.6    "PRE" > "HOL4Base.prim_rec.PRE"
    12.7 -  "<" > "Algebras.less" :: "nat => nat => bool"
    12.8 +  "<" > "Orderings.less" :: "nat => nat => bool"
    12.9  
   12.10  thm_maps
   12.11    "wellfounded_primdef" > "HOL4Base.prim_rec.wellfounded_primdef"
    13.1 --- a/src/HOL/Import/HOL/real.imp	Wed Feb 10 12:04:57 2010 +0100
    13.2 +++ b/src/HOL/Import/HOL/real.imp	Wed Feb 10 14:12:40 2010 +0100
    13.3 @@ -12,11 +12,11 @@
    13.4    "sum" > "HOL4Real.real.sum"
    13.5    "real_sub" > "Algebras.minus" :: "real => real => real"
    13.6    "real_of_num" > "RealDef.real" :: "nat => real"
    13.7 -  "real_lte" > "Algebras.less_eq" :: "real => real => bool"
    13.8 +  "real_lte" > "Orderings.less_eq" :: "real => real => bool"
    13.9    "real_gt" > "HOL4Compat.real_gt"
   13.10    "real_ge" > "HOL4Compat.real_ge"
   13.11    "pow" > "Power.power_class.power" :: "real => nat => real"
   13.12 -  "abs" > "Algebras.abs" :: "real => real"
   13.13 +  "abs" > "Groups.abs" :: "real => real"
   13.14    "/" > "Ring.divide" :: "real => real => real"
   13.15  
   13.16  thm_maps
    14.1 --- a/src/HOL/Import/HOL/realax.imp	Wed Feb 10 12:04:57 2010 +0100
    14.2 +++ b/src/HOL/Import/HOL/realax.imp	Wed Feb 10 14:12:40 2010 +0100
    14.3 @@ -29,7 +29,7 @@
    14.4    "treal_0" > "HOL4Real.realax.treal_0"
    14.5    "real_neg" > "Algebras.uminus_class.uminus" :: "real => real"
    14.6    "real_mul" > "Algebras.times_class.times" :: "real => real => real"
    14.7 -  "real_lt" > "Algebras.ord_class.less" :: "real => real => bool"
    14.8 +  "real_lt" > "Orderings.less" :: "real => real => bool"
    14.9    "real_add" > "Algebras.plus_class.plus" :: "real => real => real"
   14.10    "real_1" > "Algebras.one_class.one" :: "real"
   14.11    "real_0" > "Algebras.zero_class.zero" :: "real"
    15.1 --- a/src/HOL/IsaMakefile	Wed Feb 10 12:04:57 2010 +0100
    15.2 +++ b/src/HOL/IsaMakefile	Wed Feb 10 14:12:40 2010 +0100
    15.3 @@ -397,7 +397,6 @@
    15.4    Library/Library/document/root.tex Library/Library/document/root.bib	\
    15.5    Library/Transitive_Closure_Table.thy Library/While_Combinator.thy	\
    15.6    Library/Product_ord.thy Library/Char_nat.thy				\
    15.7 -  Library/Structure_Syntax.thy						\
    15.8    Library/Sublist_Order.thy Library/List_lexord.thy			\
    15.9    Library/Coinductive_List.thy Library/AssocList.thy			\
   15.10    Library/Formal_Power_Series.thy Library/Binomial.thy			\
    16.1 --- a/src/HOL/Library/Library.thy	Wed Feb 10 12:04:57 2010 +0100
    16.2 +++ b/src/HOL/Library/Library.thy	Wed Feb 10 14:12:40 2010 +0100
    16.3 @@ -51,7 +51,6 @@
    16.4    RBT
    16.5    SML_Quickcheck
    16.6    State_Monad
    16.7 -  Structure_Syntax
    16.8    Sum_Of_Squares
    16.9    Transitive_Closure_Table
   16.10    Univ_Poly
    17.1 --- a/src/HOL/Library/Structure_Syntax.thy	Wed Feb 10 12:04:57 2010 +0100
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,14 +0,0 @@
    17.4 -(* Author: Florian Haftmann, TU Muenchen *)
    17.5 -
    17.6 -header {* Index syntax for structures *}
    17.7 -
    17.8 -theory Structure_Syntax
    17.9 -imports Pure
   17.10 -begin
   17.11 -
   17.12 -syntax
   17.13 -  "_index1"  :: index    ("\<^sub>1")
   17.14 -translations
   17.15 -  (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
   17.16 -
   17.17 -end
    18.1 --- a/src/HOL/Mutabelle/Mutabelle.thy	Wed Feb 10 12:04:57 2010 +0100
    18.2 +++ b/src/HOL/Mutabelle/Mutabelle.thy	Wed Feb 10 14:12:40 2010 +0100
    18.3 @@ -16,7 +16,7 @@
    18.4    (@{const_name dummy_pattern}, "'a::{}"),
    18.5    (@{const_name Algebras.uminus}, "'a"),
    18.6    (@{const_name Nat.size}, "'a"),
    18.7 -  (@{const_name Algebras.abs}, "'a")];
    18.8 +  (@{const_name Groups.abs}, "'a")];
    18.9  
   18.10  val forbidden_thms =
   18.11   ["finite_intvl_succ_class",
    19.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Feb 10 12:04:57 2010 +0100
    19.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Feb 10 14:12:40 2010 +0100
    19.3 @@ -197,7 +197,7 @@
    19.4    (@{const_name "dummy_pattern"}, "'a::{}") (*,
    19.5    (@{const_name "uminus"}, "'a"),
    19.6    (@{const_name "Nat.size"}, "'a"),
    19.7 -  (@{const_name "Algebras.abs"}, "'a") *)]
    19.8 +  (@{const_name "Groups.abs"}, "'a") *)]
    19.9  
   19.10  val forbidden_thms =
   19.11   ["finite_intvl_succ_class",
    20.1 --- a/src/HOL/Orderings.thy	Wed Feb 10 12:04:57 2010 +0100
    20.2 +++ b/src/HOL/Orderings.thy	Wed Feb 10 14:12:40 2010 +0100
    20.3 @@ -11,6 +11,41 @@
    20.4    "~~/src/Provers/quasi.ML"  (* FIXME unused? *)
    20.5  begin
    20.6  
    20.7 +subsection {* Syntactic orders *}
    20.8 +
    20.9 +class ord =
   20.10 +  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   20.11 +    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   20.12 +begin
   20.13 +
   20.14 +notation
   20.15 +  less_eq  ("op <=") and
   20.16 +  less_eq  ("(_/ <= _)" [51, 51] 50) and
   20.17 +  less  ("op <") and
   20.18 +  less  ("(_/ < _)"  [51, 51] 50)
   20.19 +  
   20.20 +notation (xsymbols)
   20.21 +  less_eq  ("op \<le>") and
   20.22 +  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
   20.23 +
   20.24 +notation (HTML output)
   20.25 +  less_eq  ("op \<le>") and
   20.26 +  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
   20.27 +
   20.28 +abbreviation (input)
   20.29 +  greater_eq  (infix ">=" 50) where
   20.30 +  "x >= y \<equiv> y <= x"
   20.31 +
   20.32 +notation (input)
   20.33 +  greater_eq  (infix "\<ge>" 50)
   20.34 +
   20.35 +abbreviation (input)
   20.36 +  greater  (infix ">" 50) where
   20.37 +  "x > y \<equiv> y < x"
   20.38 +
   20.39 +end
   20.40 +
   20.41 +
   20.42  subsection {* Quasi orders *}
   20.43  
   20.44  class preorder = ord +
    21.1 --- a/src/HOL/Real.thy	Wed Feb 10 12:04:57 2010 +0100
    21.2 +++ b/src/HOL/Real.thy	Wed Feb 10 14:12:40 2010 +0100
    21.3 @@ -2,25 +2,4 @@
    21.4  imports RComplete RealVector
    21.5  begin
    21.6  
    21.7 -lemma field_le_epsilon:
    21.8 -  fixes x y :: "'a:: {number_ring,division_by_zero,linordered_field}"
    21.9 -  assumes e: "(!!e. 0 < e ==> x \<le> y + e)"
   21.10 -  shows "x \<le> y"
   21.11 -proof (rule ccontr)
   21.12 -  assume xy: "\<not> x \<le> y"
   21.13 -  hence "(x-y)/2 > 0"
   21.14 -    by simp
   21.15 -  hence "x \<le> y + (x - y) / 2"
   21.16 -    by (rule e [of "(x-y)/2"])
   21.17 -  also have "... = (x - y + 2*y)/2"
   21.18 -    by (simp add: diff_divide_distrib)
   21.19 -  also have "... = (x + y) / 2" 
   21.20 -    by simp
   21.21 -  also have "... < x" using xy 
   21.22 -    by simp
   21.23 -  finally have "x<x" .
   21.24 -  thus False
   21.25 -    by simp
   21.26 -qed
   21.27 -
   21.28  end
    22.1 --- a/src/HOL/Rings.thy	Wed Feb 10 12:04:57 2010 +0100
    22.2 +++ b/src/HOL/Rings.thy	Wed Feb 10 14:12:40 2010 +0100
    22.3 @@ -782,15 +782,6 @@
    22.4  
    22.5  end
    22.6  
    22.7 -class abs_if = minus + uminus + ord + zero + abs +
    22.8 -  assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
    22.9 -
   22.10 -class sgn_if = minus + uminus + zero + one + ord + sgn +
   22.11 -  assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
   22.12 -
   22.13 -lemma (in sgn_if) sgn0[simp]: "sgn 0 = 0"
   22.14 -by(simp add:sgn_if)
   22.15 -
   22.16  class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if
   22.17  begin
   22.18  
    23.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Wed Feb 10 12:04:57 2010 +0100
    23.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Wed Feb 10 14:12:40 2010 +0100
    23.3 @@ -80,10 +80,10 @@
    23.4    let
    23.5      val goals = cterm_of thy o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
    23.6    in
    23.7 -    case try_proof (goals @{const_name Algebras.less}) solve_tac of
    23.8 +    case try_proof (goals @{const_name Orderings.less}) solve_tac of
    23.9        Solved thm => Less thm
   23.10      | Stuck thm =>
   23.11 -      (case try_proof (goals @{const_name Algebras.less_eq}) solve_tac of
   23.12 +      (case try_proof (goals @{const_name Orderings.less_eq}) solve_tac of
   23.13           Solved thm2 => LessEq (thm2, thm)
   23.14         | Stuck thm2 =>
   23.15           if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const] then False thm2
    24.1 --- a/src/HOL/Tools/Function/termination.ML	Wed Feb 10 12:04:57 2010 +0100
    24.2 +++ b/src/HOL/Tools/Function/termination.ML	Wed Feb 10 14:12:40 2010 +0100
    24.3 @@ -203,10 +203,10 @@
    24.4               HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
    24.5                 $ (m2 $ r) $ (m1 $ l)))))) tac
    24.6    in
    24.7 -    case try @{const_name Algebras.less} of
    24.8 +    case try @{const_name Orderings.less} of
    24.9         Solved thm => Less thm
   24.10       | Stuck thm =>
   24.11 -       (case try @{const_name Algebras.less_eq} of
   24.12 +       (case try @{const_name Orderings.less_eq} of
   24.13            Solved thm2 => LessEq (thm2, thm)
   24.14          | Stuck thm2 =>
   24.15            if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const]
    25.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Feb 10 12:04:57 2010 +0100
    25.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Feb 10 14:12:40 2010 +0100
    25.3 @@ -223,7 +223,7 @@
    25.4    @{const_name False},
    25.5    @{const_name Suc}, @{const_name Nat.zero_nat_inst.zero_nat},
    25.6    @{const_name Nat.one_nat_inst.one_nat},
    25.7 -  @{const_name Algebras.ord_class.less}, @{const_name Algebras.ord_class.less_eq},
    25.8 +  @{const_name Orderings.less}, @{const_name Orderings.less_eq},
    25.9    @{const_name Algebras.zero},
   25.10    @{const_name Algebras.one},  @{const_name Algebras.plus},
   25.11    @{const_name Nat.ord_nat_inst.less_eq_nat},
    26.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Wed Feb 10 12:04:57 2010 +0100
    26.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Wed Feb 10 14:12:40 2010 +0100
    26.3 @@ -73,10 +73,10 @@
    26.4  | Const ("op =",ty)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
    26.5  | Const (@{const_name Not},_) $ (Const ("op =",_)$y$_) =>
    26.6    if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
    26.7 -| Const (@{const_name Algebras.less}, _) $ y$ z =>
    26.8 +| Const (@{const_name Orderings.less}, _) $ y$ z =>
    26.9     if term_of x aconv y then Lt (Thm.dest_arg ct)
   26.10     else if term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox
   26.11 -| Const (@{const_name Algebras.less_eq}, _) $ y $ z =>
   26.12 +| Const (@{const_name Orderings.less_eq}, _) $ y $ z =>
   26.13     if term_of x aconv y then Le (Thm.dest_arg ct)
   26.14     else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
   26.15  | Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$y$_) =>
   26.16 @@ -217,10 +217,10 @@
   26.17    end
   26.18   | _ => addC $ (mulC $ one $ tm) $ zero;
   26.19  
   26.20 -fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name Algebras.less}, T) $ s $ t)) =
   26.21 -    lin vs (Const (@{const_name Algebras.less_eq}, T) $ t $ s)
   26.22 -  | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name Algebras.less_eq}, T) $ s $ t)) =
   26.23 -    lin vs (Const (@{const_name Algebras.less}, T) $ t $ s)
   26.24 +fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name Orderings.less}, T) $ s $ t)) =
   26.25 +    lin vs (Const (@{const_name Orderings.less_eq}, T) $ t $ s)
   26.26 +  | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name Orderings.less_eq}, T) $ s $ t)) =
   26.27 +    lin vs (Const (@{const_name Orderings.less}, T) $ t $ s)
   26.28    | lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t)
   26.29    | lin (vs as x::_) (Const(@{const_name Rings.dvd},_)$d$t) =
   26.30      HOLogic.mk_binrel @{const_name Rings.dvd} (numeral1 abs d, lint vs t)
   26.31 @@ -295,11 +295,11 @@
   26.32     case (term_of t) of
   26.33      Const(s,_)$(Const(@{const_name Algebras.times},_)$c$y)$ _ =>
   26.34      if x aconv y andalso member (op =)
   26.35 -      ["op =", @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
   26.36 +      ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   26.37      then (ins (dest_numeral c) acc,dacc) else (acc,dacc)
   26.38    | Const(s,_)$_$(Const(@{const_name Algebras.times},_)$c$y) =>
   26.39      if x aconv y andalso member (op =)
   26.40 -       [@{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
   26.41 +       [@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   26.42      then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
   26.43    | Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_) =>
   26.44      if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)
   26.45 @@ -337,11 +337,11 @@
   26.46    | Const (@{const_name Not},_)$_ => arg_conv unit_conv t
   26.47    | Const(s,_)$(Const(@{const_name Algebras.times},_)$c$y)$ _ =>
   26.48      if x=y andalso member (op =)
   26.49 -      ["op =", @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
   26.50 +      ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   26.51      then cv (l div dest_numeral c) t else Thm.reflexive t
   26.52    | Const(s,_)$_$(Const(@{const_name Algebras.times},_)$c$y) =>
   26.53      if x=y andalso member (op =)
   26.54 -      [@{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
   26.55 +      [@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   26.56      then cv (l div dest_numeral c) t else Thm.reflexive t
   26.57    | Const(@{const_name Rings.dvd},_)$d$(r as (Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_)) =>
   26.58      if x=y then
   26.59 @@ -560,8 +560,8 @@
   26.60  fun qf_of_term ps vs t =  case t
   26.61   of Const("True",_) => T
   26.62    | Const("False",_) => F
   26.63 -  | Const(@{const_name Algebras.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
   26.64 -  | Const(@{const_name Algebras.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
   26.65 +  | Const(@{const_name Orderings.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
   26.66 +  | Const(@{const_name Orderings.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
   26.67    | Const(@{const_name Rings.dvd},_)$t1$t2 =>
   26.68        (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")  (* FIXME avoid handle _ *)
   26.69    | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
    27.1 --- a/src/HOL/Tools/inductive.ML	Wed Feb 10 12:04:57 2010 +0100
    27.2 +++ b/src/HOL/Tools/inductive.ML	Wed Feb 10 14:12:40 2010 +0100
    27.3 @@ -184,7 +184,7 @@
    27.4      case concl_of thm of
    27.5        Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
    27.6      | _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
    27.7 -    | _ $ (Const (@{const_name Algebras.less_eq}, _) $ _ $ _) =>
    27.8 +    | _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) =>
    27.9        dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
   27.10          (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
   27.11      | _ => thm
   27.12 @@ -561,7 +561,7 @@
   27.13           (list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))) preds));
   27.14  
   27.15      val ind_concl = HOLogic.mk_Trueprop
   27.16 -      (HOLogic.mk_binrel @{const_name Algebras.less_eq} (rec_const, ind_pred));
   27.17 +      (HOLogic.mk_binrel @{const_name Orderings.less_eq} (rec_const, ind_pred));
   27.18  
   27.19      val raw_fp_induct = (mono RS (fp_def RS @{thm def_lfp_induct}));
   27.20  
    28.1 --- a/src/HOL/Tools/int_arith.ML	Wed Feb 10 12:04:57 2010 +0100
    28.2 +++ b/src/HOL/Tools/int_arith.ML	Wed Feb 10 14:12:40 2010 +0100
    28.3 @@ -55,7 +55,7 @@
    28.4        @{const_name Algebras.times}, @{const_name Algebras.uminus},
    28.5        @{const_name Algebras.minus}, @{const_name Algebras.plus},
    28.6        @{const_name Algebras.zero},
    28.7 -      @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
    28.8 +      @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
    28.9    | check (a $ b) = check a andalso check b
   28.10    | check _ = false;
   28.11  
    29.1 --- a/src/HOL/Tools/lin_arith.ML	Wed Feb 10 12:04:57 2010 +0100
    29.2 +++ b/src/HOL/Tools/lin_arith.ML	Wed Feb 10 14:12:40 2010 +0100
    29.3 @@ -229,8 +229,8 @@
    29.4    val (q, j) = poly (rhs, Rat.one, ([], Rat.zero))
    29.5  in
    29.6    case rel of
    29.7 -    @{const_name Algebras.less}    => SOME (p, i, "<", q, j)
    29.8 -  | @{const_name Algebras.less_eq} => SOME (p, i, "<=", q, j)
    29.9 +    @{const_name Orderings.less}    => SOME (p, i, "<", q, j)
   29.10 +  | @{const_name Orderings.less_eq} => SOME (p, i, "<=", q, j)
   29.11    | "op ="              => SOME (p, i, "=", q, j)
   29.12    | _                   => NONE
   29.13  end handle Rat.DIVZERO => NONE;
   29.14 @@ -292,7 +292,7 @@
   29.15      case head_of lhs of
   29.16        Const (a, _) => member (op =) [@{const_name Orderings.max},
   29.17                                      @{const_name Orderings.min},
   29.18 -                                    @{const_name Algebras.abs},
   29.19 +                                    @{const_name Groups.abs},
   29.20                                      @{const_name Algebras.minus},
   29.21                                      "Int.nat" (*DYNAMIC BINDING!*),
   29.22                                      "Divides.div_class.mod" (*DYNAMIC BINDING!*),
   29.23 @@ -372,7 +372,7 @@
   29.24          val rev_terms     = rev terms
   29.25          val terms1        = map (subst_term [(split_term, t1)]) rev_terms
   29.26          val terms2        = map (subst_term [(split_term, t2)]) rev_terms
   29.27 -        val t1_leq_t2     = Const (@{const_name Algebras.less_eq},
   29.28 +        val t1_leq_t2     = Const (@{const_name Orderings.less_eq},
   29.29                                      split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
   29.30          val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
   29.31          val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   29.32 @@ -387,7 +387,7 @@
   29.33          val rev_terms     = rev terms
   29.34          val terms1        = map (subst_term [(split_term, t1)]) rev_terms
   29.35          val terms2        = map (subst_term [(split_term, t2)]) rev_terms
   29.36 -        val t1_leq_t2     = Const (@{const_name Algebras.less_eq},
   29.37 +        val t1_leq_t2     = Const (@{const_name Orderings.less_eq},
   29.38                                      split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
   29.39          val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
   29.40          val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   29.41 @@ -397,16 +397,16 @@
   29.42          SOME [(Ts, subgoal1), (Ts, subgoal2)]
   29.43        end
   29.44      (* ?P (abs ?a) = ((0 <= ?a --> ?P ?a) & (?a < 0 --> ?P (- ?a))) *)
   29.45 -    | (Const (@{const_name Algebras.abs}, _), [t1]) =>
   29.46 +    | (Const (@{const_name Groups.abs}, _), [t1]) =>
   29.47        let
   29.48          val rev_terms   = rev terms
   29.49          val terms1      = map (subst_term [(split_term, t1)]) rev_terms
   29.50          val terms2      = map (subst_term [(split_term, Const (@{const_name Algebras.uminus},
   29.51                              split_type --> split_type) $ t1)]) rev_terms
   29.52          val zero        = Const (@{const_name Algebras.zero}, split_type)
   29.53 -        val zero_leq_t1 = Const (@{const_name Algebras.less_eq},
   29.54 +        val zero_leq_t1 = Const (@{const_name Orderings.less_eq},
   29.55                              split_type --> split_type --> HOLogic.boolT) $ zero $ t1
   29.56 -        val t1_lt_zero  = Const (@{const_name Algebras.less},
   29.57 +        val t1_lt_zero  = Const (@{const_name Orderings.less},
   29.58                              split_type --> split_type --> HOLogic.boolT) $ t1 $ zero
   29.59          val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   29.60          val subgoal1    = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false]
   29.61 @@ -427,7 +427,7 @@
   29.62                                  (map (incr_boundvars 1) rev_terms)
   29.63          val t1'             = incr_boundvars 1 t1
   29.64          val t2'             = incr_boundvars 1 t2
   29.65 -        val t1_lt_t2        = Const (@{const_name Algebras.less},
   29.66 +        val t1_lt_t2        = Const (@{const_name Orderings.less},
   29.67                                  split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
   29.68          val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
   29.69                                  (Const (@{const_name Algebras.plus},
   29.70 @@ -451,7 +451,7 @@
   29.71          val t1'         = incr_boundvars 1 t1
   29.72          val t1_eq_nat_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
   29.73                              (Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n)
   29.74 -        val t1_lt_zero  = Const (@{const_name Algebras.less},
   29.75 +        val t1_lt_zero  = Const (@{const_name Orderings.less},
   29.76                              HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
   29.77          val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   29.78          val subgoal1    = (HOLogic.mk_Trueprop t1_eq_nat_n) :: terms1 @ [not_false]
   29.79 @@ -477,7 +477,7 @@
   29.80                                          split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
   29.81          val t2_neq_zero             = HOLogic.mk_not (Const ("op =",
   29.82                                          split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
   29.83 -        val j_lt_t2                 = Const (@{const_name Algebras.less},
   29.84 +        val j_lt_t2                 = Const (@{const_name Orderings.less},
   29.85                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
   29.86          val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
   29.87                                         (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
   29.88 @@ -509,7 +509,7 @@
   29.89                                          split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
   29.90          val t2_neq_zero             = HOLogic.mk_not (Const ("op =",
   29.91                                          split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
   29.92 -        val j_lt_t2                 = Const (@{const_name Algebras.less},
   29.93 +        val j_lt_t2                 = Const (@{const_name Orderings.less},
   29.94                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
   29.95          val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
   29.96                                         (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
   29.97 @@ -545,17 +545,17 @@
   29.98          val t2'                     = incr_boundvars 2 t2
   29.99          val t2_eq_zero              = Const ("op =",
  29.100                                          split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
  29.101 -        val zero_lt_t2              = Const (@{const_name Algebras.less},
  29.102 +        val zero_lt_t2              = Const (@{const_name Orderings.less},
  29.103                                          split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
  29.104 -        val t2_lt_zero              = Const (@{const_name Algebras.less},
  29.105 +        val t2_lt_zero              = Const (@{const_name Orderings.less},
  29.106                                          split_type --> split_type --> HOLogic.boolT) $ t2' $ zero
  29.107 -        val zero_leq_j              = Const (@{const_name Algebras.less_eq},
  29.108 +        val zero_leq_j              = Const (@{const_name Orderings.less_eq},
  29.109                                          split_type --> split_type --> HOLogic.boolT) $ zero $ j
  29.110 -        val j_leq_zero              = Const (@{const_name Algebras.less_eq},
  29.111 +        val j_leq_zero              = Const (@{const_name Orderings.less_eq},
  29.112                                          split_type --> split_type --> HOLogic.boolT) $ j $ zero
  29.113 -        val j_lt_t2                 = Const (@{const_name Algebras.less},
  29.114 +        val j_lt_t2                 = Const (@{const_name Orderings.less},
  29.115                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
  29.116 -        val t2_lt_j                 = Const (@{const_name Algebras.less},
  29.117 +        val t2_lt_j                 = Const (@{const_name Orderings.less},
  29.118                                          split_type --> split_type--> HOLogic.boolT) $ t2' $ j
  29.119          val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
  29.120                                         (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
  29.121 @@ -599,17 +599,17 @@
  29.122          val t2'                     = incr_boundvars 2 t2
  29.123          val t2_eq_zero              = Const ("op =",
  29.124                                          split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
  29.125 -        val zero_lt_t2              = Const (@{const_name Algebras.less},
  29.126 +        val zero_lt_t2              = Const (@{const_name Orderings.less},
  29.127                                          split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
  29.128 -        val t2_lt_zero              = Const (@{const_name Algebras.less},
  29.129 +        val t2_lt_zero              = Const (@{const_name Orderings.less},
  29.130                                          split_type --> split_type --> HOLogic.boolT) $ t2' $ zero
  29.131 -        val zero_leq_j              = Const (@{const_name Algebras.less_eq},
  29.132 +        val zero_leq_j              = Const (@{const_name Orderings.less_eq},
  29.133                                          split_type --> split_type --> HOLogic.boolT) $ zero $ j
  29.134 -        val j_leq_zero              = Const (@{const_name Algebras.less_eq},
  29.135 +        val j_leq_zero              = Const (@{const_name Orderings.less_eq},
  29.136                                          split_type --> split_type --> HOLogic.boolT) $ j $ zero
  29.137 -        val j_lt_t2                 = Const (@{const_name Algebras.less},
  29.138 +        val j_lt_t2                 = Const (@{const_name Orderings.less},
  29.139                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
  29.140 -        val t2_lt_j                 = Const (@{const_name Algebras.less},
  29.141 +        val t2_lt_j                 = Const (@{const_name Orderings.less},
  29.142                                          split_type --> split_type--> HOLogic.boolT) $ t2' $ j
  29.143          val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
  29.144                                         (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
    30.1 --- a/src/HOL/Tools/nat_arith.ML	Wed Feb 10 12:04:57 2010 +0100
    30.2 +++ b/src/HOL/Tools/nat_arith.ML	Wed Feb 10 14:12:40 2010 +0100
    30.3 @@ -69,16 +69,16 @@
    30.4  structure LessCancelSums = CancelSumsFun
    30.5  (struct
    30.6    open CommonCancelSums;
    30.7 -  val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less};
    30.8 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT;
    30.9 +  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less};
   30.10 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT;
   30.11    val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
   30.12  end);
   30.13  
   30.14  structure LeCancelSums = CancelSumsFun
   30.15  (struct
   30.16    open CommonCancelSums;
   30.17 -  val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq};
   30.18 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT;
   30.19 +  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq};
   30.20 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT;
   30.21    val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
   30.22  end);
   30.23  
    31.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Wed Feb 10 12:04:57 2010 +0100
    31.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Wed Feb 10 14:12:40 2010 +0100
    31.3 @@ -176,8 +176,8 @@
    31.4  structure LessCancelNumerals = CancelNumeralsFun
    31.5   (open CancelNumeralsCommon
    31.6    val prove_conv = Arith_Data.prove_conv
    31.7 -  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
    31.8 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT
    31.9 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   31.10 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
   31.11    val bal_add1 = @{thm nat_less_add_iff1} RS trans
   31.12    val bal_add2 = @{thm nat_less_add_iff2} RS trans
   31.13  );
   31.14 @@ -185,8 +185,8 @@
   31.15  structure LeCancelNumerals = CancelNumeralsFun
   31.16   (open CancelNumeralsCommon
   31.17    val prove_conv = Arith_Data.prove_conv
   31.18 -  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
   31.19 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT
   31.20 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   31.21 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
   31.22    val bal_add1 = @{thm nat_le_add_iff1} RS trans
   31.23    val bal_add2 = @{thm nat_le_add_iff2} RS trans
   31.24  );
   31.25 @@ -308,8 +308,8 @@
   31.26  structure LessCancelNumeralFactor = CancelNumeralFactorFun
   31.27   (open CancelNumeralFactorCommon
   31.28    val prove_conv = Arith_Data.prove_conv
   31.29 -  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
   31.30 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT
   31.31 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   31.32 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
   31.33    val cancel = @{thm nat_mult_less_cancel1} RS trans
   31.34    val neg_exchanges = true
   31.35  )
   31.36 @@ -317,8 +317,8 @@
   31.37  structure LeCancelNumeralFactor = CancelNumeralFactorFun
   31.38   (open CancelNumeralFactorCommon
   31.39    val prove_conv = Arith_Data.prove_conv
   31.40 -  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
   31.41 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT
   31.42 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   31.43 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
   31.44    val cancel = @{thm nat_mult_le_cancel1} RS trans
   31.45    val neg_exchanges = true
   31.46  )
   31.47 @@ -387,16 +387,16 @@
   31.48  structure LessCancelFactor = ExtractCommonTermFun
   31.49   (open CancelFactorCommon
   31.50    val prove_conv = Arith_Data.prove_conv
   31.51 -  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
   31.52 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT
   31.53 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   31.54 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
   31.55    fun simp_conv _ _ = SOME @{thm nat_mult_less_cancel_disj}
   31.56  );
   31.57  
   31.58  structure LeCancelFactor = ExtractCommonTermFun
   31.59   (open CancelFactorCommon
   31.60    val prove_conv = Arith_Data.prove_conv
   31.61 -  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
   31.62 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT
   31.63 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   31.64 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
   31.65    fun simp_conv _ _ = SOME @{thm nat_mult_le_cancel_disj}
   31.66  );
   31.67  
    32.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Wed Feb 10 12:04:57 2010 +0100
    32.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Wed Feb 10 14:12:40 2010 +0100
    32.3 @@ -229,8 +229,8 @@
    32.4  structure LessCancelNumerals = CancelNumeralsFun
    32.5   (open CancelNumeralsCommon
    32.6    val prove_conv = Arith_Data.prove_conv
    32.7 -  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
    32.8 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} Term.dummyT
    32.9 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   32.10 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
   32.11    val bal_add1 = @{thm less_add_iff1} RS trans
   32.12    val bal_add2 = @{thm less_add_iff2} RS trans
   32.13  );
   32.14 @@ -238,8 +238,8 @@
   32.15  structure LeCancelNumerals = CancelNumeralsFun
   32.16   (open CancelNumeralsCommon
   32.17    val prove_conv = Arith_Data.prove_conv
   32.18 -  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
   32.19 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} Term.dummyT
   32.20 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   32.21 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
   32.22    val bal_add1 = @{thm le_add_iff1} RS trans
   32.23    val bal_add2 = @{thm le_add_iff2} RS trans
   32.24  );
   32.25 @@ -409,8 +409,8 @@
   32.26  structure LessCancelNumeralFactor = CancelNumeralFactorFun
   32.27   (open CancelNumeralFactorCommon
   32.28    val prove_conv = Arith_Data.prove_conv
   32.29 -  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
   32.30 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} Term.dummyT
   32.31 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   32.32 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
   32.33    val cancel = @{thm mult_less_cancel_left} RS trans
   32.34    val neg_exchanges = true
   32.35  )
   32.36 @@ -418,8 +418,8 @@
   32.37  structure LeCancelNumeralFactor = CancelNumeralFactorFun
   32.38   (open CancelNumeralFactorCommon
   32.39    val prove_conv = Arith_Data.prove_conv
   32.40 -  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
   32.41 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} Term.dummyT
   32.42 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   32.43 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
   32.44    val cancel = @{thm mult_le_cancel_left} RS trans
   32.45    val neg_exchanges = true
   32.46  )
   32.47 @@ -485,7 +485,7 @@
   32.48  fun sign_conv pos_th neg_th ss t =
   32.49    let val T = fastype_of t;
   32.50        val zero = Const(@{const_name Algebras.zero}, T);
   32.51 -      val less = Const(@{const_name Algebras.less}, [T,T] ---> HOLogic.boolT);
   32.52 +      val less = Const(@{const_name Orderings.less}, [T,T] ---> HOLogic.boolT);
   32.53        val pos = less $ zero $ t and neg = less $ t $ zero
   32.54        fun prove p =
   32.55          Option.map Eq_True_elim (Lin_Arith.simproc ss p)
   32.56 @@ -524,8 +524,8 @@
   32.57  structure LeCancelFactor = ExtractCommonTermFun
   32.58   (open CancelFactorCommon
   32.59    val prove_conv = Arith_Data.prove_conv
   32.60 -  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
   32.61 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} Term.dummyT
   32.62 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   32.63 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
   32.64    val simp_conv = sign_conv
   32.65      @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg}
   32.66  );
   32.67 @@ -534,8 +534,8 @@
   32.68  structure LessCancelFactor = ExtractCommonTermFun
   32.69   (open CancelFactorCommon
   32.70    val prove_conv = Arith_Data.prove_conv
   32.71 -  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
   32.72 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} Term.dummyT
   32.73 +  val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   32.74 +  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
   32.75    val simp_conv = sign_conv
   32.76      @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg}
   32.77  );
    33.1 --- a/src/HOL/Tools/refute.ML	Wed Feb 10 12:04:57 2010 +0100
    33.2 +++ b/src/HOL/Tools/refute.ML	Wed Feb 10 14:12:40 2010 +0100
    33.3 @@ -708,7 +708,7 @@
    33.4        (* other optimizations *)
    33.5        | Const (@{const_name Finite_Set.card}, _) => t
    33.6        | Const (@{const_name Finite_Set.finite}, _) => t
    33.7 -      | Const (@{const_name Algebras.less}, Type ("fun", [Type ("nat", []),
    33.8 +      | Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
    33.9          Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t
   33.10        | Const (@{const_name Algebras.plus}, Type ("fun", [Type ("nat", []),
   33.11          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
   33.12 @@ -883,7 +883,7 @@
   33.13        | Const (@{const_name Finite_Set.card}, T) => collect_type_axioms T axs
   33.14        | Const (@{const_name Finite_Set.finite}, T) =>
   33.15          collect_type_axioms T axs
   33.16 -      | Const (@{const_name Algebras.less}, T as Type ("fun", [Type ("nat", []),
   33.17 +      | Const (@{const_name Orderings.less}, T as Type ("fun", [Type ("nat", []),
   33.18          Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
   33.19            collect_type_axioms T axs
   33.20        | Const (@{const_name Algebras.plus}, T as Type ("fun", [Type ("nat", []),
   33.21 @@ -2771,7 +2771,7 @@
   33.22  
   33.23    fun Nat_less_interpreter thy model args t =
   33.24      case t of
   33.25 -      Const (@{const_name Algebras.less}, Type ("fun", [Type ("nat", []),
   33.26 +      Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
   33.27          Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
   33.28        let
   33.29          val size_of_nat = size_of_type thy model (Type ("nat", []))
    34.1 --- a/src/HOL/Tools/res_clause.ML	Wed Feb 10 12:04:57 2010 +0100
    34.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Feb 10 14:12:40 2010 +0100
    34.3 @@ -99,7 +99,7 @@
    34.4  (*Provide readable names for the more common symbolic functions*)
    34.5  val const_trans_table =
    34.6        Symtab.make [(@{const_name "op ="}, "equal"),
    34.7 -                   (@{const_name Algebras.less_eq}, "lessequals"),
    34.8 +                   (@{const_name Orderings.less_eq}, "lessequals"),
    34.9                     (@{const_name "op &"}, "and"),
   34.10                     (@{const_name "op |"}, "or"),
   34.11                     (@{const_name "op -->"}, "implies"),
    35.1 --- a/src/HOL/ex/SVC_Oracle.thy	Wed Feb 10 12:04:57 2010 +0100
    35.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Wed Feb 10 14:12:40 2010 +0100
    35.3 @@ -95,8 +95,8 @@
    35.4        | fm ((c as Const("True", _))) = c
    35.5        | fm ((c as Const("False", _))) = c
    35.6        | fm (t as Const("op =",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    35.7 -      | fm (t as Const(@{const_name Algebras.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    35.8 -      | fm (t as Const(@{const_name Algebras.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
    35.9 +      | fm (t as Const(@{const_name Orderings.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
   35.10 +      | fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
   35.11        | fm t = replace t
   35.12      (*entry point, and abstraction of a meta-formula*)
   35.13      fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
    36.1 --- a/src/HOL/ex/svc_funcs.ML	Wed Feb 10 12:04:57 2010 +0100
    36.2 +++ b/src/HOL/ex/svc_funcs.ML	Wed Feb 10 14:12:40 2010 +0100
    36.3 @@ -107,8 +107,8 @@
    36.4                           b1 orelse b2)
    36.5                       end
    36.6                   else (*might be numeric equality*) (t, is_intnat T)
    36.7 -           | Const(@{const_name Algebras.less}, Type ("fun", [T,_]))  => (t, is_intnat T)
    36.8 -           | Const(@{const_name Algebras.less_eq}, Type ("fun", [T,_])) => (t, is_intnat T)
    36.9 +           | Const(@{const_name Orderings.less}, Type ("fun", [T,_]))  => (t, is_intnat T)
   36.10 +           | Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) => (t, is_intnat T)
   36.11             | _ => (t, false)
   36.12           end
   36.13     in #1 o tag end;
   36.14 @@ -211,13 +211,13 @@
   36.15                     else fail t
   36.16              end
   36.17          (*inequalities: possible types are nat, int, real*)
   36.18 -      | fm pos (t as Const(@{const_name Algebras.less},  Type ("fun", [T,_])) $ x $ y) =
   36.19 +      | fm pos (t as Const(@{const_name Orderings.less},  Type ("fun", [T,_])) $ x $ y) =
   36.20              if not pos orelse T = HOLogic.realT then
   36.21                  Buildin("<", [tm x, tm y])
   36.22              else if is_intnat T then
   36.23                  Buildin("<=", [suc (tm x), tm y])
   36.24              else fail t
   36.25 -      | fm pos (t as Const(@{const_name Algebras.less_eq},  Type ("fun", [T,_])) $ x $ y) =
   36.26 +      | fm pos (t as Const(@{const_name Orderings.less_eq},  Type ("fun", [T,_])) $ x $ y) =
   36.27              if pos orelse T = HOLogic.realT then
   36.28                  Buildin("<=", [tm x, tm y])
   36.29              else if is_intnat T then