# HG changeset patch
# User wenzelm
# Date 1082624494 -7200
# Node ID 02b8f3bcf7fe0cb9b0e3b7bc8ca8de3fcef2e358
# Parent  0390abdd1e622d6cd740e19db136ba7954bcbc2c
improved notation;

diff -r 0390abdd1e62 -r 02b8f3bcf7fe src/HOL/Algebra/CRing.thy
--- a/src/HOL/Algebra/CRing.thy	Thu Apr 22 11:00:22 2004 +0200
+++ b/src/HOL/Algebra/CRing.thy	Thu Apr 22 11:01:34 2004 +0200
@@ -16,12 +16,12 @@
 
 text {* Derived operations. *}
 
-constdefs
-  a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
+constdefs (structure R)
+  a_inv :: "[_, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
   "a_inv R == m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
 
   minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
-  "[| x \<in> carrier R; y \<in> carrier R |] ==> minus R x y == add R x (a_inv R y)"
+  "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y == x \<oplus> (\<ominus> y)"
 
 locale abelian_monoid = struct G +
   assumes a_comm_monoid: "comm_monoid (| carrier = carrier G,
@@ -183,10 +183,22 @@
 *}
 
 constdefs
-  finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b"
+  finsum :: "[_, 'a => 'b, 'a set] => 'b"
   "finsum G f A == finprod (| carrier = carrier G,
      mult = add G, one = zero G |) f A"
 
+syntax
+  "_finsum" :: "index => idt => 'a set => 'b => 'b"
+      ("\<Oplus>__:_. _" [1000, 0, 51, 10] 10)
+syntax (xsymbols)
+  "_finsum" :: "index => idt => 'a set => 'b => 'b"
+      ("\<Oplus>__\<in>_. _" [1000, 0, 51, 10] 10)
+syntax (HTML output)
+  "_finsum" :: "index => idt => 'a set => 'b => 'b"
+      ("\<Oplus>__\<in>_. _" [1000, 0, 51, 10] 10)
+translations
+  "\<Oplus>\<index>i:A. b" == "finsum \<struct>\<index> (%i. b) A"  -- {* Beware of argument permutation! *}
+
 (*
   lemmas (in abelian_monoid) finsum_empty [simp] =
     comm_monoid.finprod_empty [OF a_comm_monoid, simplified]
@@ -214,7 +226,7 @@
     folded finsum_def, simplified monoid_record_simps])
 
 lemma (in abelian_monoid) finsum_zero [simp]:
-  "finite A ==> finsum G (%i. \<zero>) A = \<zero>"
+  "finite A ==> (\<Oplus>i: A. \<zero>) = \<zero>"
   by (rule comm_monoid.finprod_one [OF a_comm_monoid, folded finsum_def,
     simplified monoid_record_simps])
 
diff -r 0390abdd1e62 -r 02b8f3bcf7fe src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Thu Apr 22 11:00:22 2004 +0200
+++ b/src/HOL/Algebra/Coset.thy	Thu Apr 22 11:01:34 2004 +0200
@@ -9,23 +9,23 @@
 
 declare (in group) l_inv [simp]  r_inv [simp] 
 
-constdefs
-  r_coset    :: "[('a,'b) monoid_scheme,'a set, 'a] => 'a set"    
-   "r_coset G H a == (% x. (mult G) x a) ` H"
+constdefs (structure G)
+  r_coset    :: "[_,'a set, 'a] => 'a set"    
+   "r_coset G H a == (% x. x \<otimes> a) ` H"
 
-  l_coset    :: "[('a,'b) monoid_scheme, 'a, 'a set] => 'a set"
-   "l_coset G a H == (% x. (mult G) a x) ` H"
+  l_coset    :: "[_, 'a, 'a set] => 'a set"
+   "l_coset G a H == (% x. a \<otimes> x) ` H"
 
-  rcosets  :: "[('a,'b) monoid_scheme,'a set] => ('a set)set"
+  rcosets  :: "[_, 'a set] => ('a set)set"
    "rcosets G H == r_coset G H ` (carrier G)"
 
-  set_mult  :: "[('a,'b) monoid_scheme,'a set,'a set] => 'a set"
-   "set_mult G H K == (%(x,y). (mult G) x y) ` (H \<times> K)"
+  set_mult  :: "[_, 'a set ,'a set] => 'a set"
+   "set_mult G H K == (%(x,y). x \<otimes> y) ` (H \<times> K)"
 
-  set_inv   :: "[('a,'b) monoid_scheme,'a set] => 'a set"
-   "set_inv G H == (m_inv G) ` H"
+  set_inv   :: "[_,'a set] => 'a set"
+   "set_inv G H == m_inv G ` H"
 
-  normal     :: "['a set, ('a,'b) monoid_scheme] => bool"       (infixl "<|" 60)
+  normal     :: "['a set, _] => bool"       (infixl "<|" 60)
    "normal H G == subgroup H G & 
                   (\<forall>x \<in> carrier G. r_coset G H x = l_coset G x H)"
 
diff -r 0390abdd1e62 -r 02b8f3bcf7fe src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Thu Apr 22 11:00:22 2004 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy	Thu Apr 22 11:01:34 2004 +0200
@@ -9,9 +9,10 @@
 
 theory FiniteProduct = Group:
 
-(* Instantiation of LC from Finite_Set.thy is not possible,
-   because here we have explicit typing rules like x : carrier G.
-   We introduce an explicit argument for the domain D *)
+text {* Instantiation of @{text LC} from theory @{text Finite_Set} is not
+  possible, because here we have explicit typing rules like @{text "x
+  : carrier G"}.  We introduce an explicit argument for the domain
+  @{text D}. *}
 
 consts
   foldSetD :: "['a set, 'b => 'a => 'a, 'a] => ('b set * 'a) set"
@@ -281,14 +282,23 @@
 
 subsection {* Products over Finite Sets *}
 
-constdefs
-  finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
+constdefs (structure G)
+  finprod :: "[_, 'a => 'b, 'a set] => 'b"
   "finprod G f A == if finite A
-      then foldD (carrier G) (mult G o f) (one G) A
+      then foldD (carrier G) (mult G o f) \<one> A
       else arbitrary"
 
-(* TODO: nice syntax for the summation operator inside the locale
-   like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *)
+syntax
+  "_finprod" :: "index => idt => 'a set => 'b => 'b"
+      ("\<Otimes>__:_. _" [1000, 0, 51, 10] 10)
+syntax (xsymbols)
+  "_finprod" :: "index => idt => 'a set => 'b => 'b"
+      ("\<Otimes>__\<in>_. _" [1000, 0, 51, 10] 10)
+syntax (HTML output)
+  "_finprod" :: "index => idt => 'a set => 'b => 'b"
+      ("\<Otimes>__\<in>_. _" [1000, 0, 51, 10] 10)
+translations
+  "\<Otimes>\<index>i:A. b" == "finprod \<struct>\<index> (%i. b) A"  -- {* Beware of argument permutation! *}
 
 ML_setup {* 
   simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
@@ -324,7 +334,7 @@
   done
 
 lemma (in comm_monoid) finprod_one [simp]:
-  "finite A ==> finprod G (%i. \<one>) A = \<one>"
+  "finite A ==> (\<Otimes>i:A. \<one>) = \<one>"
 proof (induct set: Finites)
   case empty show ?case by simp
 next
diff -r 0390abdd1e62 -r 02b8f3bcf7fe src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Thu Apr 22 11:00:22 2004 +0200
+++ b/src/HOL/Algebra/Group.thy	Thu Apr 22 11:01:34 2004 +0200
@@ -31,14 +31,12 @@
 record 'a monoid = "'a semigroup" +
   one :: 'a ("\<one>\<index>")
 
-constdefs
-  m_inv :: "[('a, 'm) monoid_scheme, 'a] => 'a" ("inv\<index> _" [81] 80)
-  "m_inv G x == (THE y. y \<in> carrier G &
-                  mult G x y = one G & mult G y x = one G)"
+constdefs (structure G)
+  m_inv :: "_ => 'a => 'a" ("inv\<index> _" [81] 80)
+  "inv x == (THE y. y \<in> carrier G & x \<otimes> y = \<one> & y \<otimes> x = \<one>)"
 
-  Units :: "('a, 'm) monoid_scheme => 'a set"
-  "Units G == {y. y \<in> carrier G &
-                  (EX x : carrier G. mult G x y = one G & mult G y x = one G)}"
+  Units :: "_ => 'a set"
+  "Units G == {y. y \<in> carrier G & (EX x : carrier G. x \<otimes> y = \<one> & y \<otimes> x = \<one>)}"
 
 consts
   pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
@@ -492,20 +490,13 @@
 
 subsection {* Direct Products *}
 
-constdefs
-  DirProdSemigroup ::
-    "[('a, 'm) semigroup_scheme, ('b, 'n) semigroup_scheme]
-    => ('a \<times> 'b) semigroup"
-    (infixr "\<times>\<^sub>s" 80)
+constdefs (structure G and H)
+  DirProdSemigroup :: "_ => _ => ('a \<times> 'b) semigroup"  (infixr "\<times>\<^sub>s" 80)
   "G \<times>\<^sub>s H == (| carrier = carrier G \<times> carrier H,
-    mult = (%(xg, xh) (yg, yh). (mult G xg yg, mult H xh yh)) |)"
+    mult = (%(xg, xh) (yg, yh). (xg \<otimes> yg, xh \<otimes>\<^sub>2 yh)) |)"
 
-  DirProdGroup ::
-    "[('a, 'm) monoid_scheme, ('b, 'n) monoid_scheme] => ('a \<times> 'b) monoid"
-    (infixr "\<times>\<^sub>g" 80)
-  "G \<times>\<^sub>g H == (| carrier = carrier (G \<times>\<^sub>s H),
-    mult = mult (G \<times>\<^sub>s H),
-    one = (one G, one H) |)"
+  DirProdGroup :: "_ => _ => ('a \<times> 'b) monoid"  (infixr "\<times>\<^sub>g" 80)
+  "G \<times>\<^sub>g H == semigroup.extend (G \<times>\<^sub>s H) (| one = (\<one>, \<one>\<^sub>2) |)"
 
 lemma DirProdSemigroup_magma:
   includes magma G + magma H
@@ -529,13 +520,13 @@
   includes magma G + magma H
   shows "magma (G \<times>\<^sub>g H)"
   by (rule magma.intro)
-    (auto simp add: DirProdGroup_def DirProdSemigroup_def)
+    (auto simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
 
 lemma DirProdGroup_semigroup_axioms:
   includes semigroup G + semigroup H
   shows "semigroup_axioms (G \<times>\<^sub>g H)"
   by (rule semigroup_axioms.intro)
-    (auto simp add: DirProdGroup_def DirProdSemigroup_def
+    (auto simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs
       G.m_assoc H.m_assoc)
 
 lemma DirProdGroup_semigroup:
@@ -545,26 +536,26 @@
   by (fast intro: semigroup.intro
     DirProdGroup_magma DirProdGroup_semigroup_axioms)
 
-(* ... and further lemmas for group ... *)
+text {* \dots\ and further lemmas for group \dots *}
 
 lemma DirProdGroup_group:
   includes group G + group H
   shows "group (G \<times>\<^sub>g H)"
   by (rule groupI)
     (auto intro: G.m_assoc H.m_assoc G.l_inv H.l_inv
-      simp add: DirProdGroup_def DirProdSemigroup_def)
+      simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
 
 lemma carrier_DirProdGroup [simp]:
      "carrier (G \<times>\<^sub>g H) = carrier G \<times> carrier H"
-  by (simp add: DirProdGroup_def DirProdSemigroup_def)
+  by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
 
 lemma one_DirProdGroup [simp]:
      "one (G \<times>\<^sub>g H) = (one G, one H)"
-  by (simp add: DirProdGroup_def DirProdSemigroup_def);
+  by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
 
 lemma mult_DirProdGroup [simp]:
      "mult (G \<times>\<^sub>g H) (g, h) (g', h') = (mult G g g', mult H h h')"
-  by (simp add: DirProdGroup_def DirProdSemigroup_def)
+  by (simp add: DirProdGroup_def DirProdSemigroup_def semigroup.defs)
 
 lemma inv_DirProdGroup [simp]:
   includes group G + group H
@@ -577,12 +568,11 @@
 
 subsection {* Homomorphisms *}
 
-constdefs
-  hom :: "[('a, 'c) semigroup_scheme, ('b, 'd) semigroup_scheme]
-    => ('a => 'b)set"
+constdefs (structure G and H)
+  hom :: "_ => _ => ('a => 'b) set"
   "hom G H ==
     {h. h \<in> carrier G -> carrier H &
-      (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (mult G x y) = mult H (h x) (h y))}"
+      (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes> y) = h x \<otimes>\<^sub>2 h y)}"
 
 lemma (in semigroup) hom:
   includes semigroup G
diff -r 0390abdd1e62 -r 02b8f3bcf7fe src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Thu Apr 22 11:00:22 2004 +0200
+++ b/src/HOL/Algebra/Lattice.thy	Thu Apr 22 11:01:34 2004 +0200
@@ -25,40 +25,41 @@
                   "[| x \<sqsubseteq> y; y \<sqsubseteq> z;
                    x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
 
-constdefs
-  less :: "[('a, 'm) order_scheme, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
-  "less L x y == le L x y & x ~= y"
+constdefs (structure L)
+  less :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
+  "x \<sqsubset> y == x \<sqsubseteq> y & x ~= y"
 
-  (* Upper and lower bounds of a set. *)
-  Upper :: "[('a, 'm) order_scheme, 'a set] => 'a set"
+  -- {* Upper and lower bounds of a set. *}
+  Upper :: "[_, 'a set] => 'a set"
   "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> le L x u)} \<inter>
                 carrier L"
 
-  Lower :: "[('a, 'm) order_scheme, 'a set] => 'a set"
+  Lower :: "[_, 'a set] => 'a set"
   "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> le L l x)} \<inter>
                 carrier L"
 
-  (* Least and greatest, as predicate. *)
-  least :: "[('a, 'm) order_scheme, 'a, 'a set] => bool"
+  -- {* Least and greatest, as predicate. *}
+  least :: "[_, 'a, 'a set] => bool"
   "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. le L l x)"
 
-  greatest :: "[('a, 'm) order_scheme, 'a, 'a set] => bool"
+  greatest :: "[_, 'a, 'a set] => bool"
   "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. le L x g)"
 
-  (* Supremum and infimum *)
-  sup :: "[('a, 'm) order_scheme, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
-  "sup L A == THE x. least L x (Upper L A)"
+  -- {* Supremum and infimum *}
+  sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
+  "\<Squnion>A == THE x. least L x (Upper L A)"
 
-  inf :: "[('a, 'm) order_scheme, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
-  "inf L A == THE x. greatest L x (Lower L A)"
+  inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
+  "\<Sqinter>A == THE x. greatest L x (Lower L A)"
 
-  join :: "[('a, 'm) order_scheme, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
-  "join L x y == sup L {x, y}"
+  join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
+  "x \<squnion> y == sup L {x, y}"
 
-  meet :: "[('a, 'm) order_scheme, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 65)
-  "meet L x y == inf L {x, y}"
+  meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 65)
+  "x \<sqinter> y == inf L {x, y}"
 
-(* Upper *)
+
+subsubsection {* Upper *}
 
 lemma Upper_closed [intro, simp]:
   "Upper L A \<subseteq> carrier L"
@@ -78,7 +79,8 @@
   "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
   by (unfold Upper_def) blast
 
-(* Lower *)
+
+subsubsection {* Lower *}
 
 lemma Lower_closed [intro, simp]:
   "Lower L A \<subseteq> carrier L"
@@ -98,7 +100,8 @@
   "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
   by (unfold Lower_def) blast
 
-(* least *)
+
+subsubsection {* least *}
 
 lemma least_carrier [intro, simp]:
   shows "least L l A ==> l \<in> carrier L"
@@ -131,7 +134,8 @@
   from below show "ALL x : Upper L A. s \<sqsubseteq> x" by fast
 qed
 
-(* greatest *)
+
+subsubsection {* greatest *}
 
 lemma greatest_carrier [intro, simp]:
   shows "greatest L l A ==> l \<in> carrier L"
@@ -199,8 +203,7 @@
   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L"
   by (rule joinI) (rule least_carrier)
 
-lemma (in partial_order) sup_of_singletonI:
-  (* only reflexivity needed ? *)
+lemma (in partial_order) sup_of_singletonI:      (* only reflexivity needed ? *)
   "x \<in> carrier L ==> least L x (Upper L {x})"
   by (rule least_UpperI) fast+
 
@@ -404,7 +407,7 @@
   assumes L: "x \<in> carrier L" "y \<in> carrier L" "z \<in> carrier L"
   shows "x \<squnion> (y \<squnion> z) = \<Squnion> {x, y, z}"
 proof (rule finite_sup_insertI)
-  (* The textbook argument in Jacobson I, p 457 *)
+  -- {* The textbook argument in Jacobson I, p 457 *}
   fix s
   assume sup: "least L s (Upper L {x, y, z})"
   show "x \<squnion> (y \<squnion> z) = s"
@@ -452,8 +455,7 @@
   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L"
   by (rule meetI) (rule greatest_carrier)
 
-lemma (in partial_order) inf_of_singletonI:
-  (* only reflexivity needed ? *)
+lemma (in partial_order) inf_of_singletonI:      (* only reflexivity needed ? *)
   "x \<in> carrier L ==> greatest L x (Lower L {x})"
   by (rule greatest_LowerI) fast+
 
@@ -765,17 +767,17 @@
   by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+
 qed (assumption | rule complete_lattice_axioms.intro)+
 
-constdefs
-  top :: "('a, 'm) order_scheme => 'a" ("\<top>\<index>")
-  "top L == sup L (carrier L)"
+constdefs (structure L)
+  top :: "_ => 'a" ("\<top>\<index>")
+  "\<top> == sup L (carrier L)"
 
-  bottom :: "('a, 'm) order_scheme => 'a" ("\<bottom>\<index>")
-  "bottom L == inf L (carrier L)"
+  bottom :: "_ => 'a" ("\<bottom>\<index>")
+  "\<bottom> == inf L (carrier L)"
 
 
 lemma (in complete_lattice) supI:
   "[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |]
-  ==> P (\<Squnion> A)"
+  ==> P (\<Squnion>A)"
 proof (unfold sup_def)
   assume L: "A \<subseteq> carrier L"
     and P: "!!l. least L l (Upper L A) ==> P l"
diff -r 0390abdd1e62 -r 02b8f3bcf7fe src/HOL/Algebra/Module.thy
--- a/src/HOL/Algebra/Module.thy	Thu Apr 22 11:00:22 2004 +0200
+++ b/src/HOL/Algebra/Module.thy	Thu Apr 22 11:01:34 2004 +0200
@@ -32,61 +32,64 @@
       (a \<odot>\<^sub>2 x) \<otimes>\<^sub>2 y = a \<odot>\<^sub>2 (x \<otimes>\<^sub>2 y)"
 
 lemma moduleI:
+  includes struct R + struct M
   assumes cring: "cring R"
     and abelian_group: "abelian_group M"
     and smult_closed:
-      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> smult M a x \<in> carrier M"
+      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^sub>2 x \<in> carrier M"
     and smult_l_distr:
       "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
-      smult M (add R a b) x = add M (smult M a x) (smult M b x)"
+      (a \<oplus> b) \<odot>\<^sub>2 x = (a \<odot>\<^sub>2 x) \<oplus>\<^sub>2 (b \<odot>\<^sub>2 x)"
     and smult_r_distr:
       "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
-      smult M a (add M x y) = add M (smult M a x) (smult M a y)"
+      a \<odot>\<^sub>2 (x \<oplus>\<^sub>2 y) = (a \<odot>\<^sub>2 x) \<oplus>\<^sub>2 (a \<odot>\<^sub>2 y)"
     and smult_assoc1:
       "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
-      smult M (mult R a b) x = smult M a (smult M b x)"
+      (a \<otimes> b) \<odot>\<^sub>2 x = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 x)"
     and smult_one:
-      "!!x. x \<in> carrier M ==> smult M (one R) x = x"
+      "!!x. x \<in> carrier M ==> \<one> \<odot>\<^sub>2 x = x"
   shows "module R M"
   by (auto intro: module.intro cring.axioms abelian_group.axioms
     module_axioms.intro prems)
 
 lemma algebraI:
+  includes struct R + struct M
   assumes R_cring: "cring R"
     and M_cring: "cring M"
     and smult_closed:
-      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> smult M a x \<in> carrier M"
+      "!!a x. [| a \<in> carrier R; x \<in> carrier M |] ==> a \<odot>\<^sub>2 x \<in> carrier M"
     and smult_l_distr:
       "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
-      smult M (add R a b) x = add M (smult M a x) (smult M b x)"
+      (a \<oplus> b) \<odot>\<^sub>2 x = (a \<odot>\<^sub>2 x) \<oplus>\<^sub>2 (b \<odot>\<^sub>2 x)"
     and smult_r_distr:
       "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
-      smult M a (add M x y) = add M (smult M a x) (smult M a y)"
+      a \<odot>\<^sub>2 (x \<oplus>\<^sub>2 y) = (a \<odot>\<^sub>2 x) \<oplus>\<^sub>2 (a \<odot>\<^sub>2 y)"
     and smult_assoc1:
       "!!a b x. [| a \<in> carrier R; b \<in> carrier R; x \<in> carrier M |] ==>
-      smult M (mult R a b) x = smult M a (smult M b x)"
+      (a \<otimes> b) \<odot>\<^sub>2 x = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 x)"
     and smult_one:
-      "!!x. x \<in> carrier M ==> smult M (one R) x = x"
+      "!!x. x \<in> carrier M ==> (one R) \<odot>\<^sub>2 x = x"
     and smult_assoc2:
       "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
-      mult M (smult M a x) y = smult M a (mult M x y)"
+      (a \<odot>\<^sub>2 x) \<otimes>\<^sub>2 y = a \<odot>\<^sub>2 (x \<otimes>\<^sub>2 y)"
   shows "algebra R M"
   by (auto intro!: algebra.intro algebra_axioms.intro cring.axioms 
     module_axioms.intro prems)
 
 lemma (in algebra) R_cring:
   "cring R"
-  by (rule cring.intro) assumption+
+  by (rule cring.intro)
 
 lemma (in algebra) M_cring:
   "cring M"
-  by (rule cring.intro) assumption+
+  by (rule cring.intro)
 
 lemma (in algebra) module:
   "module R M"
   by (auto intro: moduleI R_cring is_abelian_group
     smult_l_distr smult_r_distr smult_assoc1)
 
+
 subsection {* Basic Properties of Algebras *}
 
 lemma (in algebra) smult_l_null [simp]:
diff -r 0390abdd1e62 -r 02b8f3bcf7fe src/HOL/Algebra/Sylow.thy
--- a/src/HOL/Algebra/Sylow.thy	Thu Apr 22 11:00:22 2004 +0200
+++ b/src/HOL/Algebra/Sylow.thy	Thu Apr 22 11:01:34 2004 +0200
@@ -15,8 +15,8 @@
 subsection {*Order of a Group and Lagrange's Theorem*}
 
 constdefs
-  order     :: "(('a,'b) semigroup_scheme) => nat"
-   "order(S) == card(carrier S)"
+  order     :: "('a,'b) semigroup_scheme => nat"
+  "order S == card (carrier S)"
 
 theorem (in coset) lagrange:
      "[| finite(carrier G); subgroup H G |] 
diff -r 0390abdd1e62 -r 02b8f3bcf7fe src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Thu Apr 22 11:00:22 2004 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Thu Apr 22 11:01:34 2004 +0200
@@ -58,18 +58,18 @@
   monom :: "['a, nat] => 'p"
   coeff :: "['p, nat] => 'a"
 
-constdefs
-  up :: "('a, 'm) ring_scheme => (nat => 'a) set"
-  "up R == {f. f \<in> UNIV -> carrier R & (EX n. bound (zero R) n f)}"
-  UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
+constdefs (structure R)
+  up :: "_ => (nat => 'a) set"
+  "up R == {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero> n f)}"
+  UP :: "_ => ('a, nat => 'a) up_ring"
   "UP R == (|
     carrier = up R,
-    mult = (%p:up R. %q:up R. %n. finsum R (%i. mult R (p i) (q (n-i))) {..n}),
-    one = (%i. if i=0 then one R else zero R),
-    zero = (%i. zero R),
-    add = (%p:up R. %q:up R. %i. add R (p i) (q i)),
-    smult = (%a:carrier R. %p:up R. %i. mult R a (p i)),
-    monom = (%a:carrier R. %n i. if i=n then a else zero R),
+    mult = (%p:up R. %q:up R. %n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i)),
+    one = (%i. if i=0 then \<one> else \<zero>),
+    zero = (%i. \<zero>),
+    add = (%p:up R. %q:up R. %i. p i \<oplus> q i),
+    smult = (%a:carrier R. %p:up R. %i. a \<otimes> p i),
+    monom = (%a:carrier R. %n i. if i=n then a else \<zero>),
     coeff = (%p:up R. %n. p n) |)"
 
 text {*
@@ -179,9 +179,8 @@
 locale UP_domain = UP_cring + "domain" R
 
 text {*
-  Temporarily declare UP.P\_def as simp rule.
-*}
-(* TODO: use antiquotation once text (in locale) is supported. *)
+  Temporarily declare @{text UP.P_def} as simp rule.
+*}  (* TODO: use antiquotation once text (in locale) is supported. *)
 
 declare (in UP) P_def [simp]
 
@@ -785,9 +784,9 @@
 
 subsection {* The degree function *}
 
-constdefs
-  deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
-  "deg R p == LEAST n. bound (zero R) n (coeff (UP R) p)"
+constdefs (structure R)
+  deg :: "[_, nat => 'a] => nat"
+  "deg R p == LEAST n. bound \<zero> n (coeff (UP R) p)"
 
 lemma (in UP_cring) deg_aboveI:
   "[| (!!m. n < m ==> coeff P p m = \<zero>); p \<in> carrier P |] ==> deg R p <= n" 
@@ -1248,11 +1247,10 @@
   "(%a. monom P a 0) \<in> ring_hom R P"
   by (auto intro!: ring_hom_memI intro: up_eqI simp: monom_mult_is_smult)
 
-constdefs
-  eval :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme,
-          'a => 'b, 'b, nat => 'a] => 'b"
-  "eval R S phi s == (\<lambda>p \<in> carrier (UP R).
-    finsum S (%i. mult S (phi (coeff (UP R) p i)) (pow S s i)) {..deg R p})"
+constdefs (structure S)
+  eval :: "[_, _, 'a => 'b, 'b, nat => 'a] => 'b"
+  "eval R S phi s == \<lambda>p \<in> carrier (UP R).
+    \<Oplus>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes> pow S s i"
 (*
   "eval R S phi s p == if p \<in> carrier (UP R)
   then finsum S (%i. mult S (phi (coeff (UP R) p i)) (pow S s i)) {..deg R p}
@@ -1566,5 +1564,4 @@
 
 -- {* Calculates @{term "x = 500"} *}
 
-
 end