new theory Algebras.thy for generic algebraic structures
authorhaftmann
Thu Jan 28 11:48:49 2010 +0100 (2010-01-28)
changeset 3497418b41bba42b5
parent 34973 ae634fad947e
child 34975 f099b0b20646
child 34991 1adaefa63c5a
new theory Algebras.thy for generic algebraic structures
NEWS
src/HOL/Algebra/abstract/Ring2.thy
src/HOL/Algebras.thy
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/commutative_ring_tac.ML
src/HOL/Groebner_Basis.thy
src/HOL/HOL.thy
src/HOL/Hoare/hoare_tac.ML
src/HOL/Import/Generate-HOL/GenHOL4Base.thy
src/HOL/Import/Generate-HOL/GenHOL4Real.thy
src/HOL/Import/Generate-HOLLight/GenHOLLight.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/Import/HOLLight/HOLLight.thy
src/HOL/Import/HOLLight/hollight.imp
src/HOL/IsaMakefile
src/HOL/Mutabelle/Mutabelle.thy
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/NSA/NSA.thy
src/HOL/Orderings.thy
src/HOL/Prolog/Func.thy
src/HOL/Prolog/HOHH.thy
src/HOL/Prolog/Test.thy
src/HOL/Prolog/Type.thy
src/HOL/Set.thy
src/HOL/Tools/Function/lexicographic_order.ML
src/HOL/Tools/Function/size.ML
src/HOL/Tools/Function/termination.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Qelim/cooper_data.ML
src/HOL/Tools/Qelim/presburger.ML
src/HOL/Tools/arith_data.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/int_arith.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/nat_arith.ML
src/HOL/Tools/nat_numeral_simprocs.ML
src/HOL/Tools/numeral_simprocs.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/res_clause.ML
src/HOL/Transcendental.thy
src/HOL/ex/Arith_Examples.thy
src/HOL/ex/Binary.thy
src/HOL/ex/SVC_Oracle.thy
src/HOL/ex/svc_funcs.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
src/Provers/Arith/abel_cancel.ML
src/Provers/Arith/cancel_div_mod.ML
     1.1 --- a/NEWS	Thu Jan 28 11:48:43 2010 +0100
     1.2 +++ b/NEWS	Thu Jan 28 11:48:49 2010 +0100
     1.3 @@ -12,6 +12,11 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* new theory Algebras.thy contains generic algebraic structures and
     1.8 +generic algebraic operations.  INCOMPATIBILTY: constants zero, one,
     1.9 +plus, minus, uminus, times, inverse, divide, abs, sgn, less_eq and less
    1.10 +have been moved from HOL.thy to Algebras.thy.
    1.11 +
    1.12  * HOLogic.strip_psplit: types are returned in syntactic order, similar
    1.13  to other strip and tuple operations.  INCOMPATIBILITY.
    1.14  
     2.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Thu Jan 28 11:48:43 2010 +0100
     2.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Thu Jan 28 11:48:49 2010 +0100
     2.3 @@ -205,8 +205,8 @@
     2.4  ML {*
     2.5  fun ring_ord (Const (a, _)) =
     2.6      find_index (fn a' => a = a')
     2.7 -      [@{const_name HOL.zero}, @{const_name HOL.plus}, @{const_name HOL.uminus},
     2.8 -        @{const_name HOL.minus}, @{const_name HOL.one}, @{const_name HOL.times}]
     2.9 +      [@{const_name Algebras.zero}, @{const_name Algebras.plus}, @{const_name Algebras.uminus},
    2.10 +        @{const_name Algebras.minus}, @{const_name Algebras.one}, @{const_name Algebras.times}]
    2.11    | ring_ord _ = ~1;
    2.12  
    2.13  fun termless_ring (a, b) = (TermOrd.term_lpo ring_ord (a, b) = LESS);
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Algebras.thy	Thu Jan 28 11:48:49 2010 +0100
     3.3 @@ -0,0 +1,166 @@
     3.4 +(*  Title:      HOL/Algebras.thy
     3.5 +    Author:     Florian Haftmann, TU Muenchen
     3.6 +*)
     3.7 +
     3.8 +header {* Generic algebraic structures and operations *}
     3.9 +
    3.10 +theory Algebras
    3.11 +imports HOL
    3.12 +begin
    3.13 +
    3.14 +subsection {* Generic algebraic structures *}
    3.15 +
    3.16 +locale semigroup =
    3.17 +  fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
    3.18 +  assumes assoc: "a * b * c = a * (b * c)"
    3.19 +
    3.20 +locale abel_semigroup = semigroup +
    3.21 +  assumes commute: "a * b = b * a"
    3.22 +begin
    3.23 +
    3.24 +lemma left_commute:
    3.25 +  "b * (a * c) = a * (b * c)"
    3.26 +proof -
    3.27 +  have "(b * a) * c = (a * b) * c"
    3.28 +    by (simp only: commute)
    3.29 +  then show ?thesis
    3.30 +    by (simp only: assoc)
    3.31 +qed
    3.32 +
    3.33 +end
    3.34 +
    3.35 +locale semilattice = abel_semigroup +
    3.36 +  assumes idem [simp]: "a * a = a"
    3.37 +begin
    3.38 +
    3.39 +lemma left_idem [simp]:
    3.40 +  "a * (a * b) = a * b"
    3.41 +  by (simp add: assoc [symmetric])
    3.42 +
    3.43 +end
    3.44 +
    3.45 +locale lattice = inf!: abel_semigroup inf + sup!: abel_semigroup sup
    3.46 +  for inf (infixl "\<sqinter>" 70) and sup (infixl "\<squnion>" 70) +
    3.47 +  assumes sup_inf_absorb: "a \<squnion> (a \<sqinter> b) = a"
    3.48 +  and inf_sup_absorb: "a \<sqinter> (a \<squnion> b) = a"
    3.49 +
    3.50 +sublocale lattice < inf!: semilattice inf
    3.51 +proof
    3.52 +  fix a
    3.53 +  have "a \<sqinter> (a \<squnion> (a \<sqinter> a)) = a" by (fact inf_sup_absorb)
    3.54 +  then show "a \<sqinter> a = a" by (simp add: sup_inf_absorb)
    3.55 +qed
    3.56 +
    3.57 +sublocale lattice < sup!: semilattice sup
    3.58 +proof
    3.59 +  fix a
    3.60 +  have "a \<squnion> (a \<sqinter> (a \<squnion> a)) = a" by (fact sup_inf_absorb)
    3.61 +  then show "a \<squnion> a = a" by (simp add: inf_sup_absorb)
    3.62 +qed
    3.63 +
    3.64 +
    3.65 +subsection {* Generic algebraic operations *}
    3.66 +
    3.67 +class zero = 
    3.68 +  fixes zero :: 'a  ("0")
    3.69 +
    3.70 +class one =
    3.71 +  fixes one  :: 'a  ("1")
    3.72 +
    3.73 +lemma Let_0 [simp]: "Let 0 f = f 0"
    3.74 +  unfolding Let_def ..
    3.75 +
    3.76 +lemma Let_1 [simp]: "Let 1 f = f 1"
    3.77 +  unfolding Let_def ..
    3.78 +
    3.79 +setup {*
    3.80 +  Reorient_Proc.add
    3.81 +    (fn Const(@{const_name Algebras.zero}, _) => true
    3.82 +      | Const(@{const_name Algebras.one}, _) => true
    3.83 +      | _ => false)
    3.84 +*}
    3.85 +
    3.86 +simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
    3.87 +simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
    3.88 +
    3.89 +typed_print_translation {*
    3.90 +let
    3.91 +  fun tr' c = (c, fn show_sorts => fn T => fn ts =>
    3.92 +    if (not o null) ts orelse T = dummyT
    3.93 +      orelse not (! show_types) andalso can Term.dest_Type T
    3.94 +    then raise Match
    3.95 +    else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
    3.96 +in map tr' [@{const_syntax Algebras.one}, @{const_syntax Algebras.zero}] end;
    3.97 +*} -- {* show types that are presumably too general *}
    3.98 +
    3.99 +hide (open) const zero one
   3.100 +
   3.101 +class plus =
   3.102 +  fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
   3.103 +
   3.104 +class minus =
   3.105 +  fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
   3.106 +
   3.107 +class uminus =
   3.108 +  fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
   3.109 +
   3.110 +class times =
   3.111 +  fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
   3.112 +
   3.113 +class inverse =
   3.114 +  fixes inverse :: "'a \<Rightarrow> 'a"
   3.115 +    and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
   3.116 +
   3.117 +class abs =
   3.118 +  fixes abs :: "'a \<Rightarrow> 'a"
   3.119 +begin
   3.120 +
   3.121 +notation (xsymbols)
   3.122 +  abs  ("\<bar>_\<bar>")
   3.123 +
   3.124 +notation (HTML output)
   3.125 +  abs  ("\<bar>_\<bar>")
   3.126 +
   3.127 +end
   3.128 +
   3.129 +class sgn =
   3.130 +  fixes sgn :: "'a \<Rightarrow> 'a"
   3.131 +
   3.132 +class ord =
   3.133 +  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   3.134 +    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   3.135 +begin
   3.136 +
   3.137 +notation
   3.138 +  less_eq  ("op <=") and
   3.139 +  less_eq  ("(_/ <= _)" [51, 51] 50) and
   3.140 +  less  ("op <") and
   3.141 +  less  ("(_/ < _)"  [51, 51] 50)
   3.142 +  
   3.143 +notation (xsymbols)
   3.144 +  less_eq  ("op \<le>") and
   3.145 +  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
   3.146 +
   3.147 +notation (HTML output)
   3.148 +  less_eq  ("op \<le>") and
   3.149 +  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
   3.150 +
   3.151 +abbreviation (input)
   3.152 +  greater_eq  (infix ">=" 50) where
   3.153 +  "x >= y \<equiv> y <= x"
   3.154 +
   3.155 +notation (input)
   3.156 +  greater_eq  (infix "\<ge>" 50)
   3.157 +
   3.158 +abbreviation (input)
   3.159 +  greater  (infix ">" 50) where
   3.160 +  "x > y \<equiv> y < x"
   3.161 +
   3.162 +end
   3.163 +
   3.164 +syntax
   3.165 +  "_index1"  :: index    ("\<^sub>1")
   3.166 +translations
   3.167 +  (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
   3.168 +
   3.169 +end
   3.170 \ No newline at end of file
     4.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Jan 28 11:48:43 2010 +0100
     4.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Jan 28 11:48:49 2010 +0100
     4.3 @@ -655,7 +655,7 @@
     4.4      if h aconvc y then false else if h aconvc x then true else earlier t x y;
     4.5  
     4.6  fun dest_frac ct = case term_of ct of
     4.7 -   Const (@{const_name "HOL.divide"},_) $ a $ b=>
     4.8 +   Const (@{const_name Algebras.divide},_) $ a $ b=>
     4.9      Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
    4.10   | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
    4.11   | t => Rat.rat_of_int (snd (HOLogic.dest_number t))
    4.12 @@ -670,13 +670,13 @@
    4.13   end
    4.14  
    4.15  fun whatis x ct = case term_of ct of
    4.16 -  Const(@{const_name "HOL.plus"}, _)$(Const(@{const_name "HOL.times"},_)$_$y)$_ =>
    4.17 +  Const(@{const_name Algebras.plus}, _)$(Const(@{const_name Algebras.times},_)$_$y)$_ =>
    4.18       if y aconv term_of x then ("c*x+t",[(funpow 2 Thm.dest_arg1) ct, Thm.dest_arg ct])
    4.19       else ("Nox",[])
    4.20 -| Const(@{const_name "HOL.plus"}, _)$y$_ =>
    4.21 +| Const(@{const_name Algebras.plus}, _)$y$_ =>
    4.22       if y aconv term_of x then ("x+t",[Thm.dest_arg ct])
    4.23       else ("Nox",[])
    4.24 -| Const(@{const_name "HOL.times"}, _)$_$y =>
    4.25 +| Const(@{const_name Algebras.times}, _)$_$y =>
    4.26       if y aconv term_of x then ("c*x",[Thm.dest_arg1 ct])
    4.27       else ("Nox",[])
    4.28  | t => if t aconv term_of x then ("x",[]) else ("Nox",[]);
    4.29 @@ -684,7 +684,7 @@
    4.30  fun xnormalize_conv ctxt [] ct = reflexive ct
    4.31  | xnormalize_conv ctxt (vs as (x::_)) ct =
    4.32     case term_of ct of
    4.33 -   Const(@{const_name HOL.less},_)$_$Const(@{const_name "HOL.zero"},_) =>
    4.34 +   Const(@{const_name Algebras.less},_)$_$Const(@{const_name Algebras.zero},_) =>
    4.35      (case whatis x (Thm.dest_arg1 ct) of
    4.36      ("c*x+t",[c,t]) =>
    4.37         let
    4.38 @@ -727,7 +727,7 @@
    4.39      | _ => reflexive ct)
    4.40  
    4.41  
    4.42 -|  Const(@{const_name HOL.less_eq},_)$_$Const(@{const_name "HOL.zero"},_) =>
    4.43 +|  Const(@{const_name Algebras.less_eq},_)$_$Const(@{const_name Algebras.zero},_) =>
    4.44     (case whatis x (Thm.dest_arg1 ct) of
    4.45      ("c*x+t",[c,t]) =>
    4.46         let
    4.47 @@ -771,7 +771,7 @@
    4.48        in rth end
    4.49      | _ => reflexive ct)
    4.50  
    4.51 -|  Const("op =",_)$_$Const(@{const_name "HOL.zero"},_) =>
    4.52 +|  Const("op =",_)$_$Const(@{const_name Algebras.zero},_) =>
    4.53     (case whatis x (Thm.dest_arg1 ct) of
    4.54      ("c*x+t",[c,t]) =>
    4.55         let
    4.56 @@ -816,7 +816,7 @@
    4.57    val eq_iff_diff_eq_0 = mk_meta_eq @{thm "eq_iff_diff_eq_0"}
    4.58  in
    4.59  fun field_isolate_conv phi ctxt vs ct = case term_of ct of
    4.60 -  Const(@{const_name HOL.less},_)$a$b =>
    4.61 +  Const(@{const_name Algebras.less},_)$a$b =>
    4.62     let val (ca,cb) = Thm.dest_binop ct
    4.63         val T = ctyp_of_term ca
    4.64         val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
    4.65 @@ -825,7 +825,7 @@
    4.66                (Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
    4.67         val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    4.68     in rth end
    4.69 -| Const(@{const_name HOL.less_eq},_)$a$b =>
    4.70 +| Const(@{const_name Algebras.less_eq},_)$a$b =>
    4.71     let val (ca,cb) = Thm.dest_binop ct
    4.72         val T = ctyp_of_term ca
    4.73         val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
    4.74 @@ -856,11 +856,11 @@
    4.75                              else Ferrante_Rackoff_Data.Nox
    4.76     | @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
    4.77                              else Ferrante_Rackoff_Data.Nox
    4.78 -   | Const(@{const_name HOL.less},_)$y$z =>
    4.79 +   | Const(@{const_name Algebras.less},_)$y$z =>
    4.80         if term_of x aconv y then Ferrante_Rackoff_Data.Lt
    4.81          else if term_of x aconv z then Ferrante_Rackoff_Data.Gt
    4.82          else Ferrante_Rackoff_Data.Nox
    4.83 -   | Const (@{const_name HOL.less_eq},_)$y$z =>
    4.84 +   | Const (@{const_name Algebras.less_eq},_)$y$z =>
    4.85           if term_of x aconv y then Ferrante_Rackoff_Data.Le
    4.86           else if term_of x aconv z then Ferrante_Rackoff_Data.Ge
    4.87           else Ferrante_Rackoff_Data.Nox
     5.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Jan 28 11:48:43 2010 +0100
     5.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Thu Jan 28 11:48:49 2010 +0100
     5.3 @@ -2963,11 +2963,11 @@
     5.4  fun num rT x = HOLogic.mk_number rT x;
     5.5  fun rrelT rT = [rT,rT] ---> rT;
     5.6  fun rrT rT = [rT, rT] ---> bT;
     5.7 -fun divt rT = Const(@{const_name "HOL.divide"},rrelT rT);
     5.8 -fun timest rT = Const(@{const_name "HOL.times"},rrelT rT);
     5.9 -fun plust rT = Const(@{const_name "HOL.plus"},rrelT rT);
    5.10 -fun minust rT = Const(@{const_name "HOL.minus"},rrelT rT);
    5.11 -fun uminust rT = Const(@{const_name "HOL.uminus"}, rT --> rT);
    5.12 +fun divt rT = Const(@{const_name Algebras.divide},rrelT rT);
    5.13 +fun timest rT = Const(@{const_name Algebras.times},rrelT rT);
    5.14 +fun plust rT = Const(@{const_name Algebras.plus},rrelT rT);
    5.15 +fun minust rT = Const(@{const_name Algebras.minus},rrelT rT);
    5.16 +fun uminust rT = Const(@{const_name Algebras.uminus}, rT --> rT);
    5.17  fun powt rT = Const(@{const_name "power"}, [rT,@{typ "nat"}] ---> rT);
    5.18  val brT = [bT, bT] ---> bT;
    5.19  val nott = @{term "Not"};
    5.20 @@ -2975,10 +2975,10 @@
    5.21  val disjt = @{term "op |"};
    5.22  val impt = @{term "op -->"};
    5.23  val ifft = @{term "op = :: bool => _"}
    5.24 -fun llt rT = Const(@{const_name "HOL.less"},rrT rT);
    5.25 -fun lle rT = Const(@{const_name "HOL.less"},rrT rT);
    5.26 +fun llt rT = Const(@{const_name Algebras.less},rrT rT);
    5.27 +fun lle rT = Const(@{const_name Algebras.less},rrT rT);
    5.28  fun eqt rT = Const("op =",rrT rT);
    5.29 -fun rz rT = Const(@{const_name "HOL.zero"},rT);
    5.30 +fun rz rT = Const(@{const_name Algebras.zero},rT);
    5.31  
    5.32  fun dest_nat t = case t of
    5.33    Const ("Suc",_)$t' => 1 + dest_nat t'
    5.34 @@ -2986,21 +2986,21 @@
    5.35  
    5.36  fun num_of_term m t = 
    5.37   case t of
    5.38 -   Const(@{const_name "uminus"},_)$t => FRPar.Neg (num_of_term m t)
    5.39 - | Const(@{const_name "HOL.plus"},_)$a$b => FRPar.Add (num_of_term m a, num_of_term m b)
    5.40 - | Const(@{const_name "HOL.minus"},_)$a$b => FRPar.Sub (num_of_term m a, num_of_term m b)
    5.41 - | Const(@{const_name "HOL.times"},_)$a$b => FRPar.Mul (num_of_term m a, num_of_term m b)
    5.42 - | Const(@{const_name "power"},_)$a$n => FRPar.Pw (num_of_term m a, dest_nat n)
    5.43 - | Const(@{const_name "HOL.divide"},_)$a$b => FRPar.C (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
    5.44 +   Const(@{const_name Algebras.uminus},_)$t => FRPar.Neg (num_of_term m t)
    5.45 + | Const(@{const_name Algebras.plus},_)$a$b => FRPar.Add (num_of_term m a, num_of_term m b)
    5.46 + | Const(@{const_name Algebras.minus},_)$a$b => FRPar.Sub (num_of_term m a, num_of_term m b)
    5.47 + | Const(@{const_name Algebras.times},_)$a$b => FRPar.Mul (num_of_term m a, num_of_term m b)
    5.48 + | Const(@{const_name Power.power},_)$a$n => FRPar.Pw (num_of_term m a, dest_nat n)
    5.49 + | Const(@{const_name Algebras.divide},_)$a$b => FRPar.C (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
    5.50   | _ => (FRPar.C (HOLogic.dest_number t |> snd,1) 
    5.51           handle TERM _ => FRPar.Bound (AList.lookup (op aconv) m t |> the));
    5.52  
    5.53  fun tm_of_term m m' t = 
    5.54   case t of
    5.55 -   Const(@{const_name "uminus"},_)$t => FRPar.tm_Neg (tm_of_term m m' t)
    5.56 - | Const(@{const_name "HOL.plus"},_)$a$b => FRPar.tm_Add (tm_of_term m m' a, tm_of_term m m' b)
    5.57 - | Const(@{const_name "HOL.minus"},_)$a$b => FRPar.tm_Sub (tm_of_term m m' a, tm_of_term m m' b)
    5.58 - | Const(@{const_name "HOL.times"},_)$a$b => FRPar.tm_Mul (num_of_term m' a, tm_of_term m m' b)
    5.59 +   Const(@{const_name Algebras.uminus},_)$t => FRPar.tm_Neg (tm_of_term m m' t)
    5.60 + | Const(@{const_name Algebras.plus},_)$a$b => FRPar.tm_Add (tm_of_term m m' a, tm_of_term m m' b)
    5.61 + | Const(@{const_name Algebras.minus},_)$a$b => FRPar.tm_Sub (tm_of_term m m' a, tm_of_term m m' b)
    5.62 + | Const(@{const_name Algebras.times},_)$a$b => FRPar.tm_Mul (num_of_term m' a, tm_of_term m m' b)
    5.63   | _ => (FRPar.CP (num_of_term m' t) 
    5.64           handle TERM _ => FRPar.tm_Bound (AList.lookup (op aconv) m t |> the)
    5.65                | Option => FRPar.tm_Bound (AList.lookup (op aconv) m t |> the));
    5.66 @@ -3040,9 +3040,9 @@
    5.67    | Const("op =",ty)$p$q => 
    5.68         if domain_type ty = bT then FRPar.Iff(fm_of_term m m' p, fm_of_term m m' q)
    5.69         else FRPar.Eq (FRPar.tm_Sub(tm_of_term m m' p, tm_of_term m m' q))
    5.70 -  | Const(@{const_name "HOL.less"},_)$p$q => 
    5.71 +  | Const(@{const_name Algebras.less},_)$p$q => 
    5.72          FRPar.Lt (FRPar.tm_Sub(tm_of_term m m' p, tm_of_term m m' q))
    5.73 -  | Const(@{const_name "HOL.less_eq"},_)$p$q => 
    5.74 +  | Const(@{const_name Algebras.less_eq},_)$p$q => 
    5.75          FRPar.Le (FRPar.tm_Sub(tm_of_term m m' p, tm_of_term m m' q))
    5.76    | Const("Ex",_)$Abs(xn,xT,p) => 
    5.77       let val (xn', p') =  variant_abs (xn,xT,p)
     6.1 --- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Thu Jan 28 11:48:43 2010 +0100
     6.2 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Thu Jan 28 11:48:49 2010 +0100
     6.3 @@ -13,8 +13,8 @@
     6.4  struct
     6.5  
     6.6  (* Zero and One of the commutative ring *)
     6.7 -fun cring_zero T = Const (@{const_name HOL.zero}, T);
     6.8 -fun cring_one T = Const (@{const_name HOL.one}, T);
     6.9 +fun cring_zero T = Const (@{const_name Algebras.zero}, T);
    6.10 +fun cring_one T = Const (@{const_name Algebras.one}, T);
    6.11  
    6.12  (* reification functions *)
    6.13  (* add two polynom expressions *)
    6.14 @@ -49,13 +49,13 @@
    6.15    | reif_pol T vs t = pol_Pc T $ t;
    6.16  
    6.17  (* reification of polynom expressions *)
    6.18 -fun reif_polex T vs (Const (@{const_name HOL.plus}, _) $ a $ b) =
    6.19 +fun reif_polex T vs (Const (@{const_name Algebras.plus}, _) $ a $ b) =
    6.20        polex_add T $ reif_polex T vs a $ reif_polex T vs b
    6.21 -  | reif_polex T vs (Const (@{const_name HOL.minus}, _) $ a $ b) =
    6.22 +  | reif_polex T vs (Const (@{const_name Algebras.minus}, _) $ a $ b) =
    6.23        polex_sub T $ reif_polex T vs a $ reif_polex T vs b
    6.24 -  | reif_polex T vs (Const (@{const_name HOL.times}, _) $ a $ b) =
    6.25 +  | reif_polex T vs (Const (@{const_name Algebras.times}, _) $ a $ b) =
    6.26        polex_mul T $ reif_polex T vs a $ reif_polex T vs b
    6.27 -  | reif_polex T vs (Const (@{const_name HOL.uminus}, _) $ a) =
    6.28 +  | reif_polex T vs (Const (@{const_name Algebras.uminus}, _) $ a) =
    6.29        polex_neg T $ reif_polex T vs a
    6.30    | reif_polex T vs (Const (@{const_name Power.power}, _) $ a $ n) =
    6.31        polex_pow T $ reif_polex T vs a $ n
     7.1 --- a/src/HOL/Groebner_Basis.thy	Thu Jan 28 11:48:43 2010 +0100
     7.2 +++ b/src/HOL/Groebner_Basis.thy	Thu Jan 28 11:48:49 2010 +0100
     7.3 @@ -527,13 +527,13 @@
     7.4      val (l,r) = Thm.dest_binop ct
     7.5      val T = ctyp_of_term l
     7.6    in (case (term_of l, term_of r) of
     7.7 -      (Const(@{const_name "HOL.divide"},_)$_$_, _) =>
     7.8 +      (Const(@{const_name Algebras.divide},_)$_$_, _) =>
     7.9          let val (x,y) = Thm.dest_binop l val z = r
    7.10              val _ = map (HOLogic.dest_number o term_of) [x,y,z]
    7.11              val ynz = prove_nz ss T y
    7.12          in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
    7.13          end
    7.14 -     | (_, Const (@{const_name "HOL.divide"},_)$_$_) =>
    7.15 +     | (_, Const (@{const_name Algebras.divide},_)$_$_) =>
    7.16          let val (x,y) = Thm.dest_binop r val z = l
    7.17              val _ = map (HOLogic.dest_number o term_of) [x,y,z]
    7.18              val ynz = prove_nz ss T y
    7.19 @@ -543,49 +543,49 @@
    7.20    end
    7.21    handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
    7.22  
    7.23 - fun is_number (Const(@{const_name "HOL.divide"},_)$a$b) = is_number a andalso is_number b
    7.24 + fun is_number (Const(@{const_name Algebras.divide},_)$a$b) = is_number a andalso is_number b
    7.25     | is_number t = can HOLogic.dest_number t
    7.26  
    7.27   val is_number = is_number o term_of
    7.28  
    7.29   fun proc3 phi ss ct =
    7.30    (case term_of ct of
    7.31 -    Const(@{const_name HOL.less},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
    7.32 +    Const(@{const_name Algebras.less},_)$(Const(@{const_name Algebras.divide},_)$_$_)$_ =>
    7.33        let
    7.34          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
    7.35          val _ = map is_number [a,b,c]
    7.36          val T = ctyp_of_term c
    7.37          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
    7.38        in SOME (mk_meta_eq th) end
    7.39 -  | Const(@{const_name HOL.less_eq},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
    7.40 +  | Const(@{const_name Algebras.less_eq},_)$(Const(@{const_name Algebras.divide},_)$_$_)$_ =>
    7.41        let
    7.42          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
    7.43          val _ = map is_number [a,b,c]
    7.44          val T = ctyp_of_term c
    7.45          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
    7.46        in SOME (mk_meta_eq th) end
    7.47 -  | Const("op =",_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
    7.48 +  | Const("op =",_)$(Const(@{const_name Algebras.divide},_)$_$_)$_ =>
    7.49        let
    7.50          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
    7.51          val _ = map is_number [a,b,c]
    7.52          val T = ctyp_of_term c
    7.53          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
    7.54        in SOME (mk_meta_eq th) end
    7.55 -  | Const(@{const_name HOL.less},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
    7.56 +  | Const(@{const_name Algebras.less},_)$_$(Const(@{const_name Algebras.divide},_)$_$_) =>
    7.57      let
    7.58        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
    7.59          val _ = map is_number [a,b,c]
    7.60          val T = ctyp_of_term c
    7.61          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
    7.62        in SOME (mk_meta_eq th) end
    7.63 -  | Const(@{const_name HOL.less_eq},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
    7.64 +  | Const(@{const_name Algebras.less_eq},_)$_$(Const(@{const_name Algebras.divide},_)$_$_) =>
    7.65      let
    7.66        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
    7.67          val _ = map is_number [a,b,c]
    7.68          val T = ctyp_of_term c
    7.69          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
    7.70        in SOME (mk_meta_eq th) end
    7.71 -  | Const("op =",_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
    7.72 +  | Const("op =",_)$_$(Const(@{const_name Algebras.divide},_)$_$_) =>
    7.73      let
    7.74        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
    7.75          val _ = map is_number [a,b,c]
    7.76 @@ -645,15 +645,15 @@
    7.77  
    7.78  fun numeral_is_const ct =
    7.79    case term_of ct of
    7.80 -   Const (@{const_name "HOL.divide"},_) $ a $ b =>
    7.81 +   Const (@{const_name Algebras.divide},_) $ a $ b =>
    7.82       can HOLogic.dest_number a andalso can HOLogic.dest_number b
    7.83 - | Const (@{const_name "HOL.inverse"},_)$t => can HOLogic.dest_number t
    7.84 + | Const (@{const_name Algebras.inverse},_)$t => can HOLogic.dest_number t
    7.85   | t => can HOLogic.dest_number t
    7.86  
    7.87  fun dest_const ct = ((case term_of ct of
    7.88 -   Const (@{const_name "HOL.divide"},_) $ a $ b=>
    7.89 +   Const (@{const_name Algebras.divide},_) $ a $ b=>
    7.90      Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b))
    7.91 - | Const (@{const_name "HOL.inverse"},_)$t => 
    7.92 + | Const (@{const_name Algebras.inverse},_)$t => 
    7.93                 Rat.inv (Rat.rat_of_int (snd (HOLogic.dest_number t)))
    7.94   | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) 
    7.95     handle TERM _ => error "ring_dest_const")
     8.1 --- a/src/HOL/HOL.thy	Thu Jan 28 11:48:43 2010 +0100
     8.2 +++ b/src/HOL/HOL.thy	Thu Jan 28 11:48:49 2010 +0100
     8.3 @@ -1625,118 +1625,6 @@
     8.4  by blast+
     8.5  
     8.6  
     8.7 -subsection {* Generic classes and algebraic operations *}
     8.8 -
     8.9 -class zero = 
    8.10 -  fixes zero :: 'a  ("0")
    8.11 -
    8.12 -class one =
    8.13 -  fixes one  :: 'a  ("1")
    8.14 -
    8.15 -lemma Let_0 [simp]: "Let 0 f = f 0"
    8.16 -  unfolding Let_def ..
    8.17 -
    8.18 -lemma Let_1 [simp]: "Let 1 f = f 1"
    8.19 -  unfolding Let_def ..
    8.20 -
    8.21 -setup {*
    8.22 -  Reorient_Proc.add
    8.23 -    (fn Const(@{const_name HOL.zero}, _) => true
    8.24 -      | Const(@{const_name HOL.one}, _) => true
    8.25 -      | _ => false)
    8.26 -*}
    8.27 -
    8.28 -simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
    8.29 -simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
    8.30 -
    8.31 -typed_print_translation {*
    8.32 -let
    8.33 -  fun tr' c = (c, fn show_sorts => fn T => fn ts =>
    8.34 -    if (not o null) ts orelse T = dummyT
    8.35 -      orelse not (! show_types) andalso can Term.dest_Type T
    8.36 -    then raise Match
    8.37 -    else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
    8.38 -in map tr' [@{const_syntax HOL.one}, @{const_syntax HOL.zero}] end;
    8.39 -*} -- {* show types that are presumably too general *}
    8.40 -
    8.41 -hide (open) const zero one
    8.42 -
    8.43 -class plus =
    8.44 -  fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
    8.45 -
    8.46 -class minus =
    8.47 -  fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
    8.48 -
    8.49 -class uminus =
    8.50 -  fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
    8.51 -
    8.52 -class times =
    8.53 -  fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
    8.54 -
    8.55 -class inverse =
    8.56 -  fixes inverse :: "'a \<Rightarrow> 'a"
    8.57 -    and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
    8.58 -
    8.59 -class abs =
    8.60 -  fixes abs :: "'a \<Rightarrow> 'a"
    8.61 -begin
    8.62 -
    8.63 -notation (xsymbols)
    8.64 -  abs  ("\<bar>_\<bar>")
    8.65 -
    8.66 -notation (HTML output)
    8.67 -  abs  ("\<bar>_\<bar>")
    8.68 -
    8.69 -end
    8.70 -
    8.71 -class sgn =
    8.72 -  fixes sgn :: "'a \<Rightarrow> 'a"
    8.73 -
    8.74 -class ord =
    8.75 -  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    8.76 -    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    8.77 -begin
    8.78 -
    8.79 -notation
    8.80 -  less_eq  ("op <=") and
    8.81 -  less_eq  ("(_/ <= _)" [51, 51] 50) and
    8.82 -  less  ("op <") and
    8.83 -  less  ("(_/ < _)"  [51, 51] 50)
    8.84 -  
    8.85 -notation (xsymbols)
    8.86 -  less_eq  ("op \<le>") and
    8.87 -  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
    8.88 -
    8.89 -notation (HTML output)
    8.90 -  less_eq  ("op \<le>") and
    8.91 -  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
    8.92 -
    8.93 -abbreviation (input)
    8.94 -  greater_eq  (infix ">=" 50) where
    8.95 -  "x >= y \<equiv> y <= x"
    8.96 -
    8.97 -notation (input)
    8.98 -  greater_eq  (infix "\<ge>" 50)
    8.99 -
   8.100 -abbreviation (input)
   8.101 -  greater  (infix ">" 50) where
   8.102 -  "x > y \<equiv> y < x"
   8.103 -
   8.104 -end
   8.105 -
   8.106 -syntax
   8.107 -  "_index1"  :: index    ("\<^sub>1")
   8.108 -translations
   8.109 -  (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
   8.110 -
   8.111 -lemma mk_left_commute:
   8.112 -  fixes f (infix "\<otimes>" 60)
   8.113 -  assumes a: "\<And>x y z. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)" and
   8.114 -          c: "\<And>x y. x \<otimes> y = y \<otimes> x"
   8.115 -  shows "x \<otimes> (y \<otimes> z) = y \<otimes> (x \<otimes> z)"
   8.116 -  by (rule trans [OF trans [OF c a] arg_cong [OF c, of "f y"]])
   8.117 -
   8.118 -
   8.119  subsection {* Basic ML bindings *}
   8.120  
   8.121  ML {*
     9.1 --- a/src/HOL/Hoare/hoare_tac.ML	Thu Jan 28 11:48:43 2010 +0100
     9.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Thu Jan 28 11:48:49 2010 +0100
     9.3 @@ -58,7 +58,7 @@
     9.4    let val T as Type ("fun",[t,_]) = fastype_of trm
     9.5    in Collect_const t $ trm end;
     9.6  
     9.7 -fun inclt ty = Const (@{const_name HOL.less_eq}, [ty,ty] ---> boolT);
     9.8 +fun inclt ty = Const (@{const_name Algebras.less_eq}, [ty,ty] ---> boolT);
     9.9  
    9.10  
    9.11  fun Mset ctxt prop =
    10.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Thu Jan 28 11:48:43 2010 +0100
    10.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Thu Jan 28 11:48:49 2010 +0100
    10.3 @@ -166,7 +166,7 @@
    10.4  import_theory prim_rec;
    10.5  
    10.6  const_maps
    10.7 -    "<" > HOL.ord_class.less :: "[nat,nat]=>bool";
    10.8 +    "<" > Algebras.less :: "[nat,nat]=>bool";
    10.9  
   10.10  end_import;
   10.11  
   10.12 @@ -181,15 +181,15 @@
   10.13    ">"          > HOL4Compat.nat_gt
   10.14    ">="         > HOL4Compat.nat_ge
   10.15    FUNPOW       > HOL4Compat.FUNPOW
   10.16 -  "<="         > HOL.ord_class.less_eq :: "[nat,nat]=>bool"
   10.17 -  "+"          > HOL.plus_class.plus       :: "[nat,nat]=>nat"
   10.18 -  "*"          > HOL.times_class.times      :: "[nat,nat]=>nat"
   10.19 -  "-"          > HOL.minus_class.minus      :: "[nat,nat]=>nat"
   10.20 -  MIN          > Orderings.ord_class.min    :: "[nat,nat]=>nat"
   10.21 -  MAX          > Orderings.ord_class.max    :: "[nat,nat]=>nat"
   10.22 -  DIV          > Divides.div_class.div :: "[nat,nat]=>nat"
   10.23 -  MOD          > Divides.div_class.mod :: "[nat,nat]=>nat"
   10.24 -  EXP          > Power.power_class.power :: "[nat,nat]=>nat";
   10.25 +  "<="         > Algebras.less_eq :: "[nat,nat]=>bool"
   10.26 +  "+"          > Algebras.plus :: "[nat,nat]=>nat"
   10.27 +  "*"          > Algebras.times :: "[nat,nat]=>nat"
   10.28 +  "-"          > Algebras.minus :: "[nat,nat]=>nat"
   10.29 +  MIN          > Orderings.min :: "[nat,nat]=>nat"
   10.30 +  MAX          > Orderings.max :: "[nat,nat]=>nat"
   10.31 +  DIV          > Divides.div :: "[nat,nat]=>nat"
   10.32 +  MOD          > Divides.mod :: "[nat,nat]=>nat"
   10.33 +  EXP          > Power.power :: "[nat,nat]=>nat";
   10.34  
   10.35  end_import;
   10.36  
    11.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Thu Jan 28 11:48:43 2010 +0100
    11.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Thu Jan 28 11:48:49 2010 +0100
    11.3 @@ -1,5 +1,4 @@
    11.4  (*  Title:      HOL/Import/Generate-HOL/GenHOL4Real.thy
    11.5 -    ID:         $Id$
    11.6      Author:     Sebastian Skalberg (TU Muenchen)
    11.7  *)
    11.8  
    11.9 @@ -17,13 +16,13 @@
   11.10    real > RealDef.real;
   11.11  
   11.12  const_maps
   11.13 -  real_0   > 0           :: real
   11.14 -  real_1   > 1           :: real
   11.15 -  real_neg > uminus      :: "real => real"
   11.16 -  inv      > HOL.inverse :: "real => real"
   11.17 -  real_add > HOL.plus    :: "[real,real] => real"
   11.18 -  real_mul > HOL.times   :: "[real,real] => real"
   11.19 -  real_lt  > HOL.ord_class.less :: "[real,real] => bool";
   11.20 +  real_0   > Algebras.zero      :: real
   11.21 +  real_1   > Algebras.one       :: real
   11.22 +  real_neg > Algebras.uminus    :: "real => real"
   11.23 +  inv      > Algebras.inverse   :: "real => real"
   11.24 +  real_add > Algebras.plus      :: "[real,real] => real"
   11.25 +  real_mul > Algebras.times     :: "[real,real] => real"
   11.26 +  real_lt  > Algebras.less      :: "[real,real] => bool";
   11.27  
   11.28  ignore_thms
   11.29      real_TY_DEF
   11.30 @@ -51,11 +50,11 @@
   11.31  const_maps
   11.32    real_gt     > HOL4Compat.real_gt
   11.33    real_ge     > HOL4Compat.real_ge
   11.34 -  real_lte    > HOL.ord_class.less_eq :: "[real,real] => bool"
   11.35 -  real_sub    > HOL.minus    :: "[real,real] => real"
   11.36 -  "/"         > HOL.divide   :: "[real,real] => real"
   11.37 -  pow         > Power.power_class.power    :: "[real,nat] => real"
   11.38 -  abs         > HOL.abs      :: "real => real"
   11.39 +  real_lte    > Algebras.less_eq :: "[real,real] => bool"
   11.40 +  real_sub    > Algebras.minus :: "[real,real] => real"
   11.41 +  "/"         > Algebras.divide :: "[real,real] => real"
   11.42 +  pow         > Power.power :: "[real,nat] => real"
   11.43 +  abs         > Algebras.abs :: "real => real"
   11.44    real_of_num > RealDef.real :: "nat => real";
   11.45  
   11.46  end_import;
    12.1 --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Thu Jan 28 11:48:43 2010 +0100
    12.2 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Thu Jan 28 11:48:49 2010 +0100
    12.3 @@ -76,9 +76,9 @@
    12.4    SUC > Suc
    12.5    PRE > HOLLightCompat.Pred
    12.6    NUMERAL > HOL4Compat.NUMERAL
    12.7 -  "+" > HOL.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
    12.8 -  "*" > HOL.times :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    12.9 -  "-" > HOL.minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   12.10 +  "+" > Algebras.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
   12.11 +  "*" > Algebras.times :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   12.12 +  "-" > Algebras.minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   12.13    BIT0 > HOLLightCompat.NUMERAL_BIT0
   12.14    BIT1 > HOL4Compat.NUMERAL_BIT1
   12.15    INL > Sum_Type.Inl
    13.1 --- a/src/HOL/Import/HOL/arithmetic.imp	Thu Jan 28 11:48:43 2010 +0100
    13.2 +++ b/src/HOL/Import/HOL/arithmetic.imp	Thu Jan 28 11:48:49 2010 +0100
    13.3 @@ -23,10 +23,10 @@
    13.4    "ALT_ZERO" > "HOL4Compat.ALT_ZERO"
    13.5    ">=" > "HOL4Compat.nat_ge"
    13.6    ">" > "HOL4Compat.nat_gt"
    13.7 -  "<=" > "HOL.ord_class.less_eq" :: "nat => nat => bool"
    13.8 -  "-" > "HOL.minus_class.minus" :: "nat => nat => nat"
    13.9 -  "+" > "HOL.plus_class.plus" :: "nat => nat => nat"
   13.10 -  "*" > "HOL.times_class.times" :: "nat => nat => nat"
   13.11 +  "<=" > "Algebras.ord_class.less_eq" :: "nat => nat => bool"
   13.12 +  "-" > "Algebras.minus_class.minus" :: "nat => nat => nat"
   13.13 +  "+" > "Algebras.plus_class.plus" :: "nat => nat => nat"
   13.14 +  "*" > "Algebras.times_class.times" :: "nat => nat => nat"
   13.15  
   13.16  thm_maps
   13.17    "num_case_def" > "HOL4Compat.num_case_def"
    14.1 --- a/src/HOL/Import/HOL/prim_rec.imp	Thu Jan 28 11:48:43 2010 +0100
    14.2 +++ b/src/HOL/Import/HOL/prim_rec.imp	Thu Jan 28 11:48:49 2010 +0100
    14.3 @@ -18,7 +18,7 @@
    14.4    "PRIM_REC_FUN" > "HOL4Base.prim_rec.PRIM_REC_FUN"
    14.5    "PRIM_REC" > "HOL4Base.prim_rec.PRIM_REC"
    14.6    "PRE" > "HOL4Base.prim_rec.PRE"
    14.7 -  "<" > "HOL.ord_class.less" :: "nat => nat => bool"
    14.8 +  "<" > "Algebras.less" :: "nat => nat => bool"
    14.9  
   14.10  thm_maps
   14.11    "wellfounded_primdef" > "HOL4Base.prim_rec.wellfounded_primdef"
    15.1 --- a/src/HOL/Import/HOL/real.imp	Thu Jan 28 11:48:43 2010 +0100
    15.2 +++ b/src/HOL/Import/HOL/real.imp	Thu Jan 28 11:48:49 2010 +0100
    15.3 @@ -10,14 +10,14 @@
    15.4  const_maps
    15.5    "sup" > "HOL4Real.real.sup"
    15.6    "sum" > "HOL4Real.real.sum"
    15.7 -  "real_sub" > "HOL.minus_class.minus" :: "real => real => real"
    15.8 +  "real_sub" > "Algebras.minus" :: "real => real => real"
    15.9    "real_of_num" > "RealDef.real" :: "nat => real"
   15.10 -  "real_lte" > "HOL.ord_class.less_eq" :: "real => real => bool"
   15.11 +  "real_lte" > "Algebras.less_eq" :: "real => real => bool"
   15.12    "real_gt" > "HOL4Compat.real_gt"
   15.13    "real_ge" > "HOL4Compat.real_ge"
   15.14    "pow" > "Power.power_class.power" :: "real => nat => real"
   15.15 -  "abs" > "HOL.minus_class.abs" :: "real => real"
   15.16 -  "/" > "HOL.divides_class.divide" :: "real => real => real"
   15.17 +  "abs" > "Algebras.abs" :: "real => real"
   15.18 +  "/" > "Algebras.divide" :: "real => real => real"
   15.19  
   15.20  thm_maps
   15.21    "sup_def" > "HOL4Real.real.sup_def"
    16.1 --- a/src/HOL/Import/HOL/realax.imp	Thu Jan 28 11:48:43 2010 +0100
    16.2 +++ b/src/HOL/Import/HOL/realax.imp	Thu Jan 28 11:48:49 2010 +0100
    16.3 @@ -27,13 +27,13 @@
    16.4    "treal_add" > "HOL4Real.realax.treal_add"
    16.5    "treal_1" > "HOL4Real.realax.treal_1"
    16.6    "treal_0" > "HOL4Real.realax.treal_0"
    16.7 -  "real_neg" > "HOL.uminus_class.uminus" :: "real => real"
    16.8 -  "real_mul" > "HOL.times_class.times" :: "real => real => real"
    16.9 -  "real_lt" > "HOL.ord_class.less" :: "real => real => bool"
   16.10 -  "real_add" > "HOL.plus_class.plus" :: "real => real => real"
   16.11 -  "real_1" > "HOL.one_class.one" :: "real"
   16.12 -  "real_0" > "HOL.zero_class.zero" :: "real"
   16.13 -  "inv" > "HOL.divide_class.inverse" :: "real => real"
   16.14 +  "real_neg" > "Algebras.uminus_class.uminus" :: "real => real"
   16.15 +  "real_mul" > "Algebras.times_class.times" :: "real => real => real"
   16.16 +  "real_lt" > "Algebras.ord_class.less" :: "real => real => bool"
   16.17 +  "real_add" > "Algebras.plus_class.plus" :: "real => real => real"
   16.18 +  "real_1" > "Algebras.one_class.one" :: "real"
   16.19 +  "real_0" > "Algebras.zero_class.zero" :: "real"
   16.20 +  "inv" > "Algebras.divide_class.inverse" :: "real => real"
   16.21    "hreal_of_treal" > "HOL4Real.realax.hreal_of_treal"
   16.22  
   16.23  thm_maps
    17.1 --- a/src/HOL/Import/HOLLight/HOLLight.thy	Thu Jan 28 11:48:43 2010 +0100
    17.2 +++ b/src/HOL/Import/HOLLight/HOLLight.thy	Thu Jan 28 11:48:49 2010 +0100
    17.3 @@ -1119,37 +1119,37 @@
    17.4     (%x::nat.
    17.5         (All::(nat => bool) => bool)
    17.6          (%xa::nat.
    17.7 -            (op =::nat => nat => bool) ((HOL.plus::nat => nat => nat) x xa)
    17.8 -             ((HOL.plus::nat => nat => nat) x xa))))
    17.9 +            (op =::nat => nat => bool) ((plus::nat => nat => nat) x xa)
   17.10 +             ((plus::nat => nat => nat) x xa))))
   17.11   ((op &::bool => bool => bool)
   17.12 -   ((op =::nat => nat => bool) ((HOL.plus::nat => nat => nat) (0::nat) (0::nat))
   17.13 +   ((op =::nat => nat => bool) ((plus::nat => nat => nat) (0::nat) (0::nat))
   17.14       (0::nat))
   17.15     ((op &::bool => bool => bool)
   17.16       ((All::(nat => bool) => bool)
   17.17         (%x::nat.
   17.18             (op =::nat => nat => bool)
   17.19 -            ((HOL.plus::nat => nat => nat) (0::nat)
   17.20 +            ((plus::nat => nat => nat) (0::nat)
   17.21                ((NUMERAL_BIT0::nat => nat) x))
   17.22              ((NUMERAL_BIT0::nat => nat) x)))
   17.23       ((op &::bool => bool => bool)
   17.24         ((All::(nat => bool) => bool)
   17.25           (%x::nat.
   17.26               (op =::nat => nat => bool)
   17.27 -              ((HOL.plus::nat => nat => nat) (0::nat)
   17.28 +              ((plus::nat => nat => nat) (0::nat)
   17.29                  ((NUMERAL_BIT1::nat => nat) x))
   17.30                ((NUMERAL_BIT1::nat => nat) x)))
   17.31         ((op &::bool => bool => bool)
   17.32           ((All::(nat => bool) => bool)
   17.33             (%x::nat.
   17.34                 (op =::nat => nat => bool)
   17.35 -                ((HOL.plus::nat => nat => nat) ((NUMERAL_BIT0::nat => nat) x)
   17.36 +                ((plus::nat => nat => nat) ((NUMERAL_BIT0::nat => nat) x)
   17.37                    (0::nat))
   17.38                  ((NUMERAL_BIT0::nat => nat) x)))
   17.39           ((op &::bool => bool => bool)
   17.40             ((All::(nat => bool) => bool)
   17.41               (%x::nat.
   17.42                   (op =::nat => nat => bool)
   17.43 -                  ((HOL.plus::nat => nat => nat) ((NUMERAL_BIT1::nat => nat) x)
   17.44 +                  ((plus::nat => nat => nat) ((NUMERAL_BIT1::nat => nat) x)
   17.45                      (0::nat))
   17.46                    ((NUMERAL_BIT1::nat => nat) x)))
   17.47             ((op &::bool => bool => bool)
   17.48 @@ -1158,44 +1158,44 @@
   17.49                     (All::(nat => bool) => bool)
   17.50                      (%xa::nat.
   17.51                          (op =::nat => nat => bool)
   17.52 -                         ((HOL.plus::nat => nat => nat)
   17.53 +                         ((plus::nat => nat => nat)
   17.54                             ((NUMERAL_BIT0::nat => nat) x)
   17.55                             ((NUMERAL_BIT0::nat => nat) xa))
   17.56                           ((NUMERAL_BIT0::nat => nat)
   17.57 -                           ((HOL.plus::nat => nat => nat) x xa)))))
   17.58 +                           ((plus::nat => nat => nat) x xa)))))
   17.59               ((op &::bool => bool => bool)
   17.60                 ((All::(nat => bool) => bool)
   17.61                   (%x::nat.
   17.62                       (All::(nat => bool) => bool)
   17.63                        (%xa::nat.
   17.64                            (op =::nat => nat => bool)
   17.65 -                           ((HOL.plus::nat => nat => nat)
   17.66 +                           ((plus::nat => nat => nat)
   17.67                               ((NUMERAL_BIT0::nat => nat) x)
   17.68                               ((NUMERAL_BIT1::nat => nat) xa))
   17.69                             ((NUMERAL_BIT1::nat => nat)
   17.70 -                             ((HOL.plus::nat => nat => nat) x xa)))))
   17.71 +                             ((plus::nat => nat => nat) x xa)))))
   17.72                 ((op &::bool => bool => bool)
   17.73                   ((All::(nat => bool) => bool)
   17.74                     (%x::nat.
   17.75                         (All::(nat => bool) => bool)
   17.76                          (%xa::nat.
   17.77                              (op =::nat => nat => bool)
   17.78 -                             ((HOL.plus::nat => nat => nat)
   17.79 +                             ((plus::nat => nat => nat)
   17.80                                 ((NUMERAL_BIT1::nat => nat) x)
   17.81                                 ((NUMERAL_BIT0::nat => nat) xa))
   17.82                               ((NUMERAL_BIT1::nat => nat)
   17.83 -                               ((HOL.plus::nat => nat => nat) x xa)))))
   17.84 +                               ((plus::nat => nat => nat) x xa)))))
   17.85                   ((All::(nat => bool) => bool)
   17.86                     (%x::nat.
   17.87                         (All::(nat => bool) => bool)
   17.88                          (%xa::nat.
   17.89                              (op =::nat => nat => bool)
   17.90 -                             ((HOL.plus::nat => nat => nat)
   17.91 +                             ((plus::nat => nat => nat)
   17.92                                 ((NUMERAL_BIT1::nat => nat) x)
   17.93                                 ((NUMERAL_BIT1::nat => nat) xa))
   17.94                               ((NUMERAL_BIT0::nat => nat)
   17.95                                 ((Suc::nat => nat)
   17.96 -                                 ((HOL.plus::nat => nat => nat) x
   17.97 +                                 ((plus::nat => nat => nat) x
   17.98                                     xa))))))))))))))"
   17.99    by (import hollight ARITH_ADD)
  17.100  
  17.101 @@ -1258,7 +1258,7 @@
  17.102                             ((op *::nat => nat => nat)
  17.103                               ((NUMERAL_BIT0::nat => nat) x)
  17.104                               ((NUMERAL_BIT1::nat => nat) xa))
  17.105 -                           ((HOL.plus::nat => nat => nat)
  17.106 +                           ((plus::nat => nat => nat)
  17.107                               ((NUMERAL_BIT0::nat => nat) x)
  17.108                               ((NUMERAL_BIT0::nat => nat)
  17.109                                 ((NUMERAL_BIT0::nat => nat)
  17.110 @@ -1272,7 +1272,7 @@
  17.111                               ((op *::nat => nat => nat)
  17.112                                 ((NUMERAL_BIT1::nat => nat) x)
  17.113                                 ((NUMERAL_BIT0::nat => nat) xa))
  17.114 -                             ((HOL.plus::nat => nat => nat)
  17.115 +                             ((plus::nat => nat => nat)
  17.116                                 ((NUMERAL_BIT0::nat => nat) xa)
  17.117                                 ((NUMERAL_BIT0::nat => nat)
  17.118                                   ((NUMERAL_BIT0::nat => nat)
  17.119 @@ -1285,9 +1285,9 @@
  17.120                               ((op *::nat => nat => nat)
  17.121                                 ((NUMERAL_BIT1::nat => nat) x)
  17.122                                 ((NUMERAL_BIT1::nat => nat) xa))
  17.123 -                             ((HOL.plus::nat => nat => nat)
  17.124 +                             ((plus::nat => nat => nat)
  17.125                                 ((NUMERAL_BIT1::nat => nat) x)
  17.126 -                               ((HOL.plus::nat => nat => nat)
  17.127 +                               ((plus::nat => nat => nat)
  17.128                                   ((NUMERAL_BIT0::nat => nat) xa)
  17.129                                   ((NUMERAL_BIT0::nat => nat)
  17.130                                     ((NUMERAL_BIT0::nat => nat)
  17.131 @@ -7462,7 +7462,7 @@
  17.132        (%i::nat.
  17.133            ($::('A::type, ('M::type, 'N::type) finite_sum) cart
  17.134                => nat => 'A::type)
  17.135 -           u ((HOL.plus::nat => nat => nat) i
  17.136 +           u ((plus::nat => nat => nat) i
  17.137                 ((dimindex::('M::type => bool) => nat)
  17.138                   (hollight.UNIV::'M::type => bool)))))"
  17.139  
  17.140 @@ -7478,14 +7478,14 @@
  17.141        (%i::nat.
  17.142            ($::('A::type, ('M::type, 'N::type) finite_sum) cart
  17.143                => nat => 'A::type)
  17.144 -           u ((HOL.plus::nat => nat => nat) i
  17.145 +           u ((plus::nat => nat => nat) i
  17.146                 ((dimindex::('M::type => bool) => nat)
  17.147                   (hollight.UNIV::'M::type => bool)))))"
  17.148    by (import hollight DEF_sndcart)
  17.149  
  17.150  lemma DIMINDEX_HAS_SIZE_FINITE_SUM: "(HAS_SIZE::(('M::type, 'N::type) finite_sum => bool) => nat => bool)
  17.151   (hollight.UNIV::('M::type, 'N::type) finite_sum => bool)
  17.152 - ((HOL.plus::nat => nat => nat)
  17.153 + ((plus::nat => nat => nat)
  17.154     ((dimindex::('M::type => bool) => nat) (hollight.UNIV::'M::type => bool))
  17.155     ((dimindex::('N::type => bool) => nat)
  17.156       (hollight.UNIV::'N::type => bool)))"
  17.157 @@ -7494,7 +7494,7 @@
  17.158  lemma DIMINDEX_FINITE_SUM: "(op =::nat => nat => bool)
  17.159   ((dimindex::(('M::type, 'N::type) finite_sum => bool) => nat)
  17.160     (hollight.UNIV::('M::type, 'N::type) finite_sum => bool))
  17.161 - ((HOL.plus::nat => nat => nat)
  17.162 + ((plus::nat => nat => nat)
  17.163     ((dimindex::('M::type => bool) => nat) (hollight.UNIV::'M::type => bool))
  17.164     ((dimindex::('N::type => bool) => nat)
  17.165       (hollight.UNIV::'N::type => bool)))"
  17.166 @@ -8025,7 +8025,7 @@
  17.167   (nsum::('q_51017::type => bool) => ('q_51017::type => nat) => nat)
  17.168   ((iterate::(nat => nat => nat)
  17.169              => ('q_51017::type => bool) => ('q_51017::type => nat) => nat)
  17.170 -   (HOL.plus::nat => nat => nat))"
  17.171 +   (plus::nat => nat => nat))"
  17.172  
  17.173  lemma DEF_nsum: "(op =::(('q_51017::type => bool) => ('q_51017::type => nat) => nat)
  17.174         => (('q_51017::type => bool) => ('q_51017::type => nat) => nat)
  17.175 @@ -8033,17 +8033,17 @@
  17.176   (nsum::('q_51017::type => bool) => ('q_51017::type => nat) => nat)
  17.177   ((iterate::(nat => nat => nat)
  17.178              => ('q_51017::type => bool) => ('q_51017::type => nat) => nat)
  17.179 -   (HOL.plus::nat => nat => nat))"
  17.180 +   (plus::nat => nat => nat))"
  17.181    by (import hollight DEF_nsum)
  17.182  
  17.183  lemma NEUTRAL_ADD: "(op =::nat => nat => bool)
  17.184 - ((neutral::(nat => nat => nat) => nat) (HOL.plus::nat => nat => nat)) (0::nat)"
  17.185 + ((neutral::(nat => nat => nat) => nat) (plus::nat => nat => nat)) (0::nat)"
  17.186    by (import hollight NEUTRAL_ADD)
  17.187  
  17.188  lemma NEUTRAL_MUL: "neutral op * = NUMERAL_BIT1 0"
  17.189    by (import hollight NEUTRAL_MUL)
  17.190  
  17.191 -lemma MONOIDAL_ADD: "(monoidal::(nat => nat => nat) => bool) (HOL.plus::nat => nat => nat)"
  17.192 +lemma MONOIDAL_ADD: "(monoidal::(nat => nat => nat) => bool) (plus::nat => nat => nat)"
  17.193    by (import hollight MONOIDAL_ADD)
  17.194  
  17.195  lemma MONOIDAL_MUL: "(monoidal::(nat => nat => nat) => bool) (op *::nat => nat => nat)"
  17.196 @@ -8068,7 +8068,7 @@
  17.197    by (import hollight NSUM_DIFF)
  17.198  
  17.199  lemma NSUM_SUPPORT: "ALL (x::'q_51214::type => nat) xa::'q_51214::type => bool.
  17.200 -   FINITE (support HOL.plus x xa) --> nsum (support HOL.plus x xa) x = nsum xa x"
  17.201 +   FINITE (support plus x xa) --> nsum (support plus x xa) x = nsum xa x"
  17.202    by (import hollight NSUM_SUPPORT)
  17.203  
  17.204  lemma NSUM_ADD: "ALL (f::'q_51260::type => nat) (g::'q_51260::type => nat)
    18.1 --- a/src/HOL/Import/HOLLight/hollight.imp	Thu Jan 28 11:48:43 2010 +0100
    18.2 +++ b/src/HOL/Import/HOLLight/hollight.imp	Thu Jan 28 11:48:49 2010 +0100
    18.3 @@ -238,10 +238,10 @@
    18.4    "<=" > "HOLLight.hollight.<="
    18.5    "<" > "HOLLight.hollight.<"
    18.6    "/\\" > "op &"
    18.7 -  "-" > "HOL.minus_class.minus" :: "nat => nat => nat"
    18.8 +  "-" > "Algebras.minus_class.minus" :: "nat => nat => nat"
    18.9    "," > "Pair"
   18.10 -  "+" > "HOL.plus_class.plus" :: "nat => nat => nat"
   18.11 -  "*" > "HOL.times_class.times" :: "nat => nat => nat"
   18.12 +  "+" > "Algebras.plus_class.plus" :: "nat => nat => nat"
   18.13 +  "*" > "Algebras.times_class.times" :: "nat => nat => nat"
   18.14    "$" > "HOLLight.hollight.$"
   18.15    "!" > "All"
   18.16  
    19.1 --- a/src/HOL/IsaMakefile	Thu Jan 28 11:48:43 2010 +0100
    19.2 +++ b/src/HOL/IsaMakefile	Thu Jan 28 11:48:49 2010 +0100
    19.3 @@ -141,6 +141,7 @@
    19.4  	@$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base
    19.5  
    19.6  PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES)\
    19.7 +  Algebras.thy \
    19.8    Complete_Lattice.thy \
    19.9    Datatype.thy \
   19.10    Extraction.thy \
    20.1 --- a/src/HOL/Mutabelle/Mutabelle.thy	Thu Jan 28 11:48:43 2010 +0100
    20.2 +++ b/src/HOL/Mutabelle/Mutabelle.thy	Thu Jan 28 11:48:49 2010 +0100
    20.3 @@ -7,16 +7,16 @@
    20.4  val comms = [@{const_name "op ="}, @{const_name "op |"}, @{const_name "op &"}];
    20.5  
    20.6  val forbidden =
    20.7 - [(@{const_name "power"}, "'a"),
    20.8 -  ("HOL.induct_equal", "'a"),
    20.9 -  ("HOL.induct_implies", "'a"),
   20.10 -  ("HOL.induct_conj", "'a"),
   20.11 -  (@{const_name "undefined"}, "'a"),
   20.12 -  (@{const_name "default"}, "'a"),
   20.13 -  (@{const_name "dummy_pattern"}, "'a::{}"),
   20.14 -  (@{const_name "uminus"}, "'a"),
   20.15 -  (@{const_name "Nat.size"}, "'a"),
   20.16 -  (@{const_name "HOL.abs"}, "'a")];
   20.17 + [(@{const_name Power.power}, "'a"),
   20.18 +  (@{const_name HOL.induct_equal}, "'a"),
   20.19 +  (@{const_name HOL.induct_implies}, "'a"),
   20.20 +  (@{const_name HOL.induct_conj}, "'a"),
   20.21 +  (@{const_name HOL.undefined}, "'a"),
   20.22 +  (@{const_name HOL.default}, "'a"),
   20.23 +  (@{const_name dummy_pattern}, "'a::{}"),
   20.24 +  (@{const_name Algebras.uminus}, "'a"),
   20.25 +  (@{const_name Nat.size}, "'a"),
   20.26 +  (@{const_name Algebras.abs}, "'a")];
   20.27  
   20.28  val forbidden_thms =
   20.29   ["finite_intvl_succ_class",
    21.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Jan 28 11:48:43 2010 +0100
    21.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Jan 28 11:48:49 2010 +0100
    21.3 @@ -189,15 +189,15 @@
    21.4  
    21.5  val forbidden =
    21.6   [(* (@{const_name "power"}, "'a"), *)
    21.7 -  ("HOL.induct_equal", "'a"),
    21.8 -  ("HOL.induct_implies", "'a"),
    21.9 -  ("HOL.induct_conj", "'a"),
   21.10 +  (@{const_name HOL.induct_equal}, "'a"),
   21.11 +  (@{const_name HOL.induct_implies}, "'a"),
   21.12 +  (@{const_name HOL.induct_conj}, "'a"),
   21.13    (@{const_name "undefined"}, "'a"),
   21.14    (@{const_name "default"}, "'a"),
   21.15    (@{const_name "dummy_pattern"}, "'a::{}") (*,
   21.16    (@{const_name "uminus"}, "'a"),
   21.17    (@{const_name "Nat.size"}, "'a"),
   21.18 -  (@{const_name "HOL.abs"}, "'a") *)]
   21.19 +  (@{const_name "Algebras.abs"}, "'a") *)]
   21.20  
   21.21  val forbidden_thms =
   21.22   ["finite_intvl_succ_class",
    22.1 --- a/src/HOL/NSA/NSA.thy	Thu Jan 28 11:48:43 2010 +0100
    22.2 +++ b/src/HOL/NSA/NSA.thy	Thu Jan 28 11:48:49 2010 +0100
    22.3 @@ -671,12 +671,12 @@
    22.4    0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
    22.5  fun reorient_proc sg _ (_ $ t $ u) =
    22.6    case u of
    22.7 -      Const(@{const_name HOL.zero}, _) => NONE
    22.8 -    | Const(@{const_name HOL.one}, _) => NONE
    22.9 +      Const(@{const_name Algebras.zero}, _) => NONE
   22.10 +    | Const(@{const_name Algebras.one}, _) => NONE
   22.11      | Const(@{const_name Int.number_of}, _) $ _ => NONE
   22.12      | _ => SOME (case t of
   22.13 -                Const(@{const_name HOL.zero}, _) => meta_zero_approx_reorient
   22.14 -              | Const(@{const_name HOL.one}, _) => meta_one_approx_reorient
   22.15 +                Const(@{const_name Algebras.zero}, _) => meta_zero_approx_reorient
   22.16 +              | Const(@{const_name Algebras.one}, _) => meta_one_approx_reorient
   22.17                | Const(@{const_name Int.number_of}, _) $ _ =>
   22.18                                   meta_number_of_approx_reorient);
   22.19  
    23.1 --- a/src/HOL/Orderings.thy	Thu Jan 28 11:48:43 2010 +0100
    23.2 +++ b/src/HOL/Orderings.thy	Thu Jan 28 11:48:49 2010 +0100
    23.3 @@ -5,7 +5,7 @@
    23.4  header {* Abstract orderings *}
    23.5  
    23.6  theory Orderings
    23.7 -imports HOL
    23.8 +imports Algebras
    23.9  uses
   23.10    "~~/src/Provers/order.ML"
   23.11    "~~/src/Provers/quasi.ML"  (* FIXME unused? *)
    24.1 --- a/src/HOL/Prolog/Func.thy	Thu Jan 28 11:48:43 2010 +0100
    24.2 +++ b/src/HOL/Prolog/Func.thy	Thu Jan 28 11:48:49 2010 +0100
    24.3 @@ -1,12 +1,11 @@
    24.4  (*  Title:    HOL/Prolog/Func.thy
    24.5 -    ID:       $Id$
    24.6      Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
    24.7  *)
    24.8  
    24.9  header {* Untyped functional language, with call by value semantics *}
   24.10  
   24.11  theory Func
   24.12 -imports HOHH
   24.13 +imports HOHH Algebras
   24.14  begin
   24.15  
   24.16  typedecl tm
    25.1 --- a/src/HOL/Prolog/HOHH.thy	Thu Jan 28 11:48:43 2010 +0100
    25.2 +++ b/src/HOL/Prolog/HOHH.thy	Thu Jan 28 11:48:49 2010 +0100
    25.3 @@ -1,5 +1,4 @@
    25.4  (*  Title:    HOL/Prolog/HOHH.thy
    25.5 -    ID:       $Id$
    25.6      Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
    25.7  *)
    25.8  
    26.1 --- a/src/HOL/Prolog/Test.thy	Thu Jan 28 11:48:43 2010 +0100
    26.2 +++ b/src/HOL/Prolog/Test.thy	Thu Jan 28 11:48:49 2010 +0100
    26.3 @@ -1,5 +1,4 @@
    26.4  (*  Title:    HOL/Prolog/Test.thy
    26.5 -    ID:       $Id$
    26.6      Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
    26.7  *)
    26.8  
    27.1 --- a/src/HOL/Prolog/Type.thy	Thu Jan 28 11:48:43 2010 +0100
    27.2 +++ b/src/HOL/Prolog/Type.thy	Thu Jan 28 11:48:49 2010 +0100
    27.3 @@ -1,5 +1,4 @@
    27.4  (*  Title:    HOL/Prolog/Type.thy
    27.5 -    ID:       $Id$
    27.6      Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
    27.7  *)
    27.8  
    28.1 --- a/src/HOL/Set.thy	Thu Jan 28 11:48:43 2010 +0100
    28.2 +++ b/src/HOL/Set.thy	Thu Jan 28 11:48:49 2010 +0100
    28.3 @@ -928,7 +928,7 @@
    28.4    outer-level constant, which in this case is just "op :"; we instead need
    28.5    to use term-nets to associate patterns with rules.  Also, if a rule fails to
    28.6    apply, then the formula should be kept.
    28.7 -  [("HOL.uminus", Compl_iff RS iffD1), ("HOL.minus", [Diff_iff RS iffD1]),
    28.8 +  [("uminus", Compl_iff RS iffD1), ("minus", [Diff_iff RS iffD1]),
    28.9     ("Int", [IntD1,IntD2]),
   28.10     ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])]
   28.11   *)
    29.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Thu Jan 28 11:48:43 2010 +0100
    29.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Thu Jan 28 11:48:49 2010 +0100
    29.3 @@ -80,10 +80,10 @@
    29.4    let
    29.5      val goals = cterm_of thy o mk_goal (vars, prems, mfun $ lhs, mfun $ rhs)
    29.6    in
    29.7 -    case try_proof (goals @{const_name HOL.less}) solve_tac of
    29.8 +    case try_proof (goals @{const_name Algebras.less}) solve_tac of
    29.9        Solved thm => Less thm
   29.10      | Stuck thm =>
   29.11 -      (case try_proof (goals @{const_name HOL.less_eq}) solve_tac of
   29.12 +      (case try_proof (goals @{const_name Algebras.less_eq}) solve_tac of
   29.13           Solved thm2 => LessEq (thm2, thm)
   29.14         | Stuck thm2 =>
   29.15           if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const] then False thm2
    30.1 --- a/src/HOL/Tools/Function/size.ML	Thu Jan 28 11:48:43 2010 +0100
    30.2 +++ b/src/HOL/Tools/Function/size.ML	Thu Jan 28 11:48:49 2010 +0100
    30.3 @@ -25,7 +25,7 @@
    30.4  
    30.5  val lookup_size = SizeData.get #> Symtab.lookup;
    30.6  
    30.7 -fun plus (t1, t2) = Const ("HOL.plus_class.plus",
    30.8 +fun plus (t1, t2) = Const (@{const_name Algebras.plus},
    30.9    HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
   30.10  
   30.11  fun size_of_type f g h (T as Type (s, Ts)) =
    31.1 --- a/src/HOL/Tools/Function/termination.ML	Thu Jan 28 11:48:43 2010 +0100
    31.2 +++ b/src/HOL/Tools/Function/termination.ML	Thu Jan 28 11:48:49 2010 +0100
    31.3 @@ -203,10 +203,10 @@
    31.4               HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
    31.5                 $ (m2 $ r) $ (m1 $ l)))))) tac
    31.6    in
    31.7 -    case try @{const_name HOL.less} of
    31.8 +    case try @{const_name Algebras.less} of
    31.9         Solved thm => Less thm
   31.10       | Stuck thm =>
   31.11 -       (case try @{const_name HOL.less_eq} of
   31.12 +       (case try @{const_name Algebras.less_eq} of
   31.13            Solved thm2 => LessEq (thm2, thm)
   31.14          | Stuck thm2 =>
   31.15            if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const]
    32.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Jan 28 11:48:43 2010 +0100
    32.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Jan 28 11:48:49 2010 +0100
    32.3 @@ -74,7 +74,7 @@
    32.4      Const (atom_name "" T j, T)
    32.5  
    32.6  (* term -> real *)
    32.7 -fun extract_real_number (Const (@{const_name HOL.divide}, _) $ t1 $ t2) =
    32.8 +fun extract_real_number (Const (@{const_name Algebras.divide}, _) $ t1 $ t2) =
    32.9      real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
   32.10    | extract_real_number t = real (snd (HOLogic.dest_number t))
   32.11  (* term * term -> order *)
   32.12 @@ -434,7 +434,7 @@
   32.13                             0 => mk_num 0
   32.14                           | n1 => case HOLogic.dest_number t2 |> snd of
   32.15                                     1 => mk_num n1
   32.16 -                                 | n2 => Const (@{const_name HOL.divide},
   32.17 +                                 | n2 => Const (@{const_name Algebras.divide},
   32.18                                                  num_T --> num_T --> num_T)
   32.19                                           $ mk_num n1 $ mk_num n2)
   32.20                        | _ => raise TERM ("Nitpick_Model.reconstruct_term.term_\
    33.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Jan 28 11:48:43 2010 +0100
    33.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Jan 28 11:48:49 2010 +0100
    33.3 @@ -1561,7 +1561,7 @@
    33.4    end;
    33.5  
    33.6  (* special setup for simpset *)                  
    33.7 -val HOL_basic_ss' = HOL_basic_ss addsimps (@{thms "HOL.simp_thms"} @ [@{thm Pair_eq}])
    33.8 +val HOL_basic_ss' = HOL_basic_ss addsimps (@{thms HOL.simp_thms} @ [@{thm Pair_eq}])
    33.9    setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
   33.10    setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI}))
   33.11  
   33.12 @@ -1817,7 +1817,7 @@
   33.13       (* make this simpset better! *)
   33.14      asm_full_simp_tac (HOL_basic_ss' addsimps simprules) 1
   33.15      THEN print_tac' options "after prove_match:"
   33.16 -    THEN (DETERM (TRY (EqSubst.eqsubst_tac (ProofContext.init thy) [0] [@{thm "HOL.if_P"}] 1
   33.17 +    THEN (DETERM (TRY (EqSubst.eqsubst_tac (ProofContext.init thy) [0] [@{thm HOL.if_P}] 1
   33.18             THEN (REPEAT_DETERM (rtac @{thm conjI} 1 THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1))))
   33.19             THEN print_tac' options "if condition to be solved:"
   33.20             THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1 THEN print_tac' options "after if simp; in SOLVED:"))
   33.21 @@ -1843,7 +1843,7 @@
   33.22    in 
   33.23      (* remove not_False_eq_True when simpset in prove_match is better *)
   33.24      simp_tac (HOL_basic_ss addsimps
   33.25 -      (@{thms "HOL.simp_thms"} @ (@{thm not_False_eq_True} :: @{thm eval_pred} :: defs))) 1 
   33.26 +      (@{thms HOL.simp_thms} @ (@{thm not_False_eq_True} :: @{thm eval_pred} :: defs))) 1 
   33.27      (* need better control here! *)
   33.28    end
   33.29  
   33.30 @@ -2435,8 +2435,8 @@
   33.31        val [polarity, depth] = additional_arguments
   33.32        val polarity' = (case prem of Prem _ => I | Negprem _ => HOLogic.mk_not | _ => I) polarity
   33.33        val depth' =
   33.34 -        Const ("HOL.minus_class.minus", @{typ "code_numeral => code_numeral => code_numeral"})
   33.35 -          $ depth $ Const ("HOL.one_class.one", @{typ "Code_Numeral.code_numeral"})
   33.36 +        Const ("Algebras.minus", @{typ "code_numeral => code_numeral => code_numeral"})
   33.37 +          $ depth $ Const ("Algebras.one", @{typ "Code_Numeral.code_numeral"})
   33.38      in [polarity', depth'] end
   33.39    }
   33.40  
    34.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Jan 28 11:48:43 2010 +0100
    34.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Thu Jan 28 11:48:49 2010 +0100
    34.3 @@ -219,21 +219,21 @@
    34.4     @{const_name "op &"}]
    34.5  
    34.6  fun special_cases (c, T) = member (op =) [
    34.7 -  @{const_name "Product_Type.Unity"},
    34.8 -  @{const_name "False"},
    34.9 -  @{const_name "Suc"}, @{const_name Nat.zero_nat_inst.zero_nat},
   34.10 +  @{const_name Product_Type.Unity},
   34.11 +  @{const_name False},
   34.12 +  @{const_name Suc}, @{const_name Nat.zero_nat_inst.zero_nat},
   34.13    @{const_name Nat.one_nat_inst.one_nat},
   34.14 -  @{const_name "HOL.ord_class.less"}, @{const_name "HOL.ord_class.less_eq"},
   34.15 -  @{const_name "HOL.zero_class.zero"},
   34.16 -  @{const_name "HOL.one_class.one"},  @{const_name HOL.plus_class.plus},
   34.17 +  @{const_name Algebras.ord_class.less}, @{const_name Algebras.ord_class.less_eq},
   34.18 +  @{const_name Algebras.zero},
   34.19 +  @{const_name Algebras.one},  @{const_name Algebras.plus},
   34.20    @{const_name Nat.ord_nat_inst.less_eq_nat},
   34.21    @{const_name Nat.ord_nat_inst.less_nat},
   34.22    @{const_name number_nat_inst.number_of_nat},
   34.23    @{const_name Int.Bit0},
   34.24    @{const_name Int.Bit1},
   34.25    @{const_name Int.Pls},
   34.26 -  @{const_name "Int.zero_int_inst.zero_int"},
   34.27 -  @{const_name "List.filter"}] c
   34.28 +  @{const_name Int.zero_int_inst.zero_int},
   34.29 +  @{const_name List.filter}] c
   34.30  
   34.31  fun print_specification options thy constname specs = 
   34.32    if show_intermediate_results options then
    35.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Thu Jan 28 11:48:43 2010 +0100
    35.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Thu Jan 28 11:48:49 2010 +0100
    35.3 @@ -73,15 +73,15 @@
    35.4  | Const ("op =",ty)$y$_ => if term_of x aconv y then Eq (Thm.dest_arg ct) else Nox
    35.5  | Const (@{const_name Not},_) $ (Const ("op =",_)$y$_) =>
    35.6    if term_of x aconv y then NEq (funpow 2 Thm.dest_arg ct) else Nox
    35.7 -| Const (@{const_name HOL.less}, _) $ y$ z =>
    35.8 +| Const (@{const_name Algebras.less}, _) $ y$ z =>
    35.9     if term_of x aconv y then Lt (Thm.dest_arg ct)
   35.10     else if term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox
   35.11 -| Const (@{const_name HOL.less_eq}, _) $ y $ z =>
   35.12 +| Const (@{const_name Algebras.less_eq}, _) $ y $ z =>
   35.13     if term_of x aconv y then Le (Thm.dest_arg ct)
   35.14     else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
   35.15 -| Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$y$_) =>
   35.16 +| Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$y$_) =>
   35.17     if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox
   35.18 -| Const (@{const_name Not},_) $ (Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$y$_)) =>
   35.19 +| Const (@{const_name Not},_) $ (Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$y$_)) =>
   35.20     if term_of x aconv y then
   35.21     NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox
   35.22  | _ => Nox)
   35.23 @@ -175,18 +175,18 @@
   35.24    (fn _ => EVERY [simp_tac lin_ss 1, TRY (Lin_Arith.tac ctxt 1)]);
   35.25  fun linear_cmul 0 tm = zero
   35.26    | linear_cmul n tm = case tm of
   35.27 -      Const (@{const_name HOL.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b
   35.28 -    | Const (@{const_name HOL.times}, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x
   35.29 -    | Const (@{const_name HOL.minus}, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b
   35.30 -    | (m as Const (@{const_name HOL.uminus}, _)) $ a => m $ linear_cmul n a
   35.31 +      Const (@{const_name Algebras.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b
   35.32 +    | Const (@{const_name Algebras.times}, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x
   35.33 +    | Const (@{const_name Algebras.minus}, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b
   35.34 +    | (m as Const (@{const_name Algebras.uminus}, _)) $ a => m $ linear_cmul n a
   35.35      | _ => numeral1 (fn m => n * m) tm;
   35.36  fun earlier [] x y = false
   35.37    | earlier (h::t) x y =
   35.38      if h aconv y then false else if h aconv x then true else earlier t x y;
   35.39  
   35.40  fun linear_add vars tm1 tm2 = case (tm1, tm2) of
   35.41 -    (Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c1 $ x1) $ r1,
   35.42 -    Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c2 $ x2) $ r2) =>
   35.43 +    (Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c1 $ x1) $ r1,
   35.44 +    Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c2 $ x2) $ r2) =>
   35.45     if x1 = x2 then
   35.46       let val c = numeral2 Integer.add c1 c2
   35.47        in if c = zero then linear_add vars r1 r2
   35.48 @@ -194,9 +194,9 @@
   35.49       end
   35.50       else if earlier vars x1 x2 then addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2
   35.51     else addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2
   35.52 - | (Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c1 $ x1) $ r1, _) =>
   35.53 + | (Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c1 $ x1) $ r1, _) =>
   35.54        addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2
   35.55 - | (_, Const (@{const_name HOL.plus}, _) $ (Const (@{const_name HOL.times}, _) $ c2 $ x2) $ r2) =>
   35.56 + | (_, Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c2 $ x2) $ r2) =>
   35.57        addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2
   35.58   | (_, _) => numeral2 Integer.add tm1 tm2;
   35.59  
   35.60 @@ -205,10 +205,10 @@
   35.61  
   35.62  
   35.63  fun lint vars tm =  if is_numeral tm then tm  else case tm of
   35.64 -  Const (@{const_name HOL.uminus}, _) $ t => linear_neg (lint vars t)
   35.65 -| Const (@{const_name HOL.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t)
   35.66 -| Const (@{const_name HOL.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t)
   35.67 -| Const (@{const_name HOL.times}, _) $ s $ t =>
   35.68 +  Const (@{const_name Algebras.uminus}, _) $ t => linear_neg (lint vars t)
   35.69 +| Const (@{const_name Algebras.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t)
   35.70 +| Const (@{const_name Algebras.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t)
   35.71 +| Const (@{const_name Algebras.times}, _) $ s $ t =>
   35.72    let val s' = lint vars s
   35.73        val t' = lint vars t
   35.74    in if is_numeral s' then (linear_cmul (dest_numeral s') t')
   35.75 @@ -217,10 +217,10 @@
   35.76    end
   35.77   | _ => addC $ (mulC $ one $ tm) $ zero;
   35.78  
   35.79 -fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.less}, T) $ s $ t)) =
   35.80 -    lin vs (Const (@{const_name HOL.less_eq}, T) $ t $ s)
   35.81 -  | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name HOL.less_eq}, T) $ s $ t)) =
   35.82 -    lin vs (Const (@{const_name HOL.less}, T) $ t $ s)
   35.83 +fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name Algebras.less}, T) $ s $ t)) =
   35.84 +    lin vs (Const (@{const_name Algebras.less_eq}, T) $ t $ s)
   35.85 +  | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name Algebras.less_eq}, T) $ s $ t)) =
   35.86 +    lin vs (Const (@{const_name Algebras.less}, T) $ t $ s)
   35.87    | lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t)
   35.88    | lin (vs as x::_) (Const(@{const_name Ring_and_Field.dvd},_)$d$t) =
   35.89      HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} (numeral1 abs d, lint vs t)
   35.90 @@ -270,7 +270,7 @@
   35.91        val d'' = Thm.rhs_of dth |> Thm.dest_arg1
   35.92       in
   35.93        case tt' of
   35.94 -        Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$_)$_ =>
   35.95 +        Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$_)$_ =>
   35.96          let val x = dest_numeral c
   35.97          in if x < 0 then Conv.fconv_rule (arg_conv (arg_conv (lint_conv ctxt vs)))
   35.98                                         (Thm.transitive dth (inst' [d'',t'] dvd_uminus'))
   35.99 @@ -293,15 +293,15 @@
  35.100    val ins = insert (op = : int * int -> bool)
  35.101    fun h (acc,dacc) t =
  35.102     case (term_of t) of
  35.103 -    Const(s,_)$(Const(@{const_name HOL.times},_)$c$y)$ _ =>
  35.104 +    Const(s,_)$(Const(@{const_name Algebras.times},_)$c$y)$ _ =>
  35.105      if x aconv y andalso member (op =)
  35.106 -      ["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s
  35.107 +      ["op =", @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
  35.108      then (ins (dest_numeral c) acc,dacc) else (acc,dacc)
  35.109 -  | Const(s,_)$_$(Const(@{const_name HOL.times},_)$c$y) =>
  35.110 +  | Const(s,_)$_$(Const(@{const_name Algebras.times},_)$c$y) =>
  35.111      if x aconv y andalso member (op =)
  35.112 -       [@{const_name HOL.less}, @{const_name HOL.less_eq}] s
  35.113 +       [@{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
  35.114      then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
  35.115 -  | Const(@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_) =>
  35.116 +  | Const(@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_) =>
  35.117      if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)
  35.118    | Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
  35.119    | Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
  35.120 @@ -335,15 +335,15 @@
  35.121     Const("op &",_)$_$_ => binop_conv unit_conv t
  35.122    | Const("op |",_)$_$_ => binop_conv unit_conv t
  35.123    | Const (@{const_name Not},_)$_ => arg_conv unit_conv t
  35.124 -  | Const(s,_)$(Const(@{const_name HOL.times},_)$c$y)$ _ =>
  35.125 +  | Const(s,_)$(Const(@{const_name Algebras.times},_)$c$y)$ _ =>
  35.126      if x=y andalso member (op =)
  35.127 -      ["op =", @{const_name HOL.less}, @{const_name HOL.less_eq}] s
  35.128 +      ["op =", @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
  35.129      then cv (l div dest_numeral c) t else Thm.reflexive t
  35.130 -  | Const(s,_)$_$(Const(@{const_name HOL.times},_)$c$y) =>
  35.131 +  | Const(s,_)$_$(Const(@{const_name Algebras.times},_)$c$y) =>
  35.132      if x=y andalso member (op =)
  35.133 -      [@{const_name HOL.less}, @{const_name HOL.less_eq}] s
  35.134 +      [@{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
  35.135      then cv (l div dest_numeral c) t else Thm.reflexive t
  35.136 -  | Const(@{const_name Ring_and_Field.dvd},_)$d$(r as (Const(@{const_name HOL.plus},_)$(Const(@{const_name HOL.times},_)$c$y)$_)) =>
  35.137 +  | Const(@{const_name Ring_and_Field.dvd},_)$d$(r as (Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_)) =>
  35.138      if x=y then
  35.139        let
  35.140         val k = l div dest_numeral c
  35.141 @@ -546,10 +546,10 @@
  35.142    | @{term "0::int"} => C 0
  35.143    | @{term "1::int"} => C 1
  35.144    | Term.Bound i => Bound i
  35.145 -  | Const(@{const_name HOL.uminus},_)$t' => Neg (i_of_term vs t')
  35.146 -  | Const(@{const_name HOL.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
  35.147 -  | Const(@{const_name HOL.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
  35.148 -  | Const(@{const_name HOL.times},_)$t1$t2 =>
  35.149 +  | Const(@{const_name Algebras.uminus},_)$t' => Neg (i_of_term vs t')
  35.150 +  | Const(@{const_name Algebras.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
  35.151 +  | Const(@{const_name Algebras.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
  35.152 +  | Const(@{const_name Algebras.times},_)$t1$t2 =>
  35.153       (Mul (HOLogic.dest_number t1 |> snd, i_of_term vs t2)
  35.154      handle TERM _ =>
  35.155         (Mul (HOLogic.dest_number t2 |> snd, i_of_term vs t1)
  35.156 @@ -560,8 +560,8 @@
  35.157  fun qf_of_term ps vs t =  case t
  35.158   of Const("True",_) => T
  35.159    | Const("False",_) => F
  35.160 -  | Const(@{const_name HOL.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
  35.161 -  | Const(@{const_name HOL.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
  35.162 +  | Const(@{const_name Algebras.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
  35.163 +  | Const(@{const_name Algebras.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
  35.164    | Const(@{const_name Ring_and_Field.dvd},_)$t1$t2 =>
  35.165        (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")  (* FIXME avoid handle _ *)
  35.166    | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
    36.1 --- a/src/HOL/Tools/Qelim/cooper_data.ML	Thu Jan 28 11:48:43 2010 +0100
    36.2 +++ b/src/HOL/Tools/Qelim/cooper_data.ML	Thu Jan 28 11:48:49 2010 +0100
    36.3 @@ -33,7 +33,7 @@
    36.4     @{term "abs :: int => _"},
    36.5     @{term "max :: int => _"}, @{term "max :: nat => _"},
    36.6     @{term "min :: int => _"}, @{term "min :: nat => _"},
    36.7 -   @{term "HOL.uminus :: int => _"}, (*@ {term "HOL.uminus :: nat => _"},*)
    36.8 +   @{term "uminus :: int => _"}, (*@ {term "uminus :: nat => _"},*)
    36.9     @{term "Not"}, @{term "Suc"},
   36.10     @{term "Ex :: (int => _) => _"}, @{term "Ex :: (nat => _) => _"},
   36.11     @{term "All :: (int => _) => _"}, @{term "All :: (nat => _) => _"},
    37.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Thu Jan 28 11:48:43 2010 +0100
    37.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Thu Jan 28 11:48:49 2010 +0100
    37.3 @@ -52,15 +52,15 @@
    37.4  
    37.5  local
    37.6   fun isnum t = case t of 
    37.7 -   Const(@{const_name HOL.zero},_) => true
    37.8 - | Const(@{const_name HOL.one},_) => true
    37.9 +   Const(@{const_name Algebras.zero},_) => true
   37.10 + | Const(@{const_name Algebras.one},_) => true
   37.11   | @{term "Suc"}$s => isnum s
   37.12   | @{term "nat"}$s => isnum s
   37.13   | @{term "int"}$s => isnum s
   37.14 - | Const(@{const_name HOL.uminus},_)$s => isnum s
   37.15 - | Const(@{const_name HOL.plus},_)$l$r => isnum l andalso isnum r
   37.16 - | Const(@{const_name HOL.times},_)$l$r => isnum l andalso isnum r
   37.17 - | Const(@{const_name HOL.minus},_)$l$r => isnum l andalso isnum r
   37.18 + | Const(@{const_name Algebras.uminus},_)$s => isnum s
   37.19 + | Const(@{const_name Algebras.plus},_)$l$r => isnum l andalso isnum r
   37.20 + | Const(@{const_name Algebras.times},_)$l$r => isnum l andalso isnum r
   37.21 + | Const(@{const_name Algebras.minus},_)$l$r => isnum l andalso isnum r
   37.22   | Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r
   37.23   | Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r
   37.24   | Const(@{const_name Divides.div},_)$l$r => isnum l andalso isnum r
    38.1 --- a/src/HOL/Tools/arith_data.ML	Thu Jan 28 11:48:43 2010 +0100
    38.2 +++ b/src/HOL/Tools/arith_data.ML	Thu Jan 28 11:48:49 2010 +0100
    38.3 @@ -75,11 +75,11 @@
    38.4  
    38.5  fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n;
    38.6  
    38.7 -val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
    38.8 +val mk_plus = HOLogic.mk_binop @{const_name Algebras.plus};
    38.9  
   38.10  fun mk_minus t = 
   38.11    let val T = Term.fastype_of t
   38.12 -  in Const (@{const_name HOL.uminus}, T --> T) $ t end;
   38.13 +  in Const (@{const_name Algebras.uminus}, T --> T) $ t end;
   38.14  
   38.15  (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
   38.16  fun mk_sum T []        = mk_number T 0
   38.17 @@ -91,9 +91,9 @@
   38.18    | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
   38.19  
   38.20  (*decompose additions AND subtractions as a sum*)
   38.21 -fun dest_summing (pos, Const (@{const_name HOL.plus}, _) $ t $ u, ts) =
   38.22 +fun dest_summing (pos, Const (@{const_name Algebras.plus}, _) $ t $ u, ts) =
   38.23          dest_summing (pos, t, dest_summing (pos, u, ts))
   38.24 -  | dest_summing (pos, Const (@{const_name HOL.minus}, _) $ t $ u, ts) =
   38.25 +  | dest_summing (pos, Const (@{const_name Algebras.minus}, _) $ t $ u, ts) =
   38.26          dest_summing (pos, t, dest_summing (not pos, u, ts))
   38.27    | dest_summing (pos, t, ts) =
   38.28          if pos then t::ts else mk_minus t :: ts;
    39.1 --- a/src/HOL/Tools/hologic.ML	Thu Jan 28 11:48:43 2010 +0100
    39.2 +++ b/src/HOL/Tools/hologic.ML	Thu Jan 28 11:48:49 2010 +0100
    39.3 @@ -440,9 +440,9 @@
    39.4  
    39.5  val natT = Type ("nat", []);
    39.6  
    39.7 -val zero = Const ("HOL.zero_class.zero", natT);
    39.8 +val zero = Const ("Algebras.zero_class.zero", natT);
    39.9  
   39.10 -fun is_zero (Const ("HOL.zero_class.zero", _)) = true
   39.11 +fun is_zero (Const ("Algebras.zero_class.zero", _)) = true
   39.12    | is_zero _ = false;
   39.13  
   39.14  fun mk_Suc t = Const ("Suc", natT --> natT) $ t;
   39.15 @@ -458,7 +458,7 @@
   39.16        | mk n = mk_Suc (mk (n - 1));
   39.17    in if n < 0 then raise TERM ("mk_nat: negative number", []) else mk n end;
   39.18  
   39.19 -fun dest_nat (Const ("HOL.zero_class.zero", _)) = 0
   39.20 +fun dest_nat (Const ("Algebras.zero_class.zero", _)) = 0
   39.21    | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
   39.22    | dest_nat t = raise TERM ("dest_nat", [t]);
   39.23  
   39.24 @@ -508,12 +508,12 @@
   39.25    | add_numerals (Abs (_, _, t)) = add_numerals t
   39.26    | add_numerals _ = I;
   39.27  
   39.28 -fun mk_number T 0 = Const ("HOL.zero_class.zero", T)
   39.29 -  | mk_number T 1 = Const ("HOL.one_class.one", T)
   39.30 +fun mk_number T 0 = Const ("Algebras.zero_class.zero", T)
   39.31 +  | mk_number T 1 = Const ("Algebras.one_class.one", T)
   39.32    | mk_number T i = number_of_const T $ mk_numeral i;
   39.33  
   39.34 -fun dest_number (Const ("HOL.zero_class.zero", T)) = (T, 0)
   39.35 -  | dest_number (Const ("HOL.one_class.one", T)) = (T, 1)
   39.36 +fun dest_number (Const ("Algebras.zero_class.zero", T)) = (T, 0)
   39.37 +  | dest_number (Const ("Algebras.one_class.one", T)) = (T, 1)
   39.38    | dest_number (Const ("Int.number_class.number_of", Type ("fun", [_, T])) $ t) =
   39.39        (T, dest_numeral t)
   39.40    | dest_number t = raise TERM ("dest_number", [t]);
    40.1 --- a/src/HOL/Tools/inductive.ML	Thu Jan 28 11:48:43 2010 +0100
    40.2 +++ b/src/HOL/Tools/inductive.ML	Thu Jan 28 11:48:49 2010 +0100
    40.3 @@ -184,7 +184,7 @@
    40.4      case concl_of thm of
    40.5        Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
    40.6      | _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
    40.7 -    | _ $ (Const (@{const_name HOL.less_eq}, _) $ _ $ _) =>
    40.8 +    | _ $ (Const (@{const_name Algebras.less_eq}, _) $ _ $ _) =>
    40.9        dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
   40.10          (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
   40.11      | _ => thm
   40.12 @@ -561,7 +561,7 @@
   40.13           (list_comb (P, make_args' argTs xs (binder_types (fastype_of P))))) preds));
   40.14  
   40.15      val ind_concl = HOLogic.mk_Trueprop
   40.16 -      (HOLogic.mk_binrel "HOL.ord_class.less_eq" (rec_const, ind_pred));
   40.17 +      (HOLogic.mk_binrel @{const_name Algebras.less_eq} (rec_const, ind_pred));
   40.18  
   40.19      val raw_fp_induct = (mono RS (fp_def RS @{thm def_lfp_induct}));
   40.20  
    41.1 --- a/src/HOL/Tools/int_arith.ML	Thu Jan 28 11:48:43 2010 +0100
    41.2 +++ b/src/HOL/Tools/int_arith.ML	Thu Jan 28 11:48:49 2010 +0100
    41.3 @@ -49,13 +49,13 @@
    41.4    make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
    41.5    proc = proc1, identifier = []};
    41.6  
    41.7 -fun check (Const (@{const_name HOL.one}, @{typ int})) = false
    41.8 -  | check (Const (@{const_name HOL.one}, _)) = true
    41.9 +fun check (Const (@{const_name Algebras.one}, @{typ int})) = false
   41.10 +  | check (Const (@{const_name Algebras.one}, _)) = true
   41.11    | check (Const (s, _)) = member (op =) [@{const_name "op ="},
   41.12 -      @{const_name HOL.times}, @{const_name HOL.uminus},
   41.13 -      @{const_name HOL.minus}, @{const_name HOL.plus},
   41.14 -      @{const_name HOL.zero},
   41.15 -      @{const_name HOL.less}, @{const_name HOL.less_eq}] s
   41.16 +      @{const_name Algebras.times}, @{const_name Algebras.uminus},
   41.17 +      @{const_name Algebras.minus}, @{const_name Algebras.plus},
   41.18 +      @{const_name Algebras.zero},
   41.19 +      @{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
   41.20    | check (a $ b) = check a andalso check b
   41.21    | check _ = false;
   41.22  
    42.1 --- a/src/HOL/Tools/lin_arith.ML	Thu Jan 28 11:48:43 2010 +0100
    42.2 +++ b/src/HOL/Tools/lin_arith.ML	Thu Jan 28 11:48:49 2010 +0100
    42.3 @@ -138,8 +138,8 @@
    42.4  *)
    42.5  fun demult (inj_consts : (string * typ) list) : term * Rat.rat -> term option * Rat.rat =
    42.6  let
    42.7 -  fun demult ((mC as Const (@{const_name HOL.times}, _)) $ s $ t, m) =
    42.8 -      (case s of Const (@{const_name HOL.times}, _) $ s1 $ s2 =>
    42.9 +  fun demult ((mC as Const (@{const_name Algebras.times}, _)) $ s $ t, m) =
   42.10 +      (case s of Const (@{const_name Algebras.times}, _) $ s1 $ s2 =>
   42.11          (* bracketing to the right: '(s1 * s2) * t' becomes 's1 * (s2 * t)' *)
   42.12          demult (mC $ s1 $ (mC $ s2 $ t), m)
   42.13        | _ =>
   42.14 @@ -150,7 +150,7 @@
   42.15                (SOME t', m'') => (SOME (mC $ s' $ t'), m'')
   42.16              | (NONE,    m'') => (SOME s', m''))
   42.17          | (NONE,    m') => demult (t, m')))
   42.18 -    | demult ((mC as Const (@{const_name HOL.divide}, _)) $ s $ t, m) =
   42.19 +    | demult ((mC as Const (@{const_name Algebras.divide}, _)) $ s $ t, m) =
   42.20        (* FIXME: Shouldn't we simplify nested quotients, e.g. '(s/t)/u' could
   42.21           become 's/(t*u)', and '(s*t)/u' could become 's*(t/u)' ?   Note that
   42.22           if we choose to do so here, the simpset used by arith must be able to
   42.23 @@ -170,9 +170,9 @@
   42.24          (SOME _, _) => (SOME (mC $ s $ t), m)
   42.25        | (NONE,  m') => apsnd (Rat.mult (Rat.inv m')) (demult (s, m)))
   42.26      (* terms that evaluate to numeric constants *)
   42.27 -    | demult (Const (@{const_name HOL.uminus}, _) $ t, m) = demult (t, Rat.neg m)
   42.28 -    | demult (Const (@{const_name HOL.zero}, _), m) = (NONE, Rat.zero)
   42.29 -    | demult (Const (@{const_name HOL.one}, _), m) = (NONE, m)
   42.30 +    | demult (Const (@{const_name Algebras.uminus}, _) $ t, m) = demult (t, Rat.neg m)
   42.31 +    | demult (Const (@{const_name Algebras.zero}, _), m) = (NONE, Rat.zero)
   42.32 +    | demult (Const (@{const_name Algebras.one}, _), m) = (NONE, m)
   42.33      (*Warning: in rare cases number_of encloses a non-numeral,
   42.34        in which case dest_numeral raises TERM; hence all the handles below.
   42.35        Same for Suc-terms that turn out not to be numerals -
   42.36 @@ -196,23 +196,23 @@
   42.37    (* Turns a term 'all' and associated multiplicity 'm' into a list 'p' of
   42.38       summands and associated multiplicities, plus a constant 'i' (with implicit
   42.39       multiplicity 1) *)
   42.40 -  fun poly (Const (@{const_name HOL.plus}, _) $ s $ t,
   42.41 +  fun poly (Const (@{const_name Algebras.plus}, _) $ s $ t,
   42.42          m : Rat.rat, pi : (term * Rat.rat) list * Rat.rat) = poly (s, m, poly (t, m, pi))
   42.43 -    | poly (all as Const (@{const_name HOL.minus}, T) $ s $ t, m, pi) =
   42.44 +    | poly (all as Const (@{const_name Algebras.minus}, T) $ s $ t, m, pi) =
   42.45          if nT T then add_atom all m pi else poly (s, m, poly (t, Rat.neg m, pi))
   42.46 -    | poly (all as Const (@{const_name HOL.uminus}, T) $ t, m, pi) =
   42.47 +    | poly (all as Const (@{const_name Algebras.uminus}, T) $ t, m, pi) =
   42.48          if nT T then add_atom all m pi else poly (t, Rat.neg m, pi)
   42.49 -    | poly (Const (@{const_name HOL.zero}, _), _, pi) =
   42.50 +    | poly (Const (@{const_name Algebras.zero}, _), _, pi) =
   42.51          pi
   42.52 -    | poly (Const (@{const_name HOL.one}, _), m, (p, i)) =
   42.53 +    | poly (Const (@{const_name Algebras.one}, _), m, (p, i)) =
   42.54          (p, Rat.add i m)
   42.55      | poly (Const (@{const_name Suc}, _) $ t, m, (p, i)) =
   42.56          poly (t, m, (p, Rat.add i m))
   42.57 -    | poly (all as Const (@{const_name HOL.times}, _) $ _ $ _, m, pi as (p, i)) =
   42.58 +    | poly (all as Const (@{const_name Algebras.times}, _) $ _ $ _, m, pi as (p, i)) =
   42.59          (case demult inj_consts (all, m) of
   42.60             (NONE,   m') => (p, Rat.add i m')
   42.61           | (SOME u, m') => add_atom u m' pi)
   42.62 -    | poly (all as Const (@{const_name HOL.divide}, _) $ _ $ _, m, pi as (p, i)) =
   42.63 +    | poly (all as Const (@{const_name Algebras.divide}, _) $ _ $ _, m, pi as (p, i)) =
   42.64          (case demult inj_consts (all, m) of
   42.65             (NONE,   m') => (p, Rat.add i m')
   42.66           | (SOME u, m') => add_atom u m' pi)
   42.67 @@ -229,8 +229,8 @@
   42.68    val (q, j) = poly (rhs, Rat.one, ([], Rat.zero))
   42.69  in
   42.70    case rel of
   42.71 -    @{const_name HOL.less}    => SOME (p, i, "<", q, j)
   42.72 -  | @{const_name HOL.less_eq} => SOME (p, i, "<=", q, j)
   42.73 +    @{const_name Algebras.less}    => SOME (p, i, "<", q, j)
   42.74 +  | @{const_name Algebras.less_eq} => SOME (p, i, "<=", q, j)
   42.75    | "op ="              => SOME (p, i, "=", q, j)
   42.76    | _                   => NONE
   42.77  end handle Rat.DIVZERO => NONE;
   42.78 @@ -292,11 +292,11 @@
   42.79      case head_of lhs of
   42.80        Const (a, _) => member (op =) [@{const_name Orderings.max},
   42.81                                      @{const_name Orderings.min},
   42.82 -                                    @{const_name HOL.abs},
   42.83 -                                    @{const_name HOL.minus},
   42.84 -                                    "Int.nat",
   42.85 -                                    "Divides.div_class.mod",
   42.86 -                                    "Divides.div_class.div"] a
   42.87 +                                    @{const_name Algebras.abs},
   42.88 +                                    @{const_name Algebras.minus},
   42.89 +                                    "Int.nat" (*DYNAMIC BINDING!*),
   42.90 +                                    "Divides.div_class.mod" (*DYNAMIC BINDING!*),
   42.91 +                                    "Divides.div_class.div" (*DYNAMIC BINDING!*)] a
   42.92      | _            => (warning ("Lin. Arith.: wrong format for split rule " ^
   42.93                                   Display.string_of_thm_without_context thm);
   42.94                         false))
   42.95 @@ -372,7 +372,7 @@
   42.96          val rev_terms     = rev terms
   42.97          val terms1        = map (subst_term [(split_term, t1)]) rev_terms
   42.98          val terms2        = map (subst_term [(split_term, t2)]) rev_terms
   42.99 -        val t1_leq_t2     = Const (@{const_name HOL.less_eq},
  42.100 +        val t1_leq_t2     = Const (@{const_name Algebras.less_eq},
  42.101                                      split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
  42.102          val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
  42.103          val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
  42.104 @@ -387,7 +387,7 @@
  42.105          val rev_terms     = rev terms
  42.106          val terms1        = map (subst_term [(split_term, t1)]) rev_terms
  42.107          val terms2        = map (subst_term [(split_term, t2)]) rev_terms
  42.108 -        val t1_leq_t2     = Const (@{const_name HOL.less_eq},
  42.109 +        val t1_leq_t2     = Const (@{const_name Algebras.less_eq},
  42.110                                      split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
  42.111          val not_t1_leq_t2 = HOLogic.Not $ t1_leq_t2
  42.112          val not_false     = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
  42.113 @@ -397,16 +397,16 @@
  42.114          SOME [(Ts, subgoal1), (Ts, subgoal2)]
  42.115        end
  42.116      (* ?P (abs ?a) = ((0 <= ?a --> ?P ?a) & (?a < 0 --> ?P (- ?a))) *)
  42.117 -    | (Const (@{const_name HOL.abs}, _), [t1]) =>
  42.118 +    | (Const (@{const_name Algebras.abs}, _), [t1]) =>
  42.119        let
  42.120          val rev_terms   = rev terms
  42.121          val terms1      = map (subst_term [(split_term, t1)]) rev_terms
  42.122 -        val terms2      = map (subst_term [(split_term, Const (@{const_name HOL.uminus},
  42.123 +        val terms2      = map (subst_term [(split_term, Const (@{const_name Algebras.uminus},
  42.124                              split_type --> split_type) $ t1)]) rev_terms
  42.125 -        val zero        = Const (@{const_name HOL.zero}, split_type)
  42.126 -        val zero_leq_t1 = Const (@{const_name HOL.less_eq},
  42.127 +        val zero        = Const (@{const_name Algebras.zero}, split_type)
  42.128 +        val zero_leq_t1 = Const (@{const_name Algebras.less_eq},
  42.129                              split_type --> split_type --> HOLogic.boolT) $ zero $ t1
  42.130 -        val t1_lt_zero  = Const (@{const_name HOL.less},
  42.131 +        val t1_lt_zero  = Const (@{const_name Algebras.less},
  42.132                              split_type --> split_type --> HOLogic.boolT) $ t1 $ zero
  42.133          val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
  42.134          val subgoal1    = (HOLogic.mk_Trueprop zero_leq_t1) :: terms1 @ [not_false]
  42.135 @@ -415,22 +415,22 @@
  42.136          SOME [(Ts, subgoal1), (Ts, subgoal2)]
  42.137        end
  42.138      (* ?P (?a - ?b) = ((?a < ?b --> ?P 0) & (ALL d. ?a = ?b + d --> ?P d)) *)
  42.139 -    | (Const (@{const_name HOL.minus}, _), [t1, t2]) =>
  42.140 +    | (Const (@{const_name Algebras.minus}, _), [t1, t2]) =>
  42.141        let
  42.142          (* "d" in the above theorem becomes a new bound variable after NNF   *)
  42.143          (* transformation, therefore some adjustment of indices is necessary *)
  42.144          val rev_terms       = rev terms
  42.145 -        val zero            = Const (@{const_name HOL.zero}, split_type)
  42.146 +        val zero            = Const (@{const_name Algebras.zero}, split_type)
  42.147          val d               = Bound 0
  42.148          val terms1          = map (subst_term [(split_term, zero)]) rev_terms
  42.149          val terms2          = map (subst_term [(incr_boundvars 1 split_term, d)])
  42.150                                  (map (incr_boundvars 1) rev_terms)
  42.151          val t1'             = incr_boundvars 1 t1
  42.152          val t2'             = incr_boundvars 1 t2
  42.153 -        val t1_lt_t2        = Const (@{const_name HOL.less},
  42.154 +        val t1_lt_t2        = Const (@{const_name Algebras.less},
  42.155                                  split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
  42.156          val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
  42.157 -                                (Const (@{const_name HOL.plus},
  42.158 +                                (Const (@{const_name Algebras.plus},
  42.159                                    split_type --> split_type --> split_type) $ t2' $ d)
  42.160          val not_false       = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
  42.161          val subgoal1        = (HOLogic.mk_Trueprop t1_lt_t2) :: terms1 @ [not_false]
  42.162 @@ -442,8 +442,8 @@
  42.163      | (Const ("Int.nat", _), [t1]) =>
  42.164        let
  42.165          val rev_terms   = rev terms
  42.166 -        val zero_int    = Const (@{const_name HOL.zero}, HOLogic.intT)
  42.167 -        val zero_nat    = Const (@{const_name HOL.zero}, HOLogic.natT)
  42.168 +        val zero_int    = Const (@{const_name Algebras.zero}, HOLogic.intT)
  42.169 +        val zero_nat    = Const (@{const_name Algebras.zero}, HOLogic.natT)
  42.170          val n           = Bound 0
  42.171          val terms1      = map (subst_term [(incr_boundvars 1 split_term, n)])
  42.172                              (map (incr_boundvars 1) rev_terms)
  42.173 @@ -451,7 +451,7 @@
  42.174          val t1'         = incr_boundvars 1 t1
  42.175          val t1_eq_nat_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
  42.176                              (Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n)
  42.177 -        val t1_lt_zero  = Const (@{const_name HOL.less},
  42.178 +        val t1_lt_zero  = Const (@{const_name Algebras.less},
  42.179                              HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
  42.180          val not_false   = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
  42.181          val subgoal1    = (HOLogic.mk_Trueprop t1_eq_nat_n) :: terms1 @ [not_false]
  42.182 @@ -465,7 +465,7 @@
  42.183      | (Const ("Divides.div_class.mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
  42.184        let
  42.185          val rev_terms               = rev terms
  42.186 -        val zero                    = Const (@{const_name HOL.zero}, split_type)
  42.187 +        val zero                    = Const (@{const_name Algebras.zero}, split_type)
  42.188          val i                       = Bound 1
  42.189          val j                       = Bound 0
  42.190          val terms1                  = map (subst_term [(split_term, t1)]) rev_terms
  42.191 @@ -477,11 +477,11 @@
  42.192                                          split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
  42.193          val t2_neq_zero             = HOLogic.mk_not (Const ("op =",
  42.194                                          split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
  42.195 -        val j_lt_t2                 = Const (@{const_name HOL.less},
  42.196 +        val j_lt_t2                 = Const (@{const_name Algebras.less},
  42.197                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
  42.198          val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
  42.199 -                                       (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
  42.200 -                                         (Const (@{const_name HOL.times},
  42.201 +                                       (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
  42.202 +                                         (Const (@{const_name Algebras.times},
  42.203                                             split_type --> split_type --> split_type) $ t2' $ i) $ j)
  42.204          val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
  42.205          val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
  42.206 @@ -497,7 +497,7 @@
  42.207      | (Const ("Divides.div_class.div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
  42.208        let
  42.209          val rev_terms               = rev terms
  42.210 -        val zero                    = Const (@{const_name HOL.zero}, split_type)
  42.211 +        val zero                    = Const (@{const_name Algebras.zero}, split_type)
  42.212          val i                       = Bound 1
  42.213          val j                       = Bound 0
  42.214          val terms1                  = map (subst_term [(split_term, zero)]) rev_terms
  42.215 @@ -509,11 +509,11 @@
  42.216                                          split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
  42.217          val t2_neq_zero             = HOLogic.mk_not (Const ("op =",
  42.218                                          split_type --> split_type --> HOLogic.boolT) $ t2' $ zero)
  42.219 -        val j_lt_t2                 = Const (@{const_name HOL.less},
  42.220 +        val j_lt_t2                 = Const (@{const_name Algebras.less},
  42.221                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
  42.222          val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
  42.223 -                                       (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
  42.224 -                                         (Const (@{const_name HOL.times},
  42.225 +                                       (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
  42.226 +                                         (Const (@{const_name Algebras.times},
  42.227                                             split_type --> split_type --> split_type) $ t2' $ i) $ j)
  42.228          val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
  42.229          val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
  42.230 @@ -535,7 +535,7 @@
  42.231          Type ("fun", [Type ("Int.int", []), _])), [t1, t2]) =>
  42.232        let
  42.233          val rev_terms               = rev terms
  42.234 -        val zero                    = Const (@{const_name HOL.zero}, split_type)
  42.235 +        val zero                    = Const (@{const_name Algebras.zero}, split_type)
  42.236          val i                       = Bound 1
  42.237          val j                       = Bound 0
  42.238          val terms1                  = map (subst_term [(split_term, t1)]) rev_terms
  42.239 @@ -545,21 +545,21 @@
  42.240          val t2'                     = incr_boundvars 2 t2
  42.241          val t2_eq_zero              = Const ("op =",
  42.242                                          split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
  42.243 -        val zero_lt_t2              = Const (@{const_name HOL.less},
  42.244 +        val zero_lt_t2              = Const (@{const_name Algebras.less},
  42.245                                          split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
  42.246 -        val t2_lt_zero              = Const (@{const_name HOL.less},
  42.247 +        val t2_lt_zero              = Const (@{const_name Algebras.less},
  42.248                                          split_type --> split_type --> HOLogic.boolT) $ t2' $ zero
  42.249 -        val zero_leq_j              = Const (@{const_name HOL.less_eq},
  42.250 +        val zero_leq_j              = Const (@{const_name Algebras.less_eq},
  42.251                                          split_type --> split_type --> HOLogic.boolT) $ zero $ j
  42.252 -        val j_leq_zero              = Const (@{const_name HOL.less_eq},
  42.253 +        val j_leq_zero              = Const (@{const_name Algebras.less_eq},
  42.254                                          split_type --> split_type --> HOLogic.boolT) $ j $ zero
  42.255 -        val j_lt_t2                 = Const (@{const_name HOL.less},
  42.256 +        val j_lt_t2                 = Const (@{const_name Algebras.less},
  42.257                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
  42.258 -        val t2_lt_j                 = Const (@{const_name HOL.less},
  42.259 +        val t2_lt_j                 = Const (@{const_name Algebras.less},
  42.260                                          split_type --> split_type--> HOLogic.boolT) $ t2' $ j
  42.261          val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
  42.262 -                                       (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
  42.263 -                                         (Const (@{const_name HOL.times},
  42.264 +                                       (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
  42.265 +                                         (Const (@{const_name Algebras.times},
  42.266                                             split_type --> split_type --> split_type) $ t2' $ i) $ j)
  42.267          val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
  42.268          val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
  42.269 @@ -589,7 +589,7 @@
  42.270          Type ("fun", [Type ("Int.int", []), _])), [t1, t2]) =>
  42.271        let
  42.272          val rev_terms               = rev terms
  42.273 -        val zero                    = Const (@{const_name HOL.zero}, split_type)
  42.274 +        val zero                    = Const (@{const_name Algebras.zero}, split_type)
  42.275          val i                       = Bound 1
  42.276          val j                       = Bound 0
  42.277          val terms1                  = map (subst_term [(split_term, zero)]) rev_terms
  42.278 @@ -599,21 +599,21 @@
  42.279          val t2'                     = incr_boundvars 2 t2
  42.280          val t2_eq_zero              = Const ("op =",
  42.281                                          split_type --> split_type --> HOLogic.boolT) $ t2 $ zero
  42.282 -        val zero_lt_t2              = Const (@{const_name HOL.less},
  42.283 +        val zero_lt_t2              = Const (@{const_name Algebras.less},
  42.284                                          split_type --> split_type --> HOLogic.boolT) $ zero $ t2'
  42.285 -        val t2_lt_zero              = Const (@{const_name HOL.less},
  42.286 +        val t2_lt_zero              = Const (@{const_name Algebras.less},
  42.287                                          split_type --> split_type --> HOLogic.boolT) $ t2' $ zero
  42.288 -        val zero_leq_j              = Const (@{const_name HOL.less_eq},
  42.289 +        val zero_leq_j              = Const (@{const_name Algebras.less_eq},
  42.290                                          split_type --> split_type --> HOLogic.boolT) $ zero $ j
  42.291 -        val j_leq_zero              = Const (@{const_name HOL.less_eq},
  42.292 +        val j_leq_zero              = Const (@{const_name Algebras.less_eq},
  42.293                                          split_type --> split_type --> HOLogic.boolT) $ j $ zero
  42.294 -        val j_lt_t2                 = Const (@{const_name HOL.less},
  42.295 +        val j_lt_t2                 = Const (@{const_name Algebras.less},
  42.296                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
  42.297 -        val t2_lt_j                 = Const (@{const_name HOL.less},
  42.298 +        val t2_lt_j                 = Const (@{const_name Algebras.less},
  42.299                                          split_type --> split_type--> HOLogic.boolT) $ t2' $ j
  42.300          val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
  42.301 -                                       (Const (@{const_name HOL.plus}, split_type --> split_type --> split_type) $
  42.302 -                                         (Const (@{const_name HOL.times},
  42.303 +                                       (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
  42.304 +                                         (Const (@{const_name Algebras.times},
  42.305                                             split_type --> split_type --> split_type) $ t2' $ i) $ j)
  42.306          val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
  42.307          val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
    43.1 --- a/src/HOL/Tools/meson.ML	Thu Jan 28 11:48:43 2010 +0100
    43.2 +++ b/src/HOL/Tools/meson.ML	Thu Jan 28 11:48:49 2010 +0100
    43.3 @@ -403,7 +403,7 @@
    43.4        (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
    43.5  
    43.6  (*A higher-order instance of a first-order constant? Example is the definition of
    43.7 -  HOL.one, 1, at a function type in theory SetsAndFunctions.*)
    43.8 +  one, 1, at a function type in theory SetsAndFunctions.*)
    43.9  fun higher_inst_const thy (c,T) =
   43.10    case binder_types T of
   43.11        [] => false (*not a function type, OK*)
    44.1 --- a/src/HOL/Tools/nat_arith.ML	Thu Jan 28 11:48:43 2010 +0100
    44.2 +++ b/src/HOL/Tools/nat_arith.ML	Thu Jan 28 11:48:49 2010 +0100
    44.3 @@ -19,8 +19,8 @@
    44.4  
    44.5  (** abstract syntax of structure nat: 0, Suc, + **)
    44.6  
    44.7 -val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
    44.8 -val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
    44.9 +val mk_plus = HOLogic.mk_binop @{const_name Algebras.plus};
   44.10 +val dest_plus = HOLogic.dest_bin @{const_name Algebras.plus} HOLogic.natT;
   44.11  
   44.12  fun mk_sum [] = HOLogic.zero
   44.13    | mk_sum [t] = t
   44.14 @@ -69,24 +69,24 @@
   44.15  structure LessCancelSums = CancelSumsFun
   44.16  (struct
   44.17    open CommonCancelSums;
   44.18 -  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less};
   44.19 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT;
   44.20 +  val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less};
   44.21 +  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT;
   44.22    val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
   44.23  end);
   44.24  
   44.25  structure LeCancelSums = CancelSumsFun
   44.26  (struct
   44.27    open CommonCancelSums;
   44.28 -  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq};
   44.29 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT;
   44.30 +  val mk_bal = HOLogic.mk_binrel @{const_name Algebras.less_eq};
   44.31 +  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT;
   44.32    val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
   44.33  end);
   44.34  
   44.35  structure DiffCancelSums = CancelSumsFun
   44.36  (struct
   44.37    open CommonCancelSums;
   44.38 -  val mk_bal = HOLogic.mk_binop @{const_name HOL.minus};
   44.39 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT;
   44.40 +  val mk_bal = HOLogic.mk_binop @{const_name Algebras.minus};
   44.41 +  val dest_bal = HOLogic.dest_bin @{const_name Algebras.minus} HOLogic.natT;
   44.42    val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
   44.43  end);
   44.44  
    45.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Thu Jan 28 11:48:43 2010 +0100
    45.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Thu Jan 28 11:48:49 2010 +0100
    45.3 @@ -32,7 +32,7 @@
    45.4    | find_first_numeral past [] = raise TERM("find_first_numeral", []);
    45.5  
    45.6  val zero = mk_number 0;
    45.7 -val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
    45.8 +val mk_plus = HOLogic.mk_binop @{const_name Algebras.plus};
    45.9  
   45.10  (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
   45.11  fun mk_sum []        = zero
   45.12 @@ -43,7 +43,7 @@
   45.13  fun long_mk_sum []        = HOLogic.zero
   45.14    | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   45.15  
   45.16 -val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
   45.17 +val dest_plus = HOLogic.dest_bin @{const_name Algebras.plus} HOLogic.natT;
   45.18  
   45.19  
   45.20  (** Other simproc items **)
   45.21 @@ -61,14 +61,14 @@
   45.22  (*** CancelNumerals simprocs ***)
   45.23  
   45.24  val one = mk_number 1;
   45.25 -val mk_times = HOLogic.mk_binop @{const_name HOL.times};
   45.26 +val mk_times = HOLogic.mk_binop @{const_name Algebras.times};
   45.27  
   45.28  fun mk_prod [] = one
   45.29    | mk_prod [t] = t
   45.30    | mk_prod (t :: ts) = if t = one then mk_prod ts
   45.31                          else mk_times (t, mk_prod ts);
   45.32  
   45.33 -val dest_times = HOLogic.dest_bin @{const_name HOL.times} HOLogic.natT;
   45.34 +val dest_times = HOLogic.dest_bin @{const_name Algebras.times} HOLogic.natT;
   45.35  
   45.36  fun dest_prod t =
   45.37        let val (t,u) = dest_times t
   45.38 @@ -176,8 +176,8 @@
   45.39  structure LessCancelNumerals = CancelNumeralsFun
   45.40   (open CancelNumeralsCommon
   45.41    val prove_conv = Arith_Data.prove_conv
   45.42 -  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   45.43 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
   45.44 +  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
   45.45 +  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT
   45.46    val bal_add1 = @{thm nat_less_add_iff1} RS trans
   45.47    val bal_add2 = @{thm nat_less_add_iff2} RS trans
   45.48  );
   45.49 @@ -185,8 +185,8 @@
   45.50  structure LeCancelNumerals = CancelNumeralsFun
   45.51   (open CancelNumeralsCommon
   45.52    val prove_conv = Arith_Data.prove_conv
   45.53 -  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   45.54 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
   45.55 +  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
   45.56 +  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT
   45.57    val bal_add1 = @{thm nat_le_add_iff1} RS trans
   45.58    val bal_add2 = @{thm nat_le_add_iff2} RS trans
   45.59  );
   45.60 @@ -194,8 +194,8 @@
   45.61  structure DiffCancelNumerals = CancelNumeralsFun
   45.62   (open CancelNumeralsCommon
   45.63    val prove_conv = Arith_Data.prove_conv
   45.64 -  val mk_bal   = HOLogic.mk_binop @{const_name HOL.minus}
   45.65 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT
   45.66 +  val mk_bal   = HOLogic.mk_binop @{const_name Algebras.minus}
   45.67 +  val dest_bal = HOLogic.dest_bin @{const_name Algebras.minus} HOLogic.natT
   45.68    val bal_add1 = @{thm nat_diff_add_eq1} RS trans
   45.69    val bal_add2 = @{thm nat_diff_add_eq2} RS trans
   45.70  );
   45.71 @@ -308,8 +308,8 @@
   45.72  structure LessCancelNumeralFactor = CancelNumeralFactorFun
   45.73   (open CancelNumeralFactorCommon
   45.74    val prove_conv = Arith_Data.prove_conv
   45.75 -  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   45.76 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
   45.77 +  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
   45.78 +  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT
   45.79    val cancel = @{thm nat_mult_less_cancel1} RS trans
   45.80    val neg_exchanges = true
   45.81  )
   45.82 @@ -317,8 +317,8 @@
   45.83  structure LeCancelNumeralFactor = CancelNumeralFactorFun
   45.84   (open CancelNumeralFactorCommon
   45.85    val prove_conv = Arith_Data.prove_conv
   45.86 -  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   45.87 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
   45.88 +  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
   45.89 +  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT
   45.90    val cancel = @{thm nat_mult_le_cancel1} RS trans
   45.91    val neg_exchanges = true
   45.92  )
   45.93 @@ -387,16 +387,16 @@
   45.94  structure LessCancelFactor = ExtractCommonTermFun
   45.95   (open CancelFactorCommon
   45.96    val prove_conv = Arith_Data.prove_conv
   45.97 -  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   45.98 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
   45.99 +  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
  45.100 +  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} HOLogic.natT
  45.101    fun simp_conv _ _ = SOME @{thm nat_mult_less_cancel_disj}
  45.102  );
  45.103  
  45.104  structure LeCancelFactor = ExtractCommonTermFun
  45.105   (open CancelFactorCommon
  45.106    val prove_conv = Arith_Data.prove_conv
  45.107 -  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
  45.108 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
  45.109 +  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
  45.110 +  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} HOLogic.natT
  45.111    fun simp_conv _ _ = SOME @{thm nat_mult_le_cancel_disj}
  45.112  );
  45.113  
    46.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Thu Jan 28 11:48:43 2010 +0100
    46.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Thu Jan 28 11:48:49 2010 +0100
    46.3 @@ -34,12 +34,12 @@
    46.4  val long_mk_sum = Arith_Data.long_mk_sum;
    46.5  val dest_sum = Arith_Data.dest_sum;
    46.6  
    46.7 -val mk_diff = HOLogic.mk_binop @{const_name HOL.minus};
    46.8 -val dest_diff = HOLogic.dest_bin @{const_name HOL.minus} Term.dummyT;
    46.9 +val mk_diff = HOLogic.mk_binop @{const_name Algebras.minus};
   46.10 +val dest_diff = HOLogic.dest_bin @{const_name Algebras.minus} Term.dummyT;
   46.11  
   46.12 -val mk_times = HOLogic.mk_binop @{const_name HOL.times};
   46.13 +val mk_times = HOLogic.mk_binop @{const_name Algebras.times};
   46.14  
   46.15 -fun one_of T = Const(@{const_name HOL.one},T);
   46.16 +fun one_of T = Const(@{const_name Algebras.one}, T);
   46.17  
   46.18  (* build product with trailing 1 rather than Numeral 1 in order to avoid the
   46.19     unnecessary restriction to type class number_ring
   46.20 @@ -56,7 +56,7 @@
   46.21  fun long_mk_prod T []        = one_of T
   46.22    | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts);
   46.23  
   46.24 -val dest_times = HOLogic.dest_bin @{const_name HOL.times} Term.dummyT;
   46.25 +val dest_times = HOLogic.dest_bin @{const_name Algebras.times} Term.dummyT;
   46.26  
   46.27  fun dest_prod t =
   46.28        let val (t,u) = dest_times t
   46.29 @@ -72,7 +72,7 @@
   46.30  fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t);
   46.31  
   46.32  (*Express t as a product of (possibly) a numeral with other sorted terms*)
   46.33 -fun dest_coeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_coeff (~sign) t
   46.34 +fun dest_coeff sign (Const (@{const_name Algebras.uminus}, _) $ t) = dest_coeff (~sign) t
   46.35    | dest_coeff sign t =
   46.36      let val ts = sort TermOrd.term_ord (dest_prod t)
   46.37          val (n, ts') = find_first_numeral [] ts
   46.38 @@ -96,7 +96,7 @@
   46.39    Fractions are reduced later by the cancel_numeral_factor simproc.*)
   46.40  fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
   46.41  
   46.42 -val mk_divide = HOLogic.mk_binop @{const_name HOL.divide};
   46.43 +val mk_divide = HOLogic.mk_binop @{const_name Algebras.divide};
   46.44  
   46.45  (*Build term (p / q) * t*)
   46.46  fun mk_fcoeff ((p, q), t) =
   46.47 @@ -104,8 +104,8 @@
   46.48    in mk_times (mk_divide (mk_number T p, mk_number T q), t) end;
   46.49  
   46.50  (*Express t as a product of a fraction with other sorted terms*)
   46.51 -fun dest_fcoeff sign (Const (@{const_name HOL.uminus}, _) $ t) = dest_fcoeff (~sign) t
   46.52 -  | dest_fcoeff sign (Const (@{const_name HOL.divide}, _) $ t $ u) =
   46.53 +fun dest_fcoeff sign (Const (@{const_name Algebras.uminus}, _) $ t) = dest_fcoeff (~sign) t
   46.54 +  | dest_fcoeff sign (Const (@{const_name Algebras.divide}, _) $ t $ u) =
   46.55      let val (p, t') = dest_coeff sign t
   46.56          val (q, u') = dest_coeff 1 u
   46.57      in (mk_frac (p, q), mk_divide (t', u')) end
   46.58 @@ -230,8 +230,8 @@
   46.59  structure LessCancelNumerals = CancelNumeralsFun
   46.60   (open CancelNumeralsCommon
   46.61    val prove_conv = Arith_Data.prove_conv
   46.62 -  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   46.63 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
   46.64 +  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
   46.65 +  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} Term.dummyT
   46.66    val bal_add1 = @{thm less_add_iff1} RS trans
   46.67    val bal_add2 = @{thm less_add_iff2} RS trans
   46.68  );
   46.69 @@ -239,8 +239,8 @@
   46.70  structure LeCancelNumerals = CancelNumeralsFun
   46.71   (open CancelNumeralsCommon
   46.72    val prove_conv = Arith_Data.prove_conv
   46.73 -  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   46.74 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
   46.75 +  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
   46.76 +  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} Term.dummyT
   46.77    val bal_add1 = @{thm le_add_iff1} RS trans
   46.78    val bal_add2 = @{thm le_add_iff2} RS trans
   46.79  );
   46.80 @@ -392,8 +392,8 @@
   46.81  structure DivideCancelNumeralFactor = CancelNumeralFactorFun
   46.82   (open CancelNumeralFactorCommon
   46.83    val prove_conv = Arith_Data.prove_conv
   46.84 -  val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
   46.85 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
   46.86 +  val mk_bal   = HOLogic.mk_binop @{const_name Algebras.divide}
   46.87 +  val dest_bal = HOLogic.dest_bin @{const_name Algebras.divide} Term.dummyT
   46.88    val cancel = @{thm mult_divide_mult_cancel_left} RS trans
   46.89    val neg_exchanges = false
   46.90  )
   46.91 @@ -410,8 +410,8 @@
   46.92  structure LessCancelNumeralFactor = CancelNumeralFactorFun
   46.93   (open CancelNumeralFactorCommon
   46.94    val prove_conv = Arith_Data.prove_conv
   46.95 -  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   46.96 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
   46.97 +  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
   46.98 +  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} Term.dummyT
   46.99    val cancel = @{thm mult_less_cancel_left} RS trans
  46.100    val neg_exchanges = true
  46.101  )
  46.102 @@ -419,8 +419,8 @@
  46.103  structure LeCancelNumeralFactor = CancelNumeralFactorFun
  46.104   (open CancelNumeralFactorCommon
  46.105    val prove_conv = Arith_Data.prove_conv
  46.106 -  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
  46.107 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
  46.108 +  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
  46.109 +  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} Term.dummyT
  46.110    val cancel = @{thm mult_le_cancel_left} RS trans
  46.111    val neg_exchanges = true
  46.112  )
  46.113 @@ -485,8 +485,8 @@
  46.114  in
  46.115  fun sign_conv pos_th neg_th ss t =
  46.116    let val T = fastype_of t;
  46.117 -      val zero = Const(@{const_name HOL.zero}, T);
  46.118 -      val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT);
  46.119 +      val zero = Const(@{const_name Algebras.zero}, T);
  46.120 +      val less = Const(@{const_name Algebras.less}, [T,T] ---> HOLogic.boolT);
  46.121        val pos = less $ zero $ t and neg = less $ t $ zero
  46.122        fun prove p =
  46.123          Option.map Eq_True_elim (Lin_Arith.simproc ss p)
  46.124 @@ -525,8 +525,8 @@
  46.125  structure LeCancelFactor = ExtractCommonTermFun
  46.126   (open CancelFactorCommon
  46.127    val prove_conv = Arith_Data.prove_conv
  46.128 -  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
  46.129 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT
  46.130 +  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less_eq}
  46.131 +  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less_eq} Term.dummyT
  46.132    val simp_conv = sign_conv
  46.133      @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg}
  46.134  );
  46.135 @@ -535,8 +535,8 @@
  46.136  structure LessCancelFactor = ExtractCommonTermFun
  46.137   (open CancelFactorCommon
  46.138    val prove_conv = Arith_Data.prove_conv
  46.139 -  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
  46.140 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT
  46.141 +  val mk_bal   = HOLogic.mk_binrel @{const_name Algebras.less}
  46.142 +  val dest_bal = HOLogic.dest_bin @{const_name Algebras.less} Term.dummyT
  46.143    val simp_conv = sign_conv
  46.144      @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg}
  46.145  );
  46.146 @@ -571,8 +571,8 @@
  46.147  structure DivideCancelFactor = ExtractCommonTermFun
  46.148   (open CancelFactorCommon
  46.149    val prove_conv = Arith_Data.prove_conv
  46.150 -  val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
  46.151 -  val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
  46.152 +  val mk_bal   = HOLogic.mk_binop @{const_name Algebras.divide}
  46.153 +  val dest_bal = HOLogic.dest_bin @{const_name Algebras.divide} Term.dummyT
  46.154    fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
  46.155  );
  46.156  
    47.1 --- a/src/HOL/Tools/refute.ML	Thu Jan 28 11:48:43 2010 +0100
    47.2 +++ b/src/HOL/Tools/refute.ML	Thu Jan 28 11:48:49 2010 +0100
    47.3 @@ -708,13 +708,13 @@
    47.4        (* other optimizations *)
    47.5        | Const (@{const_name Finite_Set.card}, _) => t
    47.6        | Const (@{const_name Finite_Set.finite}, _) => t
    47.7 -      | Const (@{const_name HOL.less}, Type ("fun", [Type ("nat", []),
    47.8 +      | Const (@{const_name Algebras.less}, Type ("fun", [Type ("nat", []),
    47.9          Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t
   47.10 -      | Const (@{const_name HOL.plus}, Type ("fun", [Type ("nat", []),
   47.11 +      | Const (@{const_name Algebras.plus}, Type ("fun", [Type ("nat", []),
   47.12          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
   47.13 -      | Const (@{const_name HOL.minus}, Type ("fun", [Type ("nat", []),
   47.14 +      | Const (@{const_name Algebras.minus}, Type ("fun", [Type ("nat", []),
   47.15          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
   47.16 -      | Const (@{const_name HOL.times}, Type ("fun", [Type ("nat", []),
   47.17 +      | Const (@{const_name Algebras.times}, Type ("fun", [Type ("nat", []),
   47.18          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
   47.19        | Const (@{const_name List.append}, _) => t
   47.20        | Const (@{const_name lfp}, _) => t
   47.21 @@ -883,16 +883,16 @@
   47.22        | Const (@{const_name Finite_Set.card}, T) => collect_type_axioms T axs
   47.23        | Const (@{const_name Finite_Set.finite}, T) =>
   47.24          collect_type_axioms T axs
   47.25 -      | Const (@{const_name HOL.less}, T as Type ("fun", [Type ("nat", []),
   47.26 +      | Const (@{const_name Algebras.less}, T as Type ("fun", [Type ("nat", []),
   47.27          Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
   47.28            collect_type_axioms T axs
   47.29 -      | Const (@{const_name HOL.plus}, T as Type ("fun", [Type ("nat", []),
   47.30 +      | Const (@{const_name Algebras.plus}, T as Type ("fun", [Type ("nat", []),
   47.31          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   47.32            collect_type_axioms T axs
   47.33 -      | Const (@{const_name HOL.minus}, T as Type ("fun", [Type ("nat", []),
   47.34 +      | Const (@{const_name Algebras.minus}, T as Type ("fun", [Type ("nat", []),
   47.35          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   47.36            collect_type_axioms T axs
   47.37 -      | Const (@{const_name HOL.times}, T as Type ("fun", [Type ("nat", []),
   47.38 +      | Const (@{const_name Algebras.times}, T as Type ("fun", [Type ("nat", []),
   47.39          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   47.40            collect_type_axioms T axs
   47.41        | Const (@{const_name List.append}, T) => collect_type_axioms T axs
   47.42 @@ -2765,13 +2765,13 @@
   47.43    (* theory -> model -> arguments -> Term.term ->
   47.44      (interpretation * model * arguments) option *)
   47.45  
   47.46 -  (* only an optimization: 'HOL.less' could in principle be interpreted with *)
   47.47 +  (* only an optimization: 'less' could in principle be interpreted with *)
   47.48    (* interpreters available already (using its definition), but the code     *)
   47.49    (* below is more efficient                                                 *)
   47.50  
   47.51    fun Nat_less_interpreter thy model args t =
   47.52      case t of
   47.53 -      Const (@{const_name HOL.less}, Type ("fun", [Type ("nat", []),
   47.54 +      Const (@{const_name Algebras.less}, Type ("fun", [Type ("nat", []),
   47.55          Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
   47.56        let
   47.57          val size_of_nat = size_of_type thy model (Type ("nat", []))
   47.58 @@ -2788,13 +2788,13 @@
   47.59    (* theory -> model -> arguments -> Term.term ->
   47.60      (interpretation * model * arguments) option *)
   47.61  
   47.62 -  (* only an optimization: 'HOL.plus' could in principle be interpreted with *)
   47.63 +  (* only an optimization: 'plus' could in principle be interpreted with *)
   47.64    (* interpreters available already (using its definition), but the code     *)
   47.65    (* below is more efficient                                                 *)
   47.66  
   47.67    fun Nat_plus_interpreter thy model args t =
   47.68      case t of
   47.69 -      Const (@{const_name HOL.plus}, Type ("fun", [Type ("nat", []),
   47.70 +      Const (@{const_name Algebras.plus}, Type ("fun", [Type ("nat", []),
   47.71          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   47.72        let
   47.73          val size_of_nat = size_of_type thy model (Type ("nat", []))
   47.74 @@ -2819,13 +2819,13 @@
   47.75    (* theory -> model -> arguments -> Term.term ->
   47.76      (interpretation * model * arguments) option *)
   47.77  
   47.78 -  (* only an optimization: 'HOL.minus' could in principle be interpreted *)
   47.79 +  (* only an optimization: 'minus' could in principle be interpreted *)
   47.80    (* with interpreters available already (using its definition), but the *)
   47.81    (* code below is more efficient                                        *)
   47.82  
   47.83    fun Nat_minus_interpreter thy model args t =
   47.84      case t of
   47.85 -      Const (@{const_name HOL.minus}, Type ("fun", [Type ("nat", []),
   47.86 +      Const (@{const_name Algebras.minus}, Type ("fun", [Type ("nat", []),
   47.87          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   47.88        let
   47.89          val size_of_nat = size_of_type thy model (Type ("nat", []))
   47.90 @@ -2847,13 +2847,13 @@
   47.91    (* theory -> model -> arguments -> Term.term ->
   47.92      (interpretation * model * arguments) option *)
   47.93  
   47.94 -  (* only an optimization: 'HOL.times' could in principle be interpreted *)
   47.95 +  (* only an optimization: 'times' could in principle be interpreted *)
   47.96    (* with interpreters available already (using its definition), but the *)
   47.97    (* code below is more efficient                                        *)
   47.98  
   47.99    fun Nat_times_interpreter thy model args t =
  47.100      case t of
  47.101 -      Const (@{const_name HOL.times}, Type ("fun", [Type ("nat", []),
  47.102 +      Const (@{const_name Algebras.times}, Type ("fun", [Type ("nat", []),
  47.103          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
  47.104        let
  47.105          val size_of_nat = size_of_type thy model (Type ("nat", []))
    48.1 --- a/src/HOL/Tools/res_clause.ML	Thu Jan 28 11:48:43 2010 +0100
    48.2 +++ b/src/HOL/Tools/res_clause.ML	Thu Jan 28 11:48:49 2010 +0100
    48.3 @@ -99,7 +99,7 @@
    48.4  (*Provide readable names for the more common symbolic functions*)
    48.5  val const_trans_table =
    48.6        Symtab.make [(@{const_name "op ="}, "equal"),
    48.7 -                   (@{const_name HOL.less_eq}, "lessequals"),
    48.8 +                   (@{const_name Algebras.less_eq}, "lessequals"),
    48.9                     (@{const_name "op &"}, "and"),
   48.10                     (@{const_name "op |"}, "or"),
   48.11                     (@{const_name "op -->"}, "implies"),
    49.1 --- a/src/HOL/Transcendental.thy	Thu Jan 28 11:48:43 2010 +0100
    49.2 +++ b/src/HOL/Transcendental.thy	Thu Jan 28 11:48:49 2010 +0100
    49.3 @@ -36,7 +36,7 @@
    49.4  apply (subst setsum_op_ivl_Suc)
    49.5  apply (subst lemma_realpow_diff_sumr)
    49.6  apply (simp add: right_distrib del: setsum_op_ivl_Suc)
    49.7 -apply (subst mult_left_commute [where a="x - y"])
    49.8 +apply (subst mult_left_commute [of "x - y"])
    49.9  apply (erule subst)
   49.10  apply (simp add: algebra_simps)
   49.11  done
    50.1 --- a/src/HOL/ex/Arith_Examples.thy	Thu Jan 28 11:48:43 2010 +0100
    50.2 +++ b/src/HOL/ex/Arith_Examples.thy	Thu Jan 28 11:48:49 2010 +0100
    50.3 @@ -33,7 +33,7 @@
    50.4  *)
    50.5  
    50.6  subsection {* Splitting of Operators: @{term max}, @{term min}, @{term abs},
    50.7 -           @{term HOL.minus}, @{term nat}, @{term Divides.mod},
    50.8 +           @{term Algebras.minus}, @{term nat}, @{term Divides.mod},
    50.9             @{term Divides.div} *}
   50.10  
   50.11  lemma "(i::nat) <= max i j"
    51.1 --- a/src/HOL/ex/Binary.thy	Thu Jan 28 11:48:43 2010 +0100
    51.2 +++ b/src/HOL/ex/Binary.thy	Thu Jan 28 11:48:49 2010 +0100
    51.3 @@ -27,8 +27,8 @@
    51.4      | dest_bit (Const (@{const_name True}, _)) = 1
    51.5      | dest_bit t = raise TERM ("dest_bit", [t]);
    51.6  
    51.7 -  fun dest_binary (Const (@{const_name HOL.zero}, Type (@{type_name nat}, _))) = 0
    51.8 -    | dest_binary (Const (@{const_name HOL.one}, Type (@{type_name nat}, _))) = 1
    51.9 +  fun dest_binary (Const (@{const_name Algebras.zero}, Type (@{type_name nat}, _))) = 0
   51.10 +    | dest_binary (Const (@{const_name Algebras.one}, Type (@{type_name nat}, _))) = 1
   51.11      | dest_binary (Const (@{const_name bit}, _) $ bs $ b) = 2 * dest_binary bs + dest_bit b
   51.12      | dest_binary t = raise TERM ("dest_binary", [t]);
   51.13  
    52.1 --- a/src/HOL/ex/SVC_Oracle.thy	Thu Jan 28 11:48:43 2010 +0100
    52.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Thu Jan 28 11:48:49 2010 +0100
    52.3 @@ -63,21 +63,21 @@
    52.4      (*abstraction of a numeric literal*)
    52.5      fun lit t = if can HOLogic.dest_number t then t else replace t;
    52.6      (*abstraction of a real/rational expression*)
    52.7 -    fun rat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    52.8 -      | rat ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    52.9 -      | rat ((c as Const(@{const_name HOL.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
   52.10 -      | rat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
   52.11 -      | rat ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (rat x)
   52.12 +    fun rat ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
   52.13 +      | rat ((c as Const(@{const_name Algebras.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
   52.14 +      | rat ((c as Const(@{const_name Algebras.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
   52.15 +      | rat ((c as Const(@{const_name Algebras.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
   52.16 +      | rat ((c as Const(@{const_name Algebras.uminus}, _)) $ x) = c $ (rat x)
   52.17        | rat t = lit t
   52.18      (*abstraction of an integer expression: no div, mod*)
   52.19 -    fun int ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (int x) $ (int y)
   52.20 -      | int ((c as Const(@{const_name HOL.minus}, _)) $ x $ y) = c $ (int x) $ (int y)
   52.21 -      | int ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (int x) $ (int y)
   52.22 -      | int ((c as Const(@{const_name HOL.uminus}, _)) $ x) = c $ (int x)
   52.23 +    fun int ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (int x) $ (int y)
   52.24 +      | int ((c as Const(@{const_name Algebras.minus}, _)) $ x $ y) = c $ (int x) $ (int y)
   52.25 +      | int ((c as Const(@{const_name Algebras.times}, _)) $ x $ y) = c $ (int x) $ (int y)
   52.26 +      | int ((c as Const(@{const_name Algebras.uminus}, _)) $ x) = c $ (int x)
   52.27        | int t = lit t
   52.28      (*abstraction of a natural number expression: no minus*)
   52.29 -    fun nat ((c as Const(@{const_name HOL.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y)
   52.30 -      | nat ((c as Const(@{const_name HOL.times}, _)) $ x $ y) = c $ (nat x) $ (nat y)
   52.31 +    fun nat ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y)
   52.32 +      | nat ((c as Const(@{const_name Algebras.times}, _)) $ x $ y) = c $ (nat x) $ (nat y)
   52.33        | nat ((c as Const(@{const_name Suc}, _)) $ x) = c $ (nat x)
   52.34        | nat t = lit t
   52.35      (*abstraction of a relation: =, <, <=*)
   52.36 @@ -95,8 +95,8 @@
   52.37        | fm ((c as Const("True", _))) = c
   52.38        | fm ((c as Const("False", _))) = c
   52.39        | fm (t as Const("op =",  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
   52.40 -      | fm (t as Const(@{const_name HOL.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
   52.41 -      | fm (t as Const(@{const_name HOL.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
   52.42 +      | fm (t as Const(@{const_name Algebras.less},  Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
   52.43 +      | fm (t as Const(@{const_name Algebras.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
   52.44        | fm t = replace t
   52.45      (*entry point, and abstraction of a meta-formula*)
   52.46      fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
    53.1 --- a/src/HOL/ex/svc_funcs.ML	Thu Jan 28 11:48:43 2010 +0100
    53.2 +++ b/src/HOL/ex/svc_funcs.ML	Thu Jan 28 11:48:49 2010 +0100
    53.3 @@ -107,8 +107,8 @@
    53.4                           b1 orelse b2)
    53.5                       end
    53.6                   else (*might be numeric equality*) (t, is_intnat T)
    53.7 -           | Const(@{const_name HOL.less}, Type ("fun", [T,_]))  => (t, is_intnat T)
    53.8 -           | Const(@{const_name HOL.less_eq}, Type ("fun", [T,_])) => (t, is_intnat T)
    53.9 +           | Const(@{const_name Algebras.less}, Type ("fun", [T,_]))  => (t, is_intnat T)
   53.10 +           | Const(@{const_name Algebras.less_eq}, Type ("fun", [T,_])) => (t, is_intnat T)
   53.11             | _ => (t, false)
   53.12           end
   53.13     in #1 o tag end;
   53.14 @@ -146,16 +146,16 @@
   53.15      (*translation of a literal*)
   53.16      val lit = snd o HOLogic.dest_number;
   53.17      (*translation of a literal expression [no variables]*)
   53.18 -    fun litExp (Const(@{const_name HOL.plus}, T) $ x $ y) =
   53.19 +    fun litExp (Const(@{const_name Algebras.plus}, T) $ x $ y) =
   53.20            if is_numeric_op T then (litExp x) + (litExp y)
   53.21            else fail t
   53.22 -      | litExp (Const(@{const_name HOL.minus}, T) $ x $ y) =
   53.23 +      | litExp (Const(@{const_name Algebras.minus}, T) $ x $ y) =
   53.24            if is_numeric_op T then (litExp x) - (litExp y)
   53.25            else fail t
   53.26 -      | litExp (Const(@{const_name HOL.times}, T) $ x $ y) =
   53.27 +      | litExp (Const(@{const_name Algebras.times}, T) $ x $ y) =
   53.28            if is_numeric_op T then (litExp x) * (litExp y)
   53.29            else fail t
   53.30 -      | litExp (Const(@{const_name HOL.uminus}, T) $ x)   =
   53.31 +      | litExp (Const(@{const_name Algebras.uminus}, T) $ x)   =
   53.32            if is_numeric_op T then ~(litExp x)
   53.33            else fail t
   53.34        | litExp t = lit t
   53.35 @@ -163,21 +163,21 @@
   53.36      (*translation of a real/rational expression*)
   53.37      fun suc t = Interp("+", [Int 1, t])
   53.38      fun tm (Const(@{const_name Suc}, T) $ x) = suc (tm x)
   53.39 -      | tm (Const(@{const_name HOL.plus}, T) $ x $ y) =
   53.40 +      | tm (Const(@{const_name Algebras.plus}, T) $ x $ y) =
   53.41            if is_numeric_op T then Interp("+", [tm x, tm y])
   53.42            else fail t
   53.43 -      | tm (Const(@{const_name HOL.minus}, T) $ x $ y) =
   53.44 +      | tm (Const(@{const_name Algebras.minus}, T) $ x $ y) =
   53.45            if is_numeric_op T then
   53.46                Interp("+", [tm x, Interp("*", [Int ~1, tm y])])
   53.47            else fail t
   53.48 -      | tm (Const(@{const_name HOL.times}, T) $ x $ y) =
   53.49 +      | tm (Const(@{const_name Algebras.times}, T) $ x $ y) =
   53.50            if is_numeric_op T then Interp("*", [tm x, tm y])
   53.51            else fail t
   53.52 -      | tm (Const(@{const_name HOL.inverse}, T) $ x) =
   53.53 +      | tm (Const(@{const_name Algebras.inverse}, T) $ x) =
   53.54            if domain_type T = HOLogic.realT then
   53.55                Rat(1, litExp x)
   53.56            else fail t
   53.57 -      | tm (Const(@{const_name HOL.uminus}, T) $ x) =
   53.58 +      | tm (Const(@{const_name Algebras.uminus}, T) $ x) =
   53.59            if is_numeric_op T then Interp("*", [Int ~1, tm x])
   53.60            else fail t
   53.61        | tm t = Int (lit t)
   53.62 @@ -211,13 +211,13 @@
   53.63                     else fail t
   53.64              end
   53.65          (*inequalities: possible types are nat, int, real*)
   53.66 -      | fm pos (t as Const(@{const_name HOL.less},  Type ("fun", [T,_])) $ x $ y) =
   53.67 +      | fm pos (t as Const(@{const_name Algebras.less},  Type ("fun", [T,_])) $ x $ y) =
   53.68              if not pos orelse T = HOLogic.realT then
   53.69                  Buildin("<", [tm x, tm y])
   53.70              else if is_intnat T then
   53.71                  Buildin("<=", [suc (tm x), tm y])
   53.72              else fail t
   53.73 -      | fm pos (t as Const(@{const_name HOL.less_eq},  Type ("fun", [T,_])) $ x $ y) =
   53.74 +      | fm pos (t as Const(@{const_name Algebras.less_eq},  Type ("fun", [T,_])) $ x $ y) =
   53.75              if pos orelse T = HOLogic.realT then
   53.76                  Buildin("<=", [tm x, tm y])
   53.77              else if is_intnat T then
    54.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Jan 28 11:48:43 2010 +0100
    54.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Jan 28 11:48:49 2010 +0100
    54.3 @@ -719,7 +719,7 @@
    54.4    val take_stricts' = rewrite_rule copy_take_defs take_stricts;
    54.5    fun take_0 n dn =
    54.6      let
    54.7 -      val goal = mk_trp ((dc_take dn $ %%:"HOL.zero") `% x_name n === UU);
    54.8 +      val goal = mk_trp ((dc_take dn $ %%: @{const_name Algebras.zero}) `% x_name n === UU);
    54.9      in pg axs_take_def goal (K [simp_tac iterate_Cprod_ss 1]) end;
   54.10    val take_0s = mapn take_0 1 dnames;
   54.11    fun c_UU_tac ctxt = case_UU_tac ctxt (take_stricts'::copy_con_rews) 1;
    55.1 --- a/src/Provers/Arith/abel_cancel.ML	Thu Jan 28 11:48:43 2010 +0100
    55.2 +++ b/src/Provers/Arith/abel_cancel.ML	Thu Jan 28 11:48:49 2010 +0100
    55.3 @@ -28,29 +28,29 @@
    55.4  
    55.5  (* FIXME dependent on abstract syntax *)
    55.6  
    55.7 -fun zero t = Const (@{const_name HOL.zero}, t);
    55.8 -fun minus t = Const (@{const_name HOL.uminus}, t --> t);
    55.9 +fun zero t = Const (@{const_name Algebras.zero}, t);
   55.10 +fun minus t = Const (@{const_name Algebras.uminus}, t --> t);
   55.11  
   55.12 -fun add_terms pos (Const (@{const_name HOL.plus}, _) $ x $ y, ts) =
   55.13 +fun add_terms pos (Const (@{const_name Algebras.plus}, _) $ x $ y, ts) =
   55.14        add_terms pos (x, add_terms pos (y, ts))
   55.15 -  | add_terms pos (Const (@{const_name HOL.minus}, _) $ x $ y, ts) =
   55.16 +  | add_terms pos (Const (@{const_name Algebras.minus}, _) $ x $ y, ts) =
   55.17        add_terms pos (x, add_terms (not pos) (y, ts))
   55.18 -  | add_terms pos (Const (@{const_name HOL.uminus}, _) $ x, ts) =
   55.19 +  | add_terms pos (Const (@{const_name Algebras.uminus}, _) $ x, ts) =
   55.20        add_terms (not pos) (x, ts)
   55.21    | add_terms pos (x, ts) = (pos,x) :: ts;
   55.22  
   55.23  fun terms fml = add_terms true (fml, []);
   55.24  
   55.25 -fun zero1 pt (u as (c as Const(@{const_name HOL.plus},_)) $ x $ y) =
   55.26 +fun zero1 pt (u as (c as Const(@{const_name Algebras.plus},_)) $ x $ y) =
   55.27        (case zero1 pt x of NONE => (case zero1 pt y of NONE => NONE
   55.28                                     | SOME z => SOME(c $ x $ z))
   55.29         | SOME z => SOME(c $ z $ y))
   55.30 -  | zero1 (pos,t) (u as (c as Const(@{const_name HOL.minus},_)) $ x $ y) =
   55.31 +  | zero1 (pos,t) (u as (c as Const(@{const_name Algebras.minus},_)) $ x $ y) =
   55.32        (case zero1 (pos,t) x of
   55.33           NONE => (case zero1 (not pos,t) y of NONE => NONE
   55.34                    | SOME z => SOME(c $ x $ z))
   55.35         | SOME z => SOME(c $ z $ y))
   55.36 -  | zero1 (pos,t) (u as (c as Const(@{const_name HOL.uminus},_)) $ x) =
   55.37 +  | zero1 (pos,t) (u as (c as Const(@{const_name Algebras.uminus},_)) $ x) =
   55.38        (case zero1 (not pos,t) x of NONE => NONE
   55.39         | SOME z => SOME(c $ z))
   55.40    | zero1 (pos,t) u =
   55.41 @@ -71,7 +71,7 @@
   55.42  fun cancel t =
   55.43    let
   55.44      val c $ lhs $ rhs = t
   55.45 -    val opp = case c of Const(@{const_name HOL.plus},_) => true | _ => false;
   55.46 +    val opp = case c of Const(@{const_name Algebras.plus},_) => true | _ => false;
   55.47      val (pos,l) = find_common opp (terms lhs) (terms rhs)
   55.48      val posr = if opp then not pos else pos
   55.49      val t' = c $ (the(zero1 (pos,l) lhs)) $ (the(zero1 (posr,l) rhs))
    56.1 --- a/src/Provers/Arith/cancel_div_mod.ML	Thu Jan 28 11:48:43 2010 +0100
    56.2 +++ b/src/Provers/Arith/cancel_div_mod.ML	Thu Jan 28 11:48:49 2010 +0100
    56.3 @@ -1,5 +1,4 @@
    56.4  (*  Title:      Provers/Arith/cancel_div_mod.ML
    56.5 -    ID:         $Id$
    56.6      Author:     Tobias Nipkow, TU Muenchen
    56.7  
    56.8  Cancel div and mod terms:
    56.9 @@ -7,7 +6,7 @@
   56.10    A + n*(m div n) + B + (m mod n) + C  ==  A + B + C + m
   56.11  
   56.12  FIXME: Is parameterized but assumes for simplicity that + and * are named
   56.13 -HOL.plus and HOL.minus
   56.14 +as in HOL
   56.15  *)
   56.16  
   56.17  signature CANCEL_DIV_MOD_DATA =
   56.18 @@ -35,12 +34,12 @@
   56.19  functor CancelDivModFun(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
   56.20  struct
   56.21  
   56.22 -fun coll_div_mod (Const(@{const_name HOL.plus},_) $ s $ t) dms =
   56.23 +fun coll_div_mod (Const(@{const_name Algebras.plus},_) $ s $ t) dms =
   56.24        coll_div_mod t (coll_div_mod s dms)
   56.25 -  | coll_div_mod (Const(@{const_name HOL.times},_) $ m $ (Const(d,_) $ s $ n))
   56.26 +  | coll_div_mod (Const(@{const_name Algebras.times},_) $ m $ (Const(d,_) $ s $ n))
   56.27                   (dms as (divs,mods)) =
   56.28        if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
   56.29 -  | coll_div_mod (Const(@{const_name HOL.times},_) $ (Const(d,_) $ s $ n) $ m)
   56.30 +  | coll_div_mod (Const(@{const_name Algebras.times},_) $ (Const(d,_) $ s $ n) $ m)
   56.31                   (dms as (divs,mods)) =
   56.32        if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
   56.33    | coll_div_mod (Const(m,_) $ s $ n) (dms as (divs,mods)) =
   56.34 @@ -56,8 +55,8 @@
   56.35     ==> thesis by transitivity
   56.36  *)
   56.37  
   56.38 -val mk_plus = Data.mk_binop @{const_name HOL.plus};
   56.39 -val mk_times = Data.mk_binop @{const_name HOL.times};
   56.40 +val mk_plus = Data.mk_binop @{const_name Algebras.plus};
   56.41 +val mk_times = Data.mk_binop @{const_name Algebras.times};
   56.42  
   56.43  fun rearrange t pq =
   56.44    let val ts = Data.dest_sum t;