moved remaning class operations from Algebras.thy to Groups.thy
authorhaftmann
Fri Feb 19 14:47:01 2010 +0100 (2010-02-19)
changeset 352678dfd816713c6
parent 35266 07a56610c00b
child 35268 04673275441a
moved remaning class operations from Algebras.thy to Groups.thy
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/Finite_Set.thy
src/HOL/Groups.thy
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/real.imp
src/HOL/Import/HOL/realax.imp
src/HOL/Import/HOLLight/hollight.imp
src/HOL/Library/SetsAndFunctions.thy
src/HOL/List.thy
src/HOL/Mutabelle/Mutabelle.thy
src/HOL/NSA/NSA.thy
src/HOL/Tools/Function/size.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/presburger.ML
src/HOL/Tools/arith_data.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/int_arith.ML
src/HOL/Tools/lin_arith.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/ex/Arith_Examples.thy
src/HOL/ex/Binary.thy
src/HOL/ex/SVC_Oracle.thy
src/HOL/ex/Summation.thy
src/HOL/ex/svc_funcs.ML
src/Provers/Arith/abel_cancel.ML
src/Provers/Arith/cancel_div_mod.ML
     1.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Fri Feb 19 14:47:00 2010 +0100
     1.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Fri Feb 19 14:47:01 2010 +0100
     1.3 @@ -205,8 +205,8 @@
     1.4  ML {*
     1.5  fun ring_ord (Const (a, _)) =
     1.6      find_index (fn a' => a = a')
     1.7 -      [@{const_name Algebras.zero}, @{const_name Algebras.plus}, @{const_name Algebras.uminus},
     1.8 -        @{const_name Algebras.minus}, @{const_name Algebras.one}, @{const_name Algebras.times}]
     1.9 +      [@{const_name Groups.zero}, @{const_name Groups.plus}, @{const_name Groups.uminus},
    1.10 +        @{const_name Groups.minus}, @{const_name Groups.one}, @{const_name Groups.times}]
    1.11    | ring_ord _ = ~1;
    1.12  
    1.13  fun termless_ring (a, b) = (TermOrd.term_lpo ring_ord (a, b) = LESS);
     2.1 --- a/src/HOL/Algebras.thy	Fri Feb 19 14:47:00 2010 +0100
     2.2 +++ b/src/HOL/Algebras.thy	Fri Feb 19 14:47:01 2010 +0100
     2.3 @@ -8,8 +8,6 @@
     2.4  imports HOL
     2.5  begin
     2.6  
     2.7 -subsection {* Generic algebraic structures *}
     2.8 -
     2.9  text {*
    2.10    These locales provide basic structures for interpretation into
    2.11    bigger structures;  extensions require careful thinking, otherwise
    2.12 @@ -54,58 +52,4 @@
    2.13  
    2.14  end
    2.15  
    2.16 -
    2.17 -subsection {* Generic syntactic operations *}
    2.18 -
    2.19 -class zero = 
    2.20 -  fixes zero :: 'a  ("0")
    2.21 -
    2.22 -class one =
    2.23 -  fixes one  :: 'a  ("1")
    2.24 -
    2.25 -hide (open) const zero one
    2.26 -
    2.27 -syntax
    2.28 -  "_index1"  :: index    ("\<^sub>1")
    2.29 -translations
    2.30 -  (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
    2.31 -
    2.32 -lemma Let_0 [simp]: "Let 0 f = f 0"
    2.33 -  unfolding Let_def ..
    2.34 -
    2.35 -lemma Let_1 [simp]: "Let 1 f = f 1"
    2.36 -  unfolding Let_def ..
    2.37 -
    2.38 -setup {*
    2.39 -  Reorient_Proc.add
    2.40 -    (fn Const(@{const_name Algebras.zero}, _) => true
    2.41 -      | Const(@{const_name Algebras.one}, _) => true
    2.42 -      | _ => false)
    2.43 -*}
    2.44 -
    2.45 -simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
    2.46 -simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
    2.47 -
    2.48 -typed_print_translation {*
    2.49 -let
    2.50 -  fun tr' c = (c, fn show_sorts => fn T => fn ts =>
    2.51 -    if (not o null) ts orelse T = dummyT
    2.52 -      orelse not (! show_types) andalso can Term.dest_Type T
    2.53 -    then raise Match
    2.54 -    else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
    2.55 -in map tr' [@{const_syntax Algebras.one}, @{const_syntax Algebras.zero}] end;
    2.56 -*} -- {* show types that are presumably too general *}
    2.57 -
    2.58 -class plus =
    2.59 -  fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
    2.60 -
    2.61 -class minus =
    2.62 -  fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
    2.63 -
    2.64 -class uminus =
    2.65 -  fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
    2.66 -
    2.67 -class times =
    2.68 -  fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
    2.69 -
    2.70  end
    2.71 \ No newline at end of file
     3.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Fri Feb 19 14:47:00 2010 +0100
     3.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Fri Feb 19 14:47:01 2010 +0100
     3.3 @@ -670,13 +670,13 @@
     3.4   end
     3.5  
     3.6  fun whatis x ct = case term_of ct of
     3.7 -  Const(@{const_name Algebras.plus}, _)$(Const(@{const_name Algebras.times},_)$_$y)$_ =>
     3.8 +  Const(@{const_name Groups.plus}, _)$(Const(@{const_name Groups.times},_)$_$y)$_ =>
     3.9       if y aconv term_of x then ("c*x+t",[(funpow 2 Thm.dest_arg1) ct, Thm.dest_arg ct])
    3.10       else ("Nox",[])
    3.11 -| Const(@{const_name Algebras.plus}, _)$y$_ =>
    3.12 +| Const(@{const_name Groups.plus}, _)$y$_ =>
    3.13       if y aconv term_of x then ("x+t",[Thm.dest_arg ct])
    3.14       else ("Nox",[])
    3.15 -| Const(@{const_name Algebras.times}, _)$_$y =>
    3.16 +| Const(@{const_name Groups.times}, _)$_$y =>
    3.17       if y aconv term_of x then ("c*x",[Thm.dest_arg1 ct])
    3.18       else ("Nox",[])
    3.19  | t => if t aconv term_of x then ("x",[]) else ("Nox",[]);
    3.20 @@ -684,7 +684,7 @@
    3.21  fun xnormalize_conv ctxt [] ct = reflexive ct
    3.22  | xnormalize_conv ctxt (vs as (x::_)) ct =
    3.23     case term_of ct of
    3.24 -   Const(@{const_name Orderings.less},_)$_$Const(@{const_name Algebras.zero},_) =>
    3.25 +   Const(@{const_name Orderings.less},_)$_$Const(@{const_name Groups.zero},_) =>
    3.26      (case whatis x (Thm.dest_arg1 ct) of
    3.27      ("c*x+t",[c,t]) =>
    3.28         let
    3.29 @@ -727,7 +727,7 @@
    3.30      | _ => reflexive ct)
    3.31  
    3.32  
    3.33 -|  Const(@{const_name Orderings.less_eq},_)$_$Const(@{const_name Algebras.zero},_) =>
    3.34 +|  Const(@{const_name Orderings.less_eq},_)$_$Const(@{const_name Groups.zero},_) =>
    3.35     (case whatis x (Thm.dest_arg1 ct) of
    3.36      ("c*x+t",[c,t]) =>
    3.37         let
    3.38 @@ -771,7 +771,7 @@
    3.39        in rth end
    3.40      | _ => reflexive ct)
    3.41  
    3.42 -|  Const("op =",_)$_$Const(@{const_name Algebras.zero},_) =>
    3.43 +|  Const("op =",_)$_$Const(@{const_name Groups.zero},_) =>
    3.44     (case whatis x (Thm.dest_arg1 ct) of
    3.45      ("c*x+t",[c,t]) =>
    3.46         let
     4.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Feb 19 14:47:00 2010 +0100
     4.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Fri Feb 19 14:47:01 2010 +0100
     4.3 @@ -2947,10 +2947,10 @@
     4.4  fun rrelT rT = [rT,rT] ---> rT;
     4.5  fun rrT rT = [rT, rT] ---> bT;
     4.6  fun divt rT = Const(@{const_name Rings.divide},rrelT rT);
     4.7 -fun timest rT = Const(@{const_name Algebras.times},rrelT rT);
     4.8 -fun plust rT = Const(@{const_name Algebras.plus},rrelT rT);
     4.9 -fun minust rT = Const(@{const_name Algebras.minus},rrelT rT);
    4.10 -fun uminust rT = Const(@{const_name Algebras.uminus}, rT --> rT);
    4.11 +fun timest rT = Const(@{const_name Groups.times},rrelT rT);
    4.12 +fun plust rT = Const(@{const_name Groups.plus},rrelT rT);
    4.13 +fun minust rT = Const(@{const_name Groups.minus},rrelT rT);
    4.14 +fun uminust rT = Const(@{const_name Groups.uminus}, rT --> rT);
    4.15  fun powt rT = Const(@{const_name "power"}, [rT,@{typ "nat"}] ---> rT);
    4.16  val brT = [bT, bT] ---> bT;
    4.17  val nott = @{term "Not"};
    4.18 @@ -2961,7 +2961,7 @@
    4.19  fun llt rT = Const(@{const_name Orderings.less},rrT rT);
    4.20  fun lle rT = Const(@{const_name Orderings.less},rrT rT);
    4.21  fun eqt rT = Const("op =",rrT rT);
    4.22 -fun rz rT = Const(@{const_name Algebras.zero},rT);
    4.23 +fun rz rT = Const(@{const_name Groups.zero},rT);
    4.24  
    4.25  fun dest_nat t = case t of
    4.26    Const ("Suc",_)$t' => 1 + dest_nat t'
    4.27 @@ -2969,10 +2969,10 @@
    4.28  
    4.29  fun num_of_term m t = 
    4.30   case t of
    4.31 -   Const(@{const_name Algebras.uminus},_)$t => @{code poly.Neg} (num_of_term m t)
    4.32 - | Const(@{const_name Algebras.plus},_)$a$b => @{code poly.Add} (num_of_term m a, num_of_term m b)
    4.33 - | Const(@{const_name Algebras.minus},_)$a$b => @{code poly.Sub} (num_of_term m a, num_of_term m b)
    4.34 - | Const(@{const_name Algebras.times},_)$a$b => @{code poly.Mul} (num_of_term m a, num_of_term m b)
    4.35 +   Const(@{const_name Groups.uminus},_)$t => @{code poly.Neg} (num_of_term m t)
    4.36 + | Const(@{const_name Groups.plus},_)$a$b => @{code poly.Add} (num_of_term m a, num_of_term m b)
    4.37 + | Const(@{const_name Groups.minus},_)$a$b => @{code poly.Sub} (num_of_term m a, num_of_term m b)
    4.38 + | Const(@{const_name Groups.times},_)$a$b => @{code poly.Mul} (num_of_term m a, num_of_term m b)
    4.39   | Const(@{const_name Power.power},_)$a$n => @{code poly.Pw} (num_of_term m a, dest_nat n)
    4.40   | Const(@{const_name Rings.divide},_)$a$b => @{code poly.C} (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
    4.41   | _ => (@{code poly.C} (HOLogic.dest_number t |> snd,1) 
    4.42 @@ -2980,10 +2980,10 @@
    4.43  
    4.44  fun tm_of_term m m' t = 
    4.45   case t of
    4.46 -   Const(@{const_name Algebras.uminus},_)$t => @{code Neg} (tm_of_term m m' t)
    4.47 - | Const(@{const_name Algebras.plus},_)$a$b => @{code Add} (tm_of_term m m' a, tm_of_term m m' b)
    4.48 - | Const(@{const_name Algebras.minus},_)$a$b => @{code Sub} (tm_of_term m m' a, tm_of_term m m' b)
    4.49 - | Const(@{const_name Algebras.times},_)$a$b => @{code Mul} (num_of_term m' a, tm_of_term m m' b)
    4.50 +   Const(@{const_name Groups.uminus},_)$t => @{code Neg} (tm_of_term m m' t)
    4.51 + | Const(@{const_name Groups.plus},_)$a$b => @{code Add} (tm_of_term m m' a, tm_of_term m m' b)
    4.52 + | Const(@{const_name Groups.minus},_)$a$b => @{code Sub} (tm_of_term m m' a, tm_of_term m m' b)
    4.53 + | Const(@{const_name Groups.times},_)$a$b => @{code Mul} (num_of_term m' a, tm_of_term m m' b)
    4.54   | _ => (@{code CP} (num_of_term m' t) 
    4.55           handle TERM _ => @{code Bound} (AList.lookup (op aconv) m t |> the)
    4.56                | Option => @{code Bound} (AList.lookup (op aconv) m t |> the));
     5.1 --- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Fri Feb 19 14:47:00 2010 +0100
     5.2 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Fri Feb 19 14:47:01 2010 +0100
     5.3 @@ -13,8 +13,8 @@
     5.4  struct
     5.5  
     5.6  (* Zero and One of the commutative ring *)
     5.7 -fun cring_zero T = Const (@{const_name Algebras.zero}, T);
     5.8 -fun cring_one T = Const (@{const_name Algebras.one}, T);
     5.9 +fun cring_zero T = Const (@{const_name Groups.zero}, T);
    5.10 +fun cring_one T = Const (@{const_name Groups.one}, T);
    5.11  
    5.12  (* reification functions *)
    5.13  (* add two polynom expressions *)
    5.14 @@ -49,13 +49,13 @@
    5.15    | reif_pol T vs t = pol_Pc T $ t;
    5.16  
    5.17  (* reification of polynom expressions *)
    5.18 -fun reif_polex T vs (Const (@{const_name Algebras.plus}, _) $ a $ b) =
    5.19 +fun reif_polex T vs (Const (@{const_name Groups.plus}, _) $ a $ b) =
    5.20        polex_add T $ reif_polex T vs a $ reif_polex T vs b
    5.21 -  | reif_polex T vs (Const (@{const_name Algebras.minus}, _) $ a $ b) =
    5.22 +  | reif_polex T vs (Const (@{const_name Groups.minus}, _) $ a $ b) =
    5.23        polex_sub T $ reif_polex T vs a $ reif_polex T vs b
    5.24 -  | reif_polex T vs (Const (@{const_name Algebras.times}, _) $ a $ b) =
    5.25 +  | reif_polex T vs (Const (@{const_name Groups.times}, _) $ a $ b) =
    5.26        polex_mul T $ reif_polex T vs a $ reif_polex T vs b
    5.27 -  | reif_polex T vs (Const (@{const_name Algebras.uminus}, _) $ a) =
    5.28 +  | reif_polex T vs (Const (@{const_name Groups.uminus}, _) $ a) =
    5.29        polex_neg T $ reif_polex T vs a
    5.30    | reif_polex T vs (Const (@{const_name Power.power}, _) $ a $ n) =
    5.31        polex_pow T $ reif_polex T vs a $ n
     6.1 --- a/src/HOL/Finite_Set.thy	Fri Feb 19 14:47:00 2010 +0100
     6.2 +++ b/src/HOL/Finite_Set.thy	Fri Feb 19 14:47:01 2010 +0100
     6.3 @@ -1055,7 +1055,7 @@
     6.4  
     6.5  subsection {* Generalized summation over a set *}
     6.6  
     6.7 -interpretation comm_monoid_add: comm_monoid_mult "0::'a::comm_monoid_add" "op +"
     6.8 +interpretation comm_monoid_add: comm_monoid_mult "op +" "0::'a::comm_monoid_add"
     6.9    proof qed (auto intro: add_assoc add_commute)
    6.10  
    6.11  definition setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
     7.1 --- a/src/HOL/Groups.thy	Fri Feb 19 14:47:00 2010 +0100
     7.2 +++ b/src/HOL/Groups.thy	Fri Feb 19 14:47:01 2010 +0100
     7.3 @@ -6,9 +6,64 @@
     7.4  
     7.5  theory Groups
     7.6  imports Orderings
     7.7 -uses "~~/src/Provers/Arith/abel_cancel.ML"
     7.8 +uses ("~~/src/Provers/Arith/abel_cancel.ML")
     7.9  begin
    7.10  
    7.11 +subsection {* Generic operations *}
    7.12 +
    7.13 +class zero = 
    7.14 +  fixes zero :: 'a  ("0")
    7.15 +
    7.16 +class one =
    7.17 +  fixes one  :: 'a  ("1")
    7.18 +
    7.19 +hide (open) const zero one
    7.20 +
    7.21 +syntax
    7.22 +  "_index1"  :: index    ("\<^sub>1")
    7.23 +translations
    7.24 +  (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
    7.25 +
    7.26 +lemma Let_0 [simp]: "Let 0 f = f 0"
    7.27 +  unfolding Let_def ..
    7.28 +
    7.29 +lemma Let_1 [simp]: "Let 1 f = f 1"
    7.30 +  unfolding Let_def ..
    7.31 +
    7.32 +setup {*
    7.33 +  Reorient_Proc.add
    7.34 +    (fn Const(@{const_name Groups.zero}, _) => true
    7.35 +      | Const(@{const_name Groups.one}, _) => true
    7.36 +      | _ => false)
    7.37 +*}
    7.38 +
    7.39 +simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
    7.40 +simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
    7.41 +
    7.42 +typed_print_translation {*
    7.43 +let
    7.44 +  fun tr' c = (c, fn show_sorts => fn T => fn ts =>
    7.45 +    if (not o null) ts orelse T = dummyT
    7.46 +      orelse not (! show_types) andalso can Term.dest_Type T
    7.47 +    then raise Match
    7.48 +    else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
    7.49 +in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
    7.50 +*} -- {* show types that are presumably too general *}
    7.51 +
    7.52 +class plus =
    7.53 +  fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
    7.54 +
    7.55 +class minus =
    7.56 +  fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
    7.57 +
    7.58 +class uminus =
    7.59 +  fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
    7.60 +
    7.61 +class times =
    7.62 +  fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
    7.63 +
    7.64 +use "~~/src/Provers/Arith/abel_cancel.ML"
    7.65 +
    7.66  text {*
    7.67    The theory of partially ordered groups is taken from the books:
    7.68    \begin{itemize}
    7.69 @@ -1129,8 +1184,8 @@
    7.70  (* term order for abelian groups *)
    7.71  
    7.72  fun agrp_ord (Const (a, _)) = find_index (fn a' => a = a')
    7.73 -      [@{const_name Algebras.zero}, @{const_name Algebras.plus},
    7.74 -        @{const_name Algebras.uminus}, @{const_name Algebras.minus}]
    7.75 +      [@{const_name Groups.zero}, @{const_name Groups.plus},
    7.76 +        @{const_name Groups.uminus}, @{const_name Groups.minus}]
    7.77    | agrp_ord _ = ~1;
    7.78  
    7.79  fun termless_agrp (a, b) = (TermOrd.term_lpo agrp_ord (a, b) = LESS);
    7.80 @@ -1139,9 +1194,9 @@
    7.81    val ac1 = mk_meta_eq @{thm add_assoc};
    7.82    val ac2 = mk_meta_eq @{thm add_commute};
    7.83    val ac3 = mk_meta_eq @{thm add_left_commute};
    7.84 -  fun solve_add_ac thy _ (_ $ (Const (@{const_name Algebras.plus},_) $ _ $ _) $ _) =
    7.85 +  fun solve_add_ac thy _ (_ $ (Const (@{const_name Groups.plus},_) $ _ $ _) $ _) =
    7.86          SOME ac1
    7.87 -    | solve_add_ac thy _ (_ $ x $ (Const (@{const_name Algebras.plus},_) $ y $ z)) =
    7.88 +    | solve_add_ac thy _ (_ $ x $ (Const (@{const_name Groups.plus},_) $ y $ z)) =
    7.89          if termless_agrp (y, x) then SOME ac3 else NONE
    7.90      | solve_add_ac thy _ (_ $ x $ y) =
    7.91          if termless_agrp (y, x) then SOME ac2 else NONE
     8.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Fri Feb 19 14:47:00 2010 +0100
     8.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Fri Feb 19 14:47:01 2010 +0100
     8.3 @@ -182,9 +182,9 @@
     8.4    ">="         > HOL4Compat.nat_ge
     8.5    FUNPOW       > HOL4Compat.FUNPOW
     8.6    "<="         > Orderings.less_eq :: "[nat,nat]=>bool"
     8.7 -  "+"          > Algebras.plus :: "[nat,nat]=>nat"
     8.8 -  "*"          > Algebras.times :: "[nat,nat]=>nat"
     8.9 -  "-"          > Algebras.minus :: "[nat,nat]=>nat"
    8.10 +  "+"          > Groups.plus :: "[nat,nat]=>nat"
    8.11 +  "*"          > Groups.times :: "[nat,nat]=>nat"
    8.12 +  "-"          > Groups.minus :: "[nat,nat]=>nat"
    8.13    MIN          > Orderings.min :: "[nat,nat]=>nat"
    8.14    MAX          > Orderings.max :: "[nat,nat]=>nat"
    8.15    DIV          > Divides.div :: "[nat,nat]=>nat"
     9.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Fri Feb 19 14:47:00 2010 +0100
     9.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Fri Feb 19 14:47:01 2010 +0100
     9.3 @@ -16,12 +16,12 @@
     9.4    real > RealDef.real;
     9.5  
     9.6  const_maps
     9.7 -  real_0   > Algebras.zero      :: real
     9.8 -  real_1   > Algebras.one       :: real
     9.9 -  real_neg > Algebras.uminus    :: "real => real"
    9.10 -  inv      > Algebras.inverse   :: "real => real"
    9.11 -  real_add > Algebras.plus      :: "[real,real] => real"
    9.12 -  real_mul > Algebras.times     :: "[real,real] => real"
    9.13 +  real_0   > Groups.zero      :: real
    9.14 +  real_1   > Groups.one       :: real
    9.15 +  real_neg > Groups.uminus    :: "real => real"
    9.16 +  inv      > Groups.inverse   :: "real => real"
    9.17 +  real_add > Groups.plus      :: "[real,real] => real"
    9.18 +  real_mul > Groups.times     :: "[real,real] => real"
    9.19    real_lt  > Orderings.less      :: "[real,real] => bool";
    9.20  
    9.21  ignore_thms
    9.22 @@ -51,8 +51,8 @@
    9.23    real_gt     > HOL4Compat.real_gt
    9.24    real_ge     > HOL4Compat.real_ge
    9.25    real_lte    > Orderings.less_eq :: "[real,real] => bool"
    9.26 -  real_sub    > Algebras.minus :: "[real,real] => real"
    9.27 -  "/"         > Algebras.divide :: "[real,real] => real"
    9.28 +  real_sub    > Groups.minus :: "[real,real] => real"
    9.29 +  "/"         > Rings.divide :: "[real,real] => real"
    9.30    pow         > Power.power :: "[real,nat] => real"
    9.31    abs         > Groups.abs :: "real => real"
    9.32    real_of_num > RealDef.real :: "nat => real";
    10.1 --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Fri Feb 19 14:47:00 2010 +0100
    10.2 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Fri Feb 19 14:47:01 2010 +0100
    10.3 @@ -76,9 +76,9 @@
    10.4    SUC > Suc
    10.5    PRE > HOLLightCompat.Pred
    10.6    NUMERAL > HOL4Compat.NUMERAL
    10.7 -  "+" > Algebras.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
    10.8 -  "*" > Algebras.times :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    10.9 -  "-" > Algebras.minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   10.10 +  "+" > Groups.plus :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
   10.11 +  "*" > Groups.times :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   10.12 +  "-" > Groups.minus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   10.13    BIT0 > HOLLightCompat.NUMERAL_BIT0
   10.14    BIT1 > HOL4Compat.NUMERAL_BIT1
   10.15    INL > Sum_Type.Inl
    11.1 --- a/src/HOL/Import/HOL/arithmetic.imp	Fri Feb 19 14:47:00 2010 +0100
    11.2 +++ b/src/HOL/Import/HOL/arithmetic.imp	Fri Feb 19 14:47:01 2010 +0100
    11.3 @@ -24,9 +24,9 @@
    11.4    ">=" > "HOL4Compat.nat_ge"
    11.5    ">" > "HOL4Compat.nat_gt"
    11.6    "<=" > "Orderings.less_eq" :: "nat => nat => bool"
    11.7 -  "-" > "Algebras.minus_class.minus" :: "nat => nat => nat"
    11.8 -  "+" > "Algebras.plus_class.plus" :: "nat => nat => nat"
    11.9 -  "*" > "Algebras.times_class.times" :: "nat => nat => nat"
   11.10 +  "-" > "Groups.minus" :: "nat => nat => nat"
   11.11 +  "+" > "Groups.plus" :: "nat => nat => nat"
   11.12 +  "*" > "Groups.times" :: "nat => nat => nat"
   11.13  
   11.14  thm_maps
   11.15    "num_case_def" > "HOL4Compat.num_case_def"
    12.1 --- a/src/HOL/Import/HOL/real.imp	Fri Feb 19 14:47:00 2010 +0100
    12.2 +++ b/src/HOL/Import/HOL/real.imp	Fri Feb 19 14:47:01 2010 +0100
    12.3 @@ -10,7 +10,7 @@
    12.4  const_maps
    12.5    "sup" > "HOL4Real.real.sup"
    12.6    "sum" > "HOL4Real.real.sum"
    12.7 -  "real_sub" > "Algebras.minus" :: "real => real => real"
    12.8 +  "real_sub" > "Groups.minus" :: "real => real => real"
    12.9    "real_of_num" > "RealDef.real" :: "nat => real"
   12.10    "real_lte" > "Orderings.less_eq" :: "real => real => bool"
   12.11    "real_gt" > "HOL4Compat.real_gt"
    13.1 --- a/src/HOL/Import/HOL/realax.imp	Fri Feb 19 14:47:00 2010 +0100
    13.2 +++ b/src/HOL/Import/HOL/realax.imp	Fri Feb 19 14:47:01 2010 +0100
    13.3 @@ -27,12 +27,12 @@
    13.4    "treal_add" > "HOL4Real.realax.treal_add"
    13.5    "treal_1" > "HOL4Real.realax.treal_1"
    13.6    "treal_0" > "HOL4Real.realax.treal_0"
    13.7 -  "real_neg" > "Algebras.uminus_class.uminus" :: "real => real"
    13.8 -  "real_mul" > "Algebras.times_class.times" :: "real => real => real"
    13.9 +  "real_neg" > "Groups.uminus" :: "real => real"
   13.10 +  "real_mul" > "Groups.times" :: "real => real => real"
   13.11    "real_lt" > "Orderings.less" :: "real => real => bool"
   13.12 -  "real_add" > "Algebras.plus_class.plus" :: "real => real => real"
   13.13 -  "real_1" > "Algebras.one_class.one" :: "real"
   13.14 -  "real_0" > "Algebras.zero_class.zero" :: "real"
   13.15 +  "real_add" > "Groups.plus" :: "real => real => real"
   13.16 +  "real_1" > "Groups.one" :: "real"
   13.17 +  "real_0" > "Groups.zero" :: "real"
   13.18    "inv" > "Ring.inverse" :: "real => real"
   13.19    "hreal_of_treal" > "HOL4Real.realax.hreal_of_treal"
   13.20  
    14.1 --- a/src/HOL/Import/HOLLight/hollight.imp	Fri Feb 19 14:47:00 2010 +0100
    14.2 +++ b/src/HOL/Import/HOLLight/hollight.imp	Fri Feb 19 14:47:01 2010 +0100
    14.3 @@ -238,10 +238,10 @@
    14.4    "<=" > "HOLLight.hollight.<="
    14.5    "<" > "HOLLight.hollight.<"
    14.6    "/\\" > "op &"
    14.7 -  "-" > "Algebras.minus_class.minus" :: "nat => nat => nat"
    14.8 +  "-" > "Groups.minus" :: "nat => nat => nat"
    14.9    "," > "Pair"
   14.10 -  "+" > "Algebras.plus_class.plus" :: "nat => nat => nat"
   14.11 -  "*" > "Algebras.times_class.times" :: "nat => nat => nat"
   14.12 +  "+" > "Groups.plus" :: "nat => nat => nat"
   14.13 +  "*" > "Groups.times" :: "nat => nat => nat"
   14.14    "$" > "HOLLight.hollight.$"
   14.15    "!" > "All"
   14.16  
    15.1 --- a/src/HOL/Library/SetsAndFunctions.thy	Fri Feb 19 14:47:00 2010 +0100
    15.2 +++ b/src/HOL/Library/SetsAndFunctions.thy	Fri Feb 19 14:47:01 2010 +0100
    15.3 @@ -119,14 +119,14 @@
    15.4    apply (force simp add: mult_assoc)
    15.5    done
    15.6  
    15.7 -interpretation set_comm_monoid_add: comm_monoid_add "{0}" "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set"
    15.8 +interpretation set_comm_monoid_add: comm_monoid_add "op \<oplus> :: ('a::comm_monoid_add) set => 'a set => 'a set" "{0}"
    15.9    apply default
   15.10     apply (unfold set_plus_def)
   15.11     apply (force simp add: add_ac)
   15.12    apply force
   15.13    done
   15.14  
   15.15 -interpretation set_comm_monoid_mult: comm_monoid_mult "{1}" "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set"
   15.16 +interpretation set_comm_monoid_mult: comm_monoid_mult "op \<otimes> :: ('a::comm_monoid_mult) set => 'a set => 'a set" "{1}"
   15.17    apply default
   15.18     apply (unfold set_times_def)
   15.19     apply (force simp add: mult_ac)
    16.1 --- a/src/HOL/List.thy	Fri Feb 19 14:47:00 2010 +0100
    16.2 +++ b/src/HOL/List.thy	Fri Feb 19 14:47:01 2010 +0100
    16.3 @@ -2352,7 +2352,7 @@
    16.4  proof (induct xss arbitrary: xs)
    16.5    case Nil show ?case by simp
    16.6  next
    16.7 -  interpret monoid_add "[]" "op @" proof qed simp_all
    16.8 +  interpret monoid_add "op @" "[]" proof qed simp_all
    16.9    case Cons then show ?case by (simp add: foldl_absorb0)
   16.10  qed
   16.11  
    17.1 --- a/src/HOL/Mutabelle/Mutabelle.thy	Fri Feb 19 14:47:00 2010 +0100
    17.2 +++ b/src/HOL/Mutabelle/Mutabelle.thy	Fri Feb 19 14:47:01 2010 +0100
    17.3 @@ -14,7 +14,7 @@
    17.4    (@{const_name HOL.undefined}, "'a"),
    17.5    (@{const_name HOL.default}, "'a"),
    17.6    (@{const_name dummy_pattern}, "'a::{}"),
    17.7 -  (@{const_name Algebras.uminus}, "'a"),
    17.8 +  (@{const_name Groups.uminus}, "'a"),
    17.9    (@{const_name Nat.size}, "'a"),
   17.10    (@{const_name Groups.abs}, "'a")];
   17.11  
    18.1 --- a/src/HOL/NSA/NSA.thy	Fri Feb 19 14:47:00 2010 +0100
    18.2 +++ b/src/HOL/NSA/NSA.thy	Fri Feb 19 14:47:01 2010 +0100
    18.3 @@ -671,12 +671,12 @@
    18.4    0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
    18.5  fun reorient_proc sg _ (_ $ t $ u) =
    18.6    case u of
    18.7 -      Const(@{const_name Algebras.zero}, _) => NONE
    18.8 -    | Const(@{const_name Algebras.one}, _) => NONE
    18.9 +      Const(@{const_name Groups.zero}, _) => NONE
   18.10 +    | Const(@{const_name Groups.one}, _) => NONE
   18.11      | Const(@{const_name Int.number_of}, _) $ _ => NONE
   18.12      | _ => SOME (case t of
   18.13 -                Const(@{const_name Algebras.zero}, _) => meta_zero_approx_reorient
   18.14 -              | Const(@{const_name Algebras.one}, _) => meta_one_approx_reorient
   18.15 +                Const(@{const_name Groups.zero}, _) => meta_zero_approx_reorient
   18.16 +              | Const(@{const_name Groups.one}, _) => meta_one_approx_reorient
   18.17                | Const(@{const_name Int.number_of}, _) $ _ =>
   18.18                                   meta_number_of_approx_reorient);
   18.19  
    19.1 --- a/src/HOL/Tools/Function/size.ML	Fri Feb 19 14:47:00 2010 +0100
    19.2 +++ b/src/HOL/Tools/Function/size.ML	Fri Feb 19 14:47:01 2010 +0100
    19.3 @@ -25,7 +25,7 @@
    19.4  
    19.5  val lookup_size = SizeData.get #> Symtab.lookup;
    19.6  
    19.7 -fun plus (t1, t2) = Const (@{const_name Algebras.plus},
    19.8 +fun plus (t1, t2) = Const (@{const_name Groups.plus},
    19.9    HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
   19.10  
   19.11  fun size_of_type f g h (T as Type (s, Ts)) =
    20.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Feb 19 14:47:00 2010 +0100
    20.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Feb 19 14:47:01 2010 +0100
    20.3 @@ -2436,8 +2436,8 @@
    20.4        val [polarity, depth] = additional_arguments
    20.5        val polarity' = (case prem of Prem _ => I | Negprem _ => HOLogic.mk_not | _ => I) polarity
    20.6        val depth' =
    20.7 -        Const ("Algebras.minus", @{typ "code_numeral => code_numeral => code_numeral"})
    20.8 -          $ depth $ Const ("Algebras.one", @{typ "Code_Numeral.code_numeral"})
    20.9 +        Const (@{const_name Groups.minus}, @{typ "code_numeral => code_numeral => code_numeral"})
   20.10 +          $ depth $ Const (@{const_name Groups.one}, @{typ "Code_Numeral.code_numeral"})
   20.11      in [polarity', depth'] end
   20.12    }
   20.13  
    21.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Fri Feb 19 14:47:00 2010 +0100
    21.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Fri Feb 19 14:47:01 2010 +0100
    21.3 @@ -224,8 +224,8 @@
    21.4    @{const_name Suc}, @{const_name Nat.zero_nat_inst.zero_nat},
    21.5    @{const_name Nat.one_nat_inst.one_nat},
    21.6    @{const_name Orderings.less}, @{const_name Orderings.less_eq},
    21.7 -  @{const_name Algebras.zero},
    21.8 -  @{const_name Algebras.one},  @{const_name Algebras.plus},
    21.9 +  @{const_name Groups.zero},
   21.10 +  @{const_name Groups.one},  @{const_name Groups.plus},
   21.11    @{const_name Nat.ord_nat_inst.less_eq_nat},
   21.12    @{const_name Nat.ord_nat_inst.less_nat},
   21.13    @{const_name number_nat_inst.number_of_nat},
    22.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Fri Feb 19 14:47:00 2010 +0100
    22.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Fri Feb 19 14:47:01 2010 +0100
    22.3 @@ -79,9 +79,9 @@
    22.4  | Const (@{const_name Orderings.less_eq}, _) $ y $ z =>
    22.5     if term_of x aconv y then Le (Thm.dest_arg ct)
    22.6     else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
    22.7 -| Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$y$_) =>
    22.8 +| Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$y$_) =>
    22.9     if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox
   22.10 -| Const (@{const_name Not},_) $ (Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$y$_)) =>
   22.11 +| Const (@{const_name Not},_) $ (Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$y$_)) =>
   22.12     if term_of x aconv y then
   22.13     NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox
   22.14  | _ => Nox)
   22.15 @@ -175,18 +175,18 @@
   22.16    (fn _ => EVERY [simp_tac lin_ss 1, TRY (Lin_Arith.tac ctxt 1)]);
   22.17  fun linear_cmul 0 tm = zero
   22.18    | linear_cmul n tm = case tm of
   22.19 -      Const (@{const_name Algebras.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b
   22.20 -    | Const (@{const_name Algebras.times}, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x
   22.21 -    | Const (@{const_name Algebras.minus}, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b
   22.22 -    | (m as Const (@{const_name Algebras.uminus}, _)) $ a => m $ linear_cmul n a
   22.23 +      Const (@{const_name Groups.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b
   22.24 +    | Const (@{const_name Groups.times}, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x
   22.25 +    | Const (@{const_name Groups.minus}, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b
   22.26 +    | (m as Const (@{const_name Groups.uminus}, _)) $ a => m $ linear_cmul n a
   22.27      | _ => numeral1 (fn m => n * m) tm;
   22.28  fun earlier [] x y = false
   22.29    | earlier (h::t) x y =
   22.30      if h aconv y then false else if h aconv x then true else earlier t x y;
   22.31  
   22.32  fun linear_add vars tm1 tm2 = case (tm1, tm2) of
   22.33 -    (Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c1 $ x1) $ r1,
   22.34 -    Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c2 $ x2) $ r2) =>
   22.35 +    (Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c1 $ x1) $ r1,
   22.36 +    Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c2 $ x2) $ r2) =>
   22.37     if x1 = x2 then
   22.38       let val c = numeral2 Integer.add c1 c2
   22.39        in if c = zero then linear_add vars r1 r2
   22.40 @@ -194,9 +194,9 @@
   22.41       end
   22.42       else if earlier vars x1 x2 then addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2
   22.43     else addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2
   22.44 - | (Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c1 $ x1) $ r1, _) =>
   22.45 + | (Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c1 $ x1) $ r1, _) =>
   22.46        addC $ (mulC $ c1 $ x1) $ linear_add vars r1 tm2
   22.47 - | (_, Const (@{const_name Algebras.plus}, _) $ (Const (@{const_name Algebras.times}, _) $ c2 $ x2) $ r2) =>
   22.48 + | (_, Const (@{const_name Groups.plus}, _) $ (Const (@{const_name Groups.times}, _) $ c2 $ x2) $ r2) =>
   22.49        addC $ (mulC $ c2 $ x2) $ linear_add vars tm1 r2
   22.50   | (_, _) => numeral2 Integer.add tm1 tm2;
   22.51  
   22.52 @@ -205,10 +205,10 @@
   22.53  
   22.54  
   22.55  fun lint vars tm =  if is_numeral tm then tm  else case tm of
   22.56 -  Const (@{const_name Algebras.uminus}, _) $ t => linear_neg (lint vars t)
   22.57 -| Const (@{const_name Algebras.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t)
   22.58 -| Const (@{const_name Algebras.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t)
   22.59 -| Const (@{const_name Algebras.times}, _) $ s $ t =>
   22.60 +  Const (@{const_name Groups.uminus}, _) $ t => linear_neg (lint vars t)
   22.61 +| Const (@{const_name Groups.plus}, _) $ s $ t => linear_add vars (lint vars s) (lint vars t)
   22.62 +| Const (@{const_name Groups.minus}, _) $ s $ t => linear_sub vars (lint vars s) (lint vars t)
   22.63 +| Const (@{const_name Groups.times}, _) $ s $ t =>
   22.64    let val s' = lint vars s
   22.65        val t' = lint vars t
   22.66    in if is_numeral s' then (linear_cmul (dest_numeral s') t')
   22.67 @@ -270,7 +270,7 @@
   22.68        val d'' = Thm.rhs_of dth |> Thm.dest_arg1
   22.69       in
   22.70        case tt' of
   22.71 -        Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$_)$_ =>
   22.72 +        Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$_)$_ =>
   22.73          let val x = dest_numeral c
   22.74          in if x < 0 then Conv.fconv_rule (arg_conv (arg_conv (lint_conv ctxt vs)))
   22.75                                         (Thm.transitive dth (inst' [d'',t'] dvd_uminus'))
   22.76 @@ -293,15 +293,15 @@
   22.77    val ins = insert (op = : int * int -> bool)
   22.78    fun h (acc,dacc) t =
   22.79     case (term_of t) of
   22.80 -    Const(s,_)$(Const(@{const_name Algebras.times},_)$c$y)$ _ =>
   22.81 +    Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
   22.82      if x aconv y andalso member (op =)
   22.83        ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   22.84      then (ins (dest_numeral c) acc,dacc) else (acc,dacc)
   22.85 -  | Const(s,_)$_$(Const(@{const_name Algebras.times},_)$c$y) =>
   22.86 +  | Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
   22.87      if x aconv y andalso member (op =)
   22.88         [@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   22.89      then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
   22.90 -  | Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_) =>
   22.91 +  | Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_) =>
   22.92      if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)
   22.93    | Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   22.94    | Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   22.95 @@ -335,15 +335,15 @@
   22.96     Const("op &",_)$_$_ => binop_conv unit_conv t
   22.97    | Const("op |",_)$_$_ => binop_conv unit_conv t
   22.98    | Const (@{const_name Not},_)$_ => arg_conv unit_conv t
   22.99 -  | Const(s,_)$(Const(@{const_name Algebras.times},_)$c$y)$ _ =>
  22.100 +  | Const(s,_)$(Const(@{const_name Groups.times},_)$c$y)$ _ =>
  22.101      if x=y andalso member (op =)
  22.102        ["op =", @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
  22.103      then cv (l div dest_numeral c) t else Thm.reflexive t
  22.104 -  | Const(s,_)$_$(Const(@{const_name Algebras.times},_)$c$y) =>
  22.105 +  | Const(s,_)$_$(Const(@{const_name Groups.times},_)$c$y) =>
  22.106      if x=y andalso member (op =)
  22.107        [@{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
  22.108      then cv (l div dest_numeral c) t else Thm.reflexive t
  22.109 -  | Const(@{const_name Rings.dvd},_)$d$(r as (Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_)) =>
  22.110 +  | Const(@{const_name Rings.dvd},_)$d$(r as (Const(@{const_name Groups.plus},_)$(Const(@{const_name Groups.times},_)$c$y)$_)) =>
  22.111      if x=y then
  22.112        let
  22.113         val k = l div dest_numeral c
  22.114 @@ -546,10 +546,10 @@
  22.115    | @{term "0::int"} => C 0
  22.116    | @{term "1::int"} => C 1
  22.117    | Term.Bound i => Bound i
  22.118 -  | Const(@{const_name Algebras.uminus},_)$t' => Neg (i_of_term vs t')
  22.119 -  | Const(@{const_name Algebras.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
  22.120 -  | Const(@{const_name Algebras.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
  22.121 -  | Const(@{const_name Algebras.times},_)$t1$t2 =>
  22.122 +  | Const(@{const_name Groups.uminus},_)$t' => Neg (i_of_term vs t')
  22.123 +  | Const(@{const_name Groups.plus},_)$t1$t2 => Add (i_of_term vs t1,i_of_term vs t2)
  22.124 +  | Const(@{const_name Groups.minus},_)$t1$t2 => Sub (i_of_term vs t1,i_of_term vs t2)
  22.125 +  | Const(@{const_name Groups.times},_)$t1$t2 =>
  22.126       (Mul (HOLogic.dest_number t1 |> snd, i_of_term vs t2)
  22.127      handle TERM _ =>
  22.128         (Mul (HOLogic.dest_number t2 |> snd, i_of_term vs t1)
    23.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Fri Feb 19 14:47:00 2010 +0100
    23.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Fri Feb 19 14:47:01 2010 +0100
    23.3 @@ -52,15 +52,15 @@
    23.4  
    23.5  local
    23.6   fun isnum t = case t of 
    23.7 -   Const(@{const_name Algebras.zero},_) => true
    23.8 - | Const(@{const_name Algebras.one},_) => true
    23.9 +   Const(@{const_name Groups.zero},_) => true
   23.10 + | Const(@{const_name Groups.one},_) => true
   23.11   | @{term "Suc"}$s => isnum s
   23.12   | @{term "nat"}$s => isnum s
   23.13   | @{term "int"}$s => isnum s
   23.14 - | Const(@{const_name Algebras.uminus},_)$s => isnum s
   23.15 - | Const(@{const_name Algebras.plus},_)$l$r => isnum l andalso isnum r
   23.16 - | Const(@{const_name Algebras.times},_)$l$r => isnum l andalso isnum r
   23.17 - | Const(@{const_name Algebras.minus},_)$l$r => isnum l andalso isnum r
   23.18 + | Const(@{const_name Groups.uminus},_)$s => isnum s
   23.19 + | Const(@{const_name Groups.plus},_)$l$r => isnum l andalso isnum r
   23.20 + | Const(@{const_name Groups.times},_)$l$r => isnum l andalso isnum r
   23.21 + | Const(@{const_name Groups.minus},_)$l$r => isnum l andalso isnum r
   23.22   | Const(@{const_name Power.power},_)$l$r => isnum l andalso isnum r
   23.23   | Const(@{const_name Divides.mod},_)$l$r => isnum l andalso isnum r
   23.24   | Const(@{const_name Divides.div},_)$l$r => isnum l andalso isnum r
    24.1 --- a/src/HOL/Tools/arith_data.ML	Fri Feb 19 14:47:00 2010 +0100
    24.2 +++ b/src/HOL/Tools/arith_data.ML	Fri Feb 19 14:47:01 2010 +0100
    24.3 @@ -75,11 +75,11 @@
    24.4  
    24.5  fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n;
    24.6  
    24.7 -val mk_plus = HOLogic.mk_binop @{const_name Algebras.plus};
    24.8 +val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
    24.9  
   24.10  fun mk_minus t = 
   24.11    let val T = Term.fastype_of t
   24.12 -  in Const (@{const_name Algebras.uminus}, T --> T) $ t end;
   24.13 +  in Const (@{const_name Groups.uminus}, T --> T) $ t end;
   24.14  
   24.15  (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
   24.16  fun mk_sum T []        = mk_number T 0
   24.17 @@ -91,9 +91,9 @@
   24.18    | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
   24.19  
   24.20  (*decompose additions AND subtractions as a sum*)
   24.21 -fun dest_summing (pos, Const (@{const_name Algebras.plus}, _) $ t $ u, ts) =
   24.22 +fun dest_summing (pos, Const (@{const_name Groups.plus}, _) $ t $ u, ts) =
   24.23          dest_summing (pos, t, dest_summing (pos, u, ts))
   24.24 -  | dest_summing (pos, Const (@{const_name Algebras.minus}, _) $ t $ u, ts) =
   24.25 +  | dest_summing (pos, Const (@{const_name Groups.minus}, _) $ t $ u, ts) =
   24.26          dest_summing (pos, t, dest_summing (not pos, u, ts))
   24.27    | dest_summing (pos, t, ts) =
   24.28          if pos then t::ts else mk_minus t :: ts;
    25.1 --- a/src/HOL/Tools/hologic.ML	Fri Feb 19 14:47:00 2010 +0100
    25.2 +++ b/src/HOL/Tools/hologic.ML	Fri Feb 19 14:47:01 2010 +0100
    25.3 @@ -440,9 +440,9 @@
    25.4  
    25.5  val natT = Type ("nat", []);
    25.6  
    25.7 -val zero = Const ("Algebras.zero_class.zero", natT);
    25.8 +val zero = Const ("Groups.zero_class.zero", natT);
    25.9  
   25.10 -fun is_zero (Const ("Algebras.zero_class.zero", _)) = true
   25.11 +fun is_zero (Const ("Groups.zero_class.zero", _)) = true
   25.12    | is_zero _ = false;
   25.13  
   25.14  fun mk_Suc t = Const ("Suc", natT --> natT) $ t;
   25.15 @@ -458,7 +458,7 @@
   25.16        | mk n = mk_Suc (mk (n - 1));
   25.17    in if n < 0 then raise TERM ("mk_nat: negative number", []) else mk n end;
   25.18  
   25.19 -fun dest_nat (Const ("Algebras.zero_class.zero", _)) = 0
   25.20 +fun dest_nat (Const ("Groups.zero_class.zero", _)) = 0
   25.21    | dest_nat (Const ("Suc", _) $ t) = dest_nat t + 1
   25.22    | dest_nat t = raise TERM ("dest_nat", [t]);
   25.23  
   25.24 @@ -508,12 +508,12 @@
   25.25    | add_numerals (Abs (_, _, t)) = add_numerals t
   25.26    | add_numerals _ = I;
   25.27  
   25.28 -fun mk_number T 0 = Const ("Algebras.zero_class.zero", T)
   25.29 -  | mk_number T 1 = Const ("Algebras.one_class.one", T)
   25.30 +fun mk_number T 0 = Const ("Groups.zero_class.zero", T)
   25.31 +  | mk_number T 1 = Const ("Groups.one_class.one", T)
   25.32    | mk_number T i = number_of_const T $ mk_numeral i;
   25.33  
   25.34 -fun dest_number (Const ("Algebras.zero_class.zero", T)) = (T, 0)
   25.35 -  | dest_number (Const ("Algebras.one_class.one", T)) = (T, 1)
   25.36 +fun dest_number (Const ("Groups.zero_class.zero", T)) = (T, 0)
   25.37 +  | dest_number (Const ("Groups.one_class.one", T)) = (T, 1)
   25.38    | dest_number (Const ("Int.number_class.number_of", Type ("fun", [_, T])) $ t) =
   25.39        (T, dest_numeral t)
   25.40    | dest_number t = raise TERM ("dest_number", [t]);
    26.1 --- a/src/HOL/Tools/int_arith.ML	Fri Feb 19 14:47:00 2010 +0100
    26.2 +++ b/src/HOL/Tools/int_arith.ML	Fri Feb 19 14:47:01 2010 +0100
    26.3 @@ -49,12 +49,12 @@
    26.4    make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
    26.5    proc = proc1, identifier = []};
    26.6  
    26.7 -fun check (Const (@{const_name Algebras.one}, @{typ int})) = false
    26.8 -  | check (Const (@{const_name Algebras.one}, _)) = true
    26.9 +fun check (Const (@{const_name Groups.one}, @{typ int})) = false
   26.10 +  | check (Const (@{const_name Groups.one}, _)) = true
   26.11    | check (Const (s, _)) = member (op =) [@{const_name "op ="},
   26.12 -      @{const_name Algebras.times}, @{const_name Algebras.uminus},
   26.13 -      @{const_name Algebras.minus}, @{const_name Algebras.plus},
   26.14 -      @{const_name Algebras.zero},
   26.15 +      @{const_name Groups.times}, @{const_name Groups.uminus},
   26.16 +      @{const_name Groups.minus}, @{const_name Groups.plus},
   26.17 +      @{const_name Groups.zero},
   26.18        @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   26.19    | check (a $ b) = check a andalso check b
   26.20    | check _ = false;
    27.1 --- a/src/HOL/Tools/lin_arith.ML	Fri Feb 19 14:47:00 2010 +0100
    27.2 +++ b/src/HOL/Tools/lin_arith.ML	Fri Feb 19 14:47:01 2010 +0100
    27.3 @@ -138,8 +138,8 @@
    27.4  *)
    27.5  fun demult (inj_consts : (string * typ) list) : term * Rat.rat -> term option * Rat.rat =
    27.6  let
    27.7 -  fun demult ((mC as Const (@{const_name Algebras.times}, _)) $ s $ t, m) =
    27.8 -      (case s of Const (@{const_name Algebras.times}, _) $ s1 $ s2 =>
    27.9 +  fun demult ((mC as Const (@{const_name Groups.times}, _)) $ s $ t, m) =
   27.10 +      (case s of Const (@{const_name Groups.times}, _) $ s1 $ s2 =>
   27.11          (* bracketing to the right: '(s1 * s2) * t' becomes 's1 * (s2 * t)' *)
   27.12          demult (mC $ s1 $ (mC $ s2 $ t), m)
   27.13        | _ =>
   27.14 @@ -170,9 +170,9 @@
   27.15          (SOME _, _) => (SOME (mC $ s $ t), m)
   27.16        | (NONE,  m') => apsnd (Rat.mult (Rat.inv m')) (demult (s, m)))
   27.17      (* terms that evaluate to numeric constants *)
   27.18 -    | demult (Const (@{const_name Algebras.uminus}, _) $ t, m) = demult (t, Rat.neg m)
   27.19 -    | demult (Const (@{const_name Algebras.zero}, _), m) = (NONE, Rat.zero)
   27.20 -    | demult (Const (@{const_name Algebras.one}, _), m) = (NONE, m)
   27.21 +    | demult (Const (@{const_name Groups.uminus}, _) $ t, m) = demult (t, Rat.neg m)
   27.22 +    | demult (Const (@{const_name Groups.zero}, _), m) = (NONE, Rat.zero)
   27.23 +    | demult (Const (@{const_name Groups.one}, _), m) = (NONE, m)
   27.24      (*Warning: in rare cases number_of encloses a non-numeral,
   27.25        in which case dest_numeral raises TERM; hence all the handles below.
   27.26        Same for Suc-terms that turn out not to be numerals -
   27.27 @@ -196,19 +196,19 @@
   27.28    (* Turns a term 'all' and associated multiplicity 'm' into a list 'p' of
   27.29       summands and associated multiplicities, plus a constant 'i' (with implicit
   27.30       multiplicity 1) *)
   27.31 -  fun poly (Const (@{const_name Algebras.plus}, _) $ s $ t,
   27.32 +  fun poly (Const (@{const_name Groups.plus}, _) $ s $ t,
   27.33          m : Rat.rat, pi : (term * Rat.rat) list * Rat.rat) = poly (s, m, poly (t, m, pi))
   27.34 -    | poly (all as Const (@{const_name Algebras.minus}, T) $ s $ t, m, pi) =
   27.35 +    | poly (all as Const (@{const_name Groups.minus}, T) $ s $ t, m, pi) =
   27.36          if nT T then add_atom all m pi else poly (s, m, poly (t, Rat.neg m, pi))
   27.37 -    | poly (all as Const (@{const_name Algebras.uminus}, T) $ t, m, pi) =
   27.38 +    | poly (all as Const (@{const_name Groups.uminus}, T) $ t, m, pi) =
   27.39          if nT T then add_atom all m pi else poly (t, Rat.neg m, pi)
   27.40 -    | poly (Const (@{const_name Algebras.zero}, _), _, pi) =
   27.41 +    | poly (Const (@{const_name Groups.zero}, _), _, pi) =
   27.42          pi
   27.43 -    | poly (Const (@{const_name Algebras.one}, _), m, (p, i)) =
   27.44 +    | poly (Const (@{const_name Groups.one}, _), m, (p, i)) =
   27.45          (p, Rat.add i m)
   27.46      | poly (Const (@{const_name Suc}, _) $ t, m, (p, i)) =
   27.47          poly (t, m, (p, Rat.add i m))
   27.48 -    | poly (all as Const (@{const_name Algebras.times}, _) $ _ $ _, m, pi as (p, i)) =
   27.49 +    | poly (all as Const (@{const_name Groups.times}, _) $ _ $ _, m, pi as (p, i)) =
   27.50          (case demult inj_consts (all, m) of
   27.51             (NONE,   m') => (p, Rat.add i m')
   27.52           | (SOME u, m') => add_atom u m' pi)
   27.53 @@ -293,7 +293,7 @@
   27.54        Const (a, _) => member (op =) [@{const_name Orderings.max},
   27.55                                      @{const_name Orderings.min},
   27.56                                      @{const_name Groups.abs},
   27.57 -                                    @{const_name Algebras.minus},
   27.58 +                                    @{const_name Groups.minus},
   27.59                                      "Int.nat" (*DYNAMIC BINDING!*),
   27.60                                      "Divides.div_class.mod" (*DYNAMIC BINDING!*),
   27.61                                      "Divides.div_class.div" (*DYNAMIC BINDING!*)] a
   27.62 @@ -401,9 +401,9 @@
   27.63        let
   27.64          val rev_terms   = rev terms
   27.65          val terms1      = map (subst_term [(split_term, t1)]) rev_terms
   27.66 -        val terms2      = map (subst_term [(split_term, Const (@{const_name Algebras.uminus},
   27.67 +        val terms2      = map (subst_term [(split_term, Const (@{const_name Groups.uminus},
   27.68                              split_type --> split_type) $ t1)]) rev_terms
   27.69 -        val zero        = Const (@{const_name Algebras.zero}, split_type)
   27.70 +        val zero        = Const (@{const_name Groups.zero}, split_type)
   27.71          val zero_leq_t1 = Const (@{const_name Orderings.less_eq},
   27.72                              split_type --> split_type --> HOLogic.boolT) $ zero $ t1
   27.73          val t1_lt_zero  = Const (@{const_name Orderings.less},
   27.74 @@ -415,12 +415,12 @@
   27.75          SOME [(Ts, subgoal1), (Ts, subgoal2)]
   27.76        end
   27.77      (* ?P (?a - ?b) = ((?a < ?b --> ?P 0) & (ALL d. ?a = ?b + d --> ?P d)) *)
   27.78 -    | (Const (@{const_name Algebras.minus}, _), [t1, t2]) =>
   27.79 +    | (Const (@{const_name Groups.minus}, _), [t1, t2]) =>
   27.80        let
   27.81          (* "d" in the above theorem becomes a new bound variable after NNF   *)
   27.82          (* transformation, therefore some adjustment of indices is necessary *)
   27.83          val rev_terms       = rev terms
   27.84 -        val zero            = Const (@{const_name Algebras.zero}, split_type)
   27.85 +        val zero            = Const (@{const_name Groups.zero}, split_type)
   27.86          val d               = Bound 0
   27.87          val terms1          = map (subst_term [(split_term, zero)]) rev_terms
   27.88          val terms2          = map (subst_term [(incr_boundvars 1 split_term, d)])
   27.89 @@ -430,7 +430,7 @@
   27.90          val t1_lt_t2        = Const (@{const_name Orderings.less},
   27.91                                  split_type --> split_type --> HOLogic.boolT) $ t1 $ t2
   27.92          val t1_eq_t2_plus_d = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
   27.93 -                                (Const (@{const_name Algebras.plus},
   27.94 +                                (Const (@{const_name Groups.plus},
   27.95                                    split_type --> split_type --> split_type) $ t2' $ d)
   27.96          val not_false       = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
   27.97          val subgoal1        = (HOLogic.mk_Trueprop t1_lt_t2) :: terms1 @ [not_false]
   27.98 @@ -442,8 +442,8 @@
   27.99      | (Const ("Int.nat", _), [t1]) =>
  27.100        let
  27.101          val rev_terms   = rev terms
  27.102 -        val zero_int    = Const (@{const_name Algebras.zero}, HOLogic.intT)
  27.103 -        val zero_nat    = Const (@{const_name Algebras.zero}, HOLogic.natT)
  27.104 +        val zero_int    = Const (@{const_name Groups.zero}, HOLogic.intT)
  27.105 +        val zero_nat    = Const (@{const_name Groups.zero}, HOLogic.natT)
  27.106          val n           = Bound 0
  27.107          val terms1      = map (subst_term [(incr_boundvars 1 split_term, n)])
  27.108                              (map (incr_boundvars 1) rev_terms)
  27.109 @@ -465,7 +465,7 @@
  27.110      | (Const ("Divides.div_class.mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
  27.111        let
  27.112          val rev_terms               = rev terms
  27.113 -        val zero                    = Const (@{const_name Algebras.zero}, split_type)
  27.114 +        val zero                    = Const (@{const_name Groups.zero}, split_type)
  27.115          val i                       = Bound 1
  27.116          val j                       = Bound 0
  27.117          val terms1                  = map (subst_term [(split_term, t1)]) rev_terms
  27.118 @@ -480,8 +480,8 @@
  27.119          val j_lt_t2                 = Const (@{const_name Orderings.less},
  27.120                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
  27.121          val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
  27.122 -                                       (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
  27.123 -                                         (Const (@{const_name Algebras.times},
  27.124 +                                       (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
  27.125 +                                         (Const (@{const_name Groups.times},
  27.126                                             split_type --> split_type --> split_type) $ t2' $ i) $ j)
  27.127          val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
  27.128          val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
  27.129 @@ -497,7 +497,7 @@
  27.130      | (Const ("Divides.div_class.div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
  27.131        let
  27.132          val rev_terms               = rev terms
  27.133 -        val zero                    = Const (@{const_name Algebras.zero}, split_type)
  27.134 +        val zero                    = Const (@{const_name Groups.zero}, split_type)
  27.135          val i                       = Bound 1
  27.136          val j                       = Bound 0
  27.137          val terms1                  = map (subst_term [(split_term, zero)]) rev_terms
  27.138 @@ -512,8 +512,8 @@
  27.139          val j_lt_t2                 = Const (@{const_name Orderings.less},
  27.140                                          split_type --> split_type--> HOLogic.boolT) $ j $ t2'
  27.141          val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
  27.142 -                                       (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
  27.143 -                                         (Const (@{const_name Algebras.times},
  27.144 +                                       (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
  27.145 +                                         (Const (@{const_name Groups.times},
  27.146                                             split_type --> split_type --> split_type) $ t2' $ i) $ j)
  27.147          val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
  27.148          val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
  27.149 @@ -535,7 +535,7 @@
  27.150          Type ("fun", [Type ("Int.int", []), _])), [t1, t2]) =>
  27.151        let
  27.152          val rev_terms               = rev terms
  27.153 -        val zero                    = Const (@{const_name Algebras.zero}, split_type)
  27.154 +        val zero                    = Const (@{const_name Groups.zero}, split_type)
  27.155          val i                       = Bound 1
  27.156          val j                       = Bound 0
  27.157          val terms1                  = map (subst_term [(split_term, t1)]) rev_terms
  27.158 @@ -558,8 +558,8 @@
  27.159          val t2_lt_j                 = Const (@{const_name Orderings.less},
  27.160                                          split_type --> split_type--> HOLogic.boolT) $ t2' $ j
  27.161          val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
  27.162 -                                       (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
  27.163 -                                         (Const (@{const_name Algebras.times},
  27.164 +                                       (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
  27.165 +                                         (Const (@{const_name Groups.times},
  27.166                                             split_type --> split_type --> split_type) $ t2' $ i) $ j)
  27.167          val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
  27.168          val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
  27.169 @@ -589,7 +589,7 @@
  27.170          Type ("fun", [Type ("Int.int", []), _])), [t1, t2]) =>
  27.171        let
  27.172          val rev_terms               = rev terms
  27.173 -        val zero                    = Const (@{const_name Algebras.zero}, split_type)
  27.174 +        val zero                    = Const (@{const_name Groups.zero}, split_type)
  27.175          val i                       = Bound 1
  27.176          val j                       = Bound 0
  27.177          val terms1                  = map (subst_term [(split_term, zero)]) rev_terms
  27.178 @@ -612,8 +612,8 @@
  27.179          val t2_lt_j                 = Const (@{const_name Orderings.less},
  27.180                                          split_type --> split_type--> HOLogic.boolT) $ t2' $ j
  27.181          val t1_eq_t2_times_i_plus_j = Const ("op =", split_type --> split_type --> HOLogic.boolT) $ t1' $
  27.182 -                                       (Const (@{const_name Algebras.plus}, split_type --> split_type --> split_type) $
  27.183 -                                         (Const (@{const_name Algebras.times},
  27.184 +                                       (Const (@{const_name Groups.plus}, split_type --> split_type --> split_type) $
  27.185 +                                         (Const (@{const_name Groups.times},
  27.186                                             split_type --> split_type --> split_type) $ t2' $ i) $ j)
  27.187          val not_false               = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)
  27.188          val subgoal1                = (HOLogic.mk_Trueprop t2_eq_zero) :: terms1 @ [not_false]
    28.1 --- a/src/HOL/Tools/nat_arith.ML	Fri Feb 19 14:47:00 2010 +0100
    28.2 +++ b/src/HOL/Tools/nat_arith.ML	Fri Feb 19 14:47:01 2010 +0100
    28.3 @@ -19,8 +19,8 @@
    28.4  
    28.5  (** abstract syntax of structure nat: 0, Suc, + **)
    28.6  
    28.7 -val mk_plus = HOLogic.mk_binop @{const_name Algebras.plus};
    28.8 -val dest_plus = HOLogic.dest_bin @{const_name Algebras.plus} HOLogic.natT;
    28.9 +val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
   28.10 +val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
   28.11  
   28.12  fun mk_sum [] = HOLogic.zero
   28.13    | mk_sum [t] = t
   28.14 @@ -85,8 +85,8 @@
   28.15  structure DiffCancelSums = CancelSumsFun
   28.16  (struct
   28.17    open CommonCancelSums;
   28.18 -  val mk_bal = HOLogic.mk_binop @{const_name Algebras.minus};
   28.19 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.minus} HOLogic.natT;
   28.20 +  val mk_bal = HOLogic.mk_binop @{const_name Groups.minus};
   28.21 +  val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT;
   28.22    val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
   28.23  end);
   28.24  
    29.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Fri Feb 19 14:47:00 2010 +0100
    29.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Fri Feb 19 14:47:01 2010 +0100
    29.3 @@ -32,7 +32,7 @@
    29.4    | find_first_numeral past [] = raise TERM("find_first_numeral", []);
    29.5  
    29.6  val zero = mk_number 0;
    29.7 -val mk_plus = HOLogic.mk_binop @{const_name Algebras.plus};
    29.8 +val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
    29.9  
   29.10  (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
   29.11  fun mk_sum []        = zero
   29.12 @@ -43,7 +43,7 @@
   29.13  fun long_mk_sum []        = HOLogic.zero
   29.14    | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   29.15  
   29.16 -val dest_plus = HOLogic.dest_bin @{const_name Algebras.plus} HOLogic.natT;
   29.17 +val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
   29.18  
   29.19  
   29.20  (** Other simproc items **)
   29.21 @@ -61,14 +61,14 @@
   29.22  (*** CancelNumerals simprocs ***)
   29.23  
   29.24  val one = mk_number 1;
   29.25 -val mk_times = HOLogic.mk_binop @{const_name Algebras.times};
   29.26 +val mk_times = HOLogic.mk_binop @{const_name Groups.times};
   29.27  
   29.28  fun mk_prod [] = one
   29.29    | mk_prod [t] = t
   29.30    | mk_prod (t :: ts) = if t = one then mk_prod ts
   29.31                          else mk_times (t, mk_prod ts);
   29.32  
   29.33 -val dest_times = HOLogic.dest_bin @{const_name Algebras.times} HOLogic.natT;
   29.34 +val dest_times = HOLogic.dest_bin @{const_name Groups.times} HOLogic.natT;
   29.35  
   29.36  fun dest_prod t =
   29.37        let val (t,u) = dest_times t
   29.38 @@ -194,8 +194,8 @@
   29.39  structure DiffCancelNumerals = CancelNumeralsFun
   29.40   (open CancelNumeralsCommon
   29.41    val prove_conv = Arith_Data.prove_conv
   29.42 -  val mk_bal   = HOLogic.mk_binop @{const_name Algebras.minus}
   29.43 -  val dest_bal = HOLogic.dest_bin @{const_name Algebras.minus} HOLogic.natT
   29.44 +  val mk_bal   = HOLogic.mk_binop @{const_name Groups.minus}
   29.45 +  val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT
   29.46    val bal_add1 = @{thm nat_diff_add_eq1} RS trans
   29.47    val bal_add2 = @{thm nat_diff_add_eq2} RS trans
   29.48  );
    30.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Fri Feb 19 14:47:00 2010 +0100
    30.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Fri Feb 19 14:47:01 2010 +0100
    30.3 @@ -34,12 +34,12 @@
    30.4  val long_mk_sum = Arith_Data.long_mk_sum;
    30.5  val dest_sum = Arith_Data.dest_sum;
    30.6  
    30.7 -val mk_diff = HOLogic.mk_binop @{const_name Algebras.minus};
    30.8 -val dest_diff = HOLogic.dest_bin @{const_name Algebras.minus} Term.dummyT;
    30.9 +val mk_diff = HOLogic.mk_binop @{const_name Groups.minus};
   30.10 +val dest_diff = HOLogic.dest_bin @{const_name Groups.minus} Term.dummyT;
   30.11  
   30.12 -val mk_times = HOLogic.mk_binop @{const_name Algebras.times};
   30.13 +val mk_times = HOLogic.mk_binop @{const_name Groups.times};
   30.14  
   30.15 -fun one_of T = Const(@{const_name Algebras.one}, T);
   30.16 +fun one_of T = Const(@{const_name Groups.one}, T);
   30.17  
   30.18  (* build product with trailing 1 rather than Numeral 1 in order to avoid the
   30.19     unnecessary restriction to type class number_ring
   30.20 @@ -56,7 +56,7 @@
   30.21  fun long_mk_prod T []        = one_of T
   30.22    | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts);
   30.23  
   30.24 -val dest_times = HOLogic.dest_bin @{const_name Algebras.times} Term.dummyT;
   30.25 +val dest_times = HOLogic.dest_bin @{const_name Groups.times} Term.dummyT;
   30.26  
   30.27  fun dest_prod t =
   30.28        let val (t,u) = dest_times t
   30.29 @@ -72,7 +72,7 @@
   30.30  fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t);
   30.31  
   30.32  (*Express t as a product of (possibly) a numeral with other sorted terms*)
   30.33 -fun dest_coeff sign (Const (@{const_name Algebras.uminus}, _) $ t) = dest_coeff (~sign) t
   30.34 +fun dest_coeff sign (Const (@{const_name Groups.uminus}, _) $ t) = dest_coeff (~sign) t
   30.35    | dest_coeff sign t =
   30.36      let val ts = sort TermOrd.term_ord (dest_prod t)
   30.37          val (n, ts') = find_first_numeral [] ts
   30.38 @@ -104,7 +104,7 @@
   30.39    in mk_times (mk_divide (mk_number T p, mk_number T q), t) end;
   30.40  
   30.41  (*Express t as a product of a fraction with other sorted terms*)
   30.42 -fun dest_fcoeff sign (Const (@{const_name Algebras.uminus}, _) $ t) = dest_fcoeff (~sign) t
   30.43 +fun dest_fcoeff sign (Const (@{const_name Groups.uminus}, _) $ t) = dest_fcoeff (~sign) t
   30.44    | dest_fcoeff sign (Const (@{const_name Rings.divide}, _) $ t $ u) =
   30.45      let val (p, t') = dest_coeff sign t
   30.46          val (q, u') = dest_coeff 1 u
   30.47 @@ -484,7 +484,7 @@
   30.48  in
   30.49  fun sign_conv pos_th neg_th ss t =
   30.50    let val T = fastype_of t;
   30.51 -      val zero = Const(@{const_name Algebras.zero}, T);
   30.52 +      val zero = Const(@{const_name Groups.zero}, T);
   30.53        val less = Const(@{const_name Orderings.less}, [T,T] ---> HOLogic.boolT);
   30.54        val pos = less $ zero $ t and neg = less $ t $ zero
   30.55        fun prove p =
    31.1 --- a/src/HOL/Tools/refute.ML	Fri Feb 19 14:47:00 2010 +0100
    31.2 +++ b/src/HOL/Tools/refute.ML	Fri Feb 19 14:47:01 2010 +0100
    31.3 @@ -710,11 +710,11 @@
    31.4        | Const (@{const_name Finite_Set.finite}, _) => t
    31.5        | Const (@{const_name Orderings.less}, Type ("fun", [Type ("nat", []),
    31.6          Type ("fun", [Type ("nat", []), Type ("bool", [])])])) => t
    31.7 -      | Const (@{const_name Algebras.plus}, Type ("fun", [Type ("nat", []),
    31.8 +      | Const (@{const_name Groups.plus}, Type ("fun", [Type ("nat", []),
    31.9          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
   31.10 -      | Const (@{const_name Algebras.minus}, Type ("fun", [Type ("nat", []),
   31.11 +      | Const (@{const_name Groups.minus}, Type ("fun", [Type ("nat", []),
   31.12          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
   31.13 -      | Const (@{const_name Algebras.times}, Type ("fun", [Type ("nat", []),
   31.14 +      | Const (@{const_name Groups.times}, Type ("fun", [Type ("nat", []),
   31.15          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) => t
   31.16        | Const (@{const_name List.append}, _) => t
   31.17        | Const (@{const_name lfp}, _) => t
   31.18 @@ -886,13 +886,13 @@
   31.19        | Const (@{const_name Orderings.less}, T as Type ("fun", [Type ("nat", []),
   31.20          Type ("fun", [Type ("nat", []), Type ("bool", [])])])) =>
   31.21            collect_type_axioms T axs
   31.22 -      | Const (@{const_name Algebras.plus}, T as Type ("fun", [Type ("nat", []),
   31.23 +      | Const (@{const_name Groups.plus}, T as Type ("fun", [Type ("nat", []),
   31.24          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   31.25            collect_type_axioms T axs
   31.26 -      | Const (@{const_name Algebras.minus}, T as Type ("fun", [Type ("nat", []),
   31.27 +      | Const (@{const_name Groups.minus}, T as Type ("fun", [Type ("nat", []),
   31.28          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   31.29            collect_type_axioms T axs
   31.30 -      | Const (@{const_name Algebras.times}, T as Type ("fun", [Type ("nat", []),
   31.31 +      | Const (@{const_name Groups.times}, T as Type ("fun", [Type ("nat", []),
   31.32          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   31.33            collect_type_axioms T axs
   31.34        | Const (@{const_name List.append}, T) => collect_type_axioms T axs
   31.35 @@ -2794,7 +2794,7 @@
   31.36  
   31.37    fun Nat_plus_interpreter thy model args t =
   31.38      case t of
   31.39 -      Const (@{const_name Algebras.plus}, Type ("fun", [Type ("nat", []),
   31.40 +      Const (@{const_name Groups.plus}, Type ("fun", [Type ("nat", []),
   31.41          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   31.42        let
   31.43          val size_of_nat = size_of_type thy model (Type ("nat", []))
   31.44 @@ -2825,7 +2825,7 @@
   31.45  
   31.46    fun Nat_minus_interpreter thy model args t =
   31.47      case t of
   31.48 -      Const (@{const_name Algebras.minus}, Type ("fun", [Type ("nat", []),
   31.49 +      Const (@{const_name Groups.minus}, Type ("fun", [Type ("nat", []),
   31.50          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   31.51        let
   31.52          val size_of_nat = size_of_type thy model (Type ("nat", []))
   31.53 @@ -2853,7 +2853,7 @@
   31.54  
   31.55    fun Nat_times_interpreter thy model args t =
   31.56      case t of
   31.57 -      Const (@{const_name Algebras.times}, Type ("fun", [Type ("nat", []),
   31.58 +      Const (@{const_name Groups.times}, Type ("fun", [Type ("nat", []),
   31.59          Type ("fun", [Type ("nat", []), Type ("nat", [])])])) =>
   31.60        let
   31.61          val size_of_nat = size_of_type thy model (Type ("nat", []))
    32.1 --- a/src/HOL/ex/Arith_Examples.thy	Fri Feb 19 14:47:00 2010 +0100
    32.2 +++ b/src/HOL/ex/Arith_Examples.thy	Fri Feb 19 14:47:01 2010 +0100
    32.3 @@ -33,7 +33,7 @@
    32.4  *)
    32.5  
    32.6  subsection {* Splitting of Operators: @{term max}, @{term min}, @{term abs},
    32.7 -           @{term Algebras.minus}, @{term nat}, @{term Divides.mod},
    32.8 +           @{term minus}, @{term nat}, @{term Divides.mod},
    32.9             @{term Divides.div} *}
   32.10  
   32.11  lemma "(i::nat) <= max i j"
    33.1 --- a/src/HOL/ex/Binary.thy	Fri Feb 19 14:47:00 2010 +0100
    33.2 +++ b/src/HOL/ex/Binary.thy	Fri Feb 19 14:47:01 2010 +0100
    33.3 @@ -24,8 +24,8 @@
    33.4      | dest_bit (Const (@{const_name True}, _)) = 1
    33.5      | dest_bit t = raise TERM ("dest_bit", [t]);
    33.6  
    33.7 -  fun dest_binary (Const (@{const_name Algebras.zero}, Type (@{type_name nat}, _))) = 0
    33.8 -    | dest_binary (Const (@{const_name Algebras.one}, Type (@{type_name nat}, _))) = 1
    33.9 +  fun dest_binary (Const (@{const_name Groups.zero}, Type (@{type_name nat}, _))) = 0
   33.10 +    | dest_binary (Const (@{const_name Groups.one}, Type (@{type_name nat}, _))) = 1
   33.11      | dest_binary (Const (@{const_name bit}, _) $ bs $ b) = 2 * dest_binary bs + dest_bit b
   33.12      | dest_binary t = raise TERM ("dest_binary", [t]);
   33.13  
    34.1 --- a/src/HOL/ex/SVC_Oracle.thy	Fri Feb 19 14:47:00 2010 +0100
    34.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Fri Feb 19 14:47:01 2010 +0100
    34.3 @@ -63,21 +63,21 @@
    34.4      (*abstraction of a numeric literal*)
    34.5      fun lit t = if can HOLogic.dest_number t then t else replace t;
    34.6      (*abstraction of a real/rational expression*)
    34.7 -    fun rat ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    34.8 -      | rat ((c as Const(@{const_name Algebras.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
    34.9 +    fun rat ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
   34.10 +      | rat ((c as Const(@{const_name Groups.minus}, _)) $ x $ y) = c $ (rat x) $ (rat y)
   34.11        | rat ((c as Const(@{const_name Rings.divide}, _)) $ x $ y) = c $ (rat x) $ (rat y)
   34.12 -      | rat ((c as Const(@{const_name Algebras.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
   34.13 -      | rat ((c as Const(@{const_name Algebras.uminus}, _)) $ x) = c $ (rat x)
   34.14 +      | rat ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (rat x) $ (rat y)
   34.15 +      | rat ((c as Const(@{const_name Groups.uminus}, _)) $ x) = c $ (rat x)
   34.16        | rat t = lit t
   34.17      (*abstraction of an integer expression: no div, mod*)
   34.18 -    fun int ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (int x) $ (int y)
   34.19 -      | int ((c as Const(@{const_name Algebras.minus}, _)) $ x $ y) = c $ (int x) $ (int y)
   34.20 -      | int ((c as Const(@{const_name Algebras.times}, _)) $ x $ y) = c $ (int x) $ (int y)
   34.21 -      | int ((c as Const(@{const_name Algebras.uminus}, _)) $ x) = c $ (int x)
   34.22 +    fun int ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (int x) $ (int y)
   34.23 +      | int ((c as Const(@{const_name Groups.minus}, _)) $ x $ y) = c $ (int x) $ (int y)
   34.24 +      | int ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (int x) $ (int y)
   34.25 +      | int ((c as Const(@{const_name Groups.uminus}, _)) $ x) = c $ (int x)
   34.26        | int t = lit t
   34.27      (*abstraction of a natural number expression: no minus*)
   34.28 -    fun nat ((c as Const(@{const_name Algebras.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y)
   34.29 -      | nat ((c as Const(@{const_name Algebras.times}, _)) $ x $ y) = c $ (nat x) $ (nat y)
   34.30 +    fun nat ((c as Const(@{const_name Groups.plus}, _)) $ x $ y) = c $ (nat x) $ (nat y)
   34.31 +      | nat ((c as Const(@{const_name Groups.times}, _)) $ x $ y) = c $ (nat x) $ (nat y)
   34.32        | nat ((c as Const(@{const_name Suc}, _)) $ x) = c $ (nat x)
   34.33        | nat t = lit t
   34.34      (*abstraction of a relation: =, <, <=*)
    35.1 --- a/src/HOL/ex/Summation.thy	Fri Feb 19 14:47:00 2010 +0100
    35.2 +++ b/src/HOL/ex/Summation.thy	Fri Feb 19 14:47:01 2010 +0100
    35.3 @@ -28,7 +28,7 @@
    35.4  
    35.5  lemma \<Delta>_same_shift:
    35.6    assumes "\<Delta> f = \<Delta> g"
    35.7 -  shows "\<exists>l. (op +) l \<circ> f = g"
    35.8 +  shows "\<exists>l. plus l \<circ> f = g"
    35.9  proof -
   35.10    fix k
   35.11    from assms have "\<And>k. \<Delta> f k = \<Delta> g k" by simp
   35.12 @@ -44,9 +44,9 @@
   35.13      show "f k - g k = f 0 - g 0"
   35.14        by (induct k rule: int_induct) (simp_all add: k_incr k_decr)
   35.15    qed
   35.16 -  then have "\<And>k. ((op +) (g 0 - f 0) \<circ> f) k = g k"
   35.17 +  then have "\<And>k. (plus (g 0 - f 0) \<circ> f) k = g k"
   35.18      by (simp add: algebra_simps)
   35.19 -  then have "(op +) (g 0 - f 0) \<circ> f = g" ..
   35.20 +  then have "plus (g 0 - f 0) \<circ> f = g" ..
   35.21    then show ?thesis ..
   35.22  qed
   35.23  
   35.24 @@ -99,7 +99,7 @@
   35.25    "\<Sigma> (\<Delta> f) j l = f l - f j"
   35.26  proof -
   35.27    from \<Delta>_\<Sigma> have "\<Delta> (\<Sigma> (\<Delta> f) j) = \<Delta> f" .
   35.28 -  then obtain k where "(op +) k \<circ> \<Sigma> (\<Delta> f) j = f" by (blast dest: \<Delta>_same_shift)
   35.29 +  then obtain k where "plus k \<circ> \<Sigma> (\<Delta> f) j = f" by (blast dest: \<Delta>_same_shift)
   35.30    then have "\<And>q. f q = k + \<Sigma> (\<Delta> f) j q" by (simp add: expand_fun_eq)
   35.31    then show ?thesis by simp
   35.32  qed
    36.1 --- a/src/HOL/ex/svc_funcs.ML	Fri Feb 19 14:47:00 2010 +0100
    36.2 +++ b/src/HOL/ex/svc_funcs.ML	Fri Feb 19 14:47:01 2010 +0100
    36.3 @@ -146,16 +146,16 @@
    36.4      (*translation of a literal*)
    36.5      val lit = snd o HOLogic.dest_number;
    36.6      (*translation of a literal expression [no variables]*)
    36.7 -    fun litExp (Const(@{const_name Algebras.plus}, T) $ x $ y) =
    36.8 +    fun litExp (Const(@{const_name Groups.plus}, T) $ x $ y) =
    36.9            if is_numeric_op T then (litExp x) + (litExp y)
   36.10            else fail t
   36.11 -      | litExp (Const(@{const_name Algebras.minus}, T) $ x $ y) =
   36.12 +      | litExp (Const(@{const_name Groups.minus}, T) $ x $ y) =
   36.13            if is_numeric_op T then (litExp x) - (litExp y)
   36.14            else fail t
   36.15 -      | litExp (Const(@{const_name Algebras.times}, T) $ x $ y) =
   36.16 +      | litExp (Const(@{const_name Groups.times}, T) $ x $ y) =
   36.17            if is_numeric_op T then (litExp x) * (litExp y)
   36.18            else fail t
   36.19 -      | litExp (Const(@{const_name Algebras.uminus}, T) $ x)   =
   36.20 +      | litExp (Const(@{const_name Groups.uminus}, T) $ x)   =
   36.21            if is_numeric_op T then ~(litExp x)
   36.22            else fail t
   36.23        | litExp t = lit t
   36.24 @@ -163,21 +163,21 @@
   36.25      (*translation of a real/rational expression*)
   36.26      fun suc t = Interp("+", [Int 1, t])
   36.27      fun tm (Const(@{const_name Suc}, T) $ x) = suc (tm x)
   36.28 -      | tm (Const(@{const_name Algebras.plus}, T) $ x $ y) =
   36.29 +      | tm (Const(@{const_name Groups.plus}, T) $ x $ y) =
   36.30            if is_numeric_op T then Interp("+", [tm x, tm y])
   36.31            else fail t
   36.32 -      | tm (Const(@{const_name Algebras.minus}, T) $ x $ y) =
   36.33 +      | tm (Const(@{const_name Groups.minus}, T) $ x $ y) =
   36.34            if is_numeric_op T then
   36.35                Interp("+", [tm x, Interp("*", [Int ~1, tm y])])
   36.36            else fail t
   36.37 -      | tm (Const(@{const_name Algebras.times}, T) $ x $ y) =
   36.38 +      | tm (Const(@{const_name Groups.times}, T) $ x $ y) =
   36.39            if is_numeric_op T then Interp("*", [tm x, tm y])
   36.40            else fail t
   36.41        | tm (Const(@{const_name Rings.inverse}, T) $ x) =
   36.42            if domain_type T = HOLogic.realT then
   36.43                Rat(1, litExp x)
   36.44            else fail t
   36.45 -      | tm (Const(@{const_name Algebras.uminus}, T) $ x) =
   36.46 +      | tm (Const(@{const_name Groups.uminus}, T) $ x) =
   36.47            if is_numeric_op T then Interp("*", [Int ~1, tm x])
   36.48            else fail t
   36.49        | tm t = Int (lit t)
    37.1 --- a/src/Provers/Arith/abel_cancel.ML	Fri Feb 19 14:47:00 2010 +0100
    37.2 +++ b/src/Provers/Arith/abel_cancel.ML	Fri Feb 19 14:47:01 2010 +0100
    37.3 @@ -28,29 +28,29 @@
    37.4  
    37.5  (* FIXME dependent on abstract syntax *)
    37.6  
    37.7 -fun zero t = Const (@{const_name Algebras.zero}, t);
    37.8 -fun minus t = Const (@{const_name Algebras.uminus}, t --> t);
    37.9 +fun zero t = Const (@{const_name Groups.zero}, t);
   37.10 +fun minus t = Const (@{const_name Groups.uminus}, t --> t);
   37.11  
   37.12 -fun add_terms pos (Const (@{const_name Algebras.plus}, _) $ x $ y, ts) =
   37.13 +fun add_terms pos (Const (@{const_name Groups.plus}, _) $ x $ y, ts) =
   37.14        add_terms pos (x, add_terms pos (y, ts))
   37.15 -  | add_terms pos (Const (@{const_name Algebras.minus}, _) $ x $ y, ts) =
   37.16 +  | add_terms pos (Const (@{const_name Groups.minus}, _) $ x $ y, ts) =
   37.17        add_terms pos (x, add_terms (not pos) (y, ts))
   37.18 -  | add_terms pos (Const (@{const_name Algebras.uminus}, _) $ x, ts) =
   37.19 +  | add_terms pos (Const (@{const_name Groups.uminus}, _) $ x, ts) =
   37.20        add_terms (not pos) (x, ts)
   37.21    | add_terms pos (x, ts) = (pos,x) :: ts;
   37.22  
   37.23  fun terms fml = add_terms true (fml, []);
   37.24  
   37.25 -fun zero1 pt (u as (c as Const(@{const_name Algebras.plus},_)) $ x $ y) =
   37.26 +fun zero1 pt (u as (c as Const(@{const_name Groups.plus},_)) $ x $ y) =
   37.27        (case zero1 pt x of NONE => (case zero1 pt y of NONE => NONE
   37.28                                     | SOME z => SOME(c $ x $ z))
   37.29         | SOME z => SOME(c $ z $ y))
   37.30 -  | zero1 (pos,t) (u as (c as Const(@{const_name Algebras.minus},_)) $ x $ y) =
   37.31 +  | zero1 (pos,t) (u as (c as Const(@{const_name Groups.minus},_)) $ x $ y) =
   37.32        (case zero1 (pos,t) x of
   37.33           NONE => (case zero1 (not pos,t) y of NONE => NONE
   37.34                    | SOME z => SOME(c $ x $ z))
   37.35         | SOME z => SOME(c $ z $ y))
   37.36 -  | zero1 (pos,t) (u as (c as Const(@{const_name Algebras.uminus},_)) $ x) =
   37.37 +  | zero1 (pos,t) (u as (c as Const(@{const_name Groups.uminus},_)) $ x) =
   37.38        (case zero1 (not pos,t) x of NONE => NONE
   37.39         | SOME z => SOME(c $ z))
   37.40    | zero1 (pos,t) u =
   37.41 @@ -71,7 +71,7 @@
   37.42  fun cancel t =
   37.43    let
   37.44      val c $ lhs $ rhs = t
   37.45 -    val opp = case c of Const(@{const_name Algebras.plus},_) => true | _ => false;
   37.46 +    val opp = case c of Const(@{const_name Groups.plus},_) => true | _ => false;
   37.47      val (pos,l) = find_common opp (terms lhs) (terms rhs)
   37.48      val posr = if opp then not pos else pos
   37.49      val t' = c $ (the(zero1 (pos,l) lhs)) $ (the(zero1 (posr,l) rhs))
    38.1 --- a/src/Provers/Arith/cancel_div_mod.ML	Fri Feb 19 14:47:00 2010 +0100
    38.2 +++ b/src/Provers/Arith/cancel_div_mod.ML	Fri Feb 19 14:47:01 2010 +0100
    38.3 @@ -34,12 +34,12 @@
    38.4  functor CancelDivModFun(Data: CANCEL_DIV_MOD_DATA): CANCEL_DIV_MOD =
    38.5  struct
    38.6  
    38.7 -fun coll_div_mod (Const(@{const_name Algebras.plus},_) $ s $ t) dms =
    38.8 +fun coll_div_mod (Const(@{const_name Groups.plus},_) $ s $ t) dms =
    38.9        coll_div_mod t (coll_div_mod s dms)
   38.10 -  | coll_div_mod (Const(@{const_name Algebras.times},_) $ m $ (Const(d,_) $ s $ n))
   38.11 +  | coll_div_mod (Const(@{const_name Groups.times},_) $ m $ (Const(d,_) $ s $ n))
   38.12                   (dms as (divs,mods)) =
   38.13        if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
   38.14 -  | coll_div_mod (Const(@{const_name Algebras.times},_) $ (Const(d,_) $ s $ n) $ m)
   38.15 +  | coll_div_mod (Const(@{const_name Groups.times},_) $ (Const(d,_) $ s $ n) $ m)
   38.16                   (dms as (divs,mods)) =
   38.17        if d = Data.div_name andalso m=n then ((s,n)::divs,mods) else dms
   38.18    | coll_div_mod (Const(m,_) $ s $ n) (dms as (divs,mods)) =
   38.19 @@ -55,8 +55,8 @@
   38.20     ==> thesis by transitivity
   38.21  *)
   38.22  
   38.23 -val mk_plus = Data.mk_binop @{const_name Algebras.plus};
   38.24 -val mk_times = Data.mk_binop @{const_name Algebras.times};
   38.25 +val mk_plus = Data.mk_binop @{const_name Groups.plus};
   38.26 +val mk_times = Data.mk_binop @{const_name Groups.times};
   38.27  
   38.28  fun rearrange t pq =
   38.29    let val ts = Data.dest_sum t;