# HG changeset patch
# User wenzelm
# Date 1269183460 -3600
# Node ID 19f1f7066917d5c6ca7893dd07fd3965e8e9087c
# Parent  2ae4b758550180311e0232a21ab6ec8862912ada
eliminated old constdefs;

diff -r 2ae4b7585501 -r 19f1f7066917 src/HOL/Algebra/AbelCoset.thy
--- a/src/HOL/Algebra/AbelCoset.thy	Sun Mar 21 06:59:23 2010 +0100
+++ b/src/HOL/Algebra/AbelCoset.thy	Sun Mar 21 15:57:40 2010 +0100
@@ -17,26 +17,29 @@
 
 no_notation Plus (infixr "<+>" 65)
 
-constdefs (structure G)
+definition
   a_r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "+>\<index>" 60)
-  "a_r_coset G \<equiv> r_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+  where "a_r_coset G \<equiv> r_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
 
+definition
   a_l_coset    :: "[_, 'a, 'a set] \<Rightarrow> 'a set"    (infixl "<+\<index>" 60)
-  "a_l_coset G \<equiv> l_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+  where "a_l_coset G \<equiv> l_coset \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
 
+definition
   A_RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("a'_rcosets\<index> _" [81] 80)
-  "A_RCOSETS G H \<equiv> RCOSETS \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
+  where "A_RCOSETS G H \<equiv> RCOSETS \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
 
+definition
   set_add  :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<+>\<index>" 60)
-  "set_add G \<equiv> set_mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+  where "set_add G \<equiv> set_mult \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
 
+definition
   A_SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  ("a'_set'_inv\<index> _" [81] 80)
-  "A_SET_INV G H \<equiv> SET_INV \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
+  where "A_SET_INV G H \<equiv> SET_INV \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
 
-constdefs (structure G)
-  a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \<Rightarrow> ('a*'a)set"
-                  ("racong\<index> _")
-   "a_r_congruent G \<equiv> r_congruent \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
+definition
+  a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \<Rightarrow> ('a*'a)set"  ("racong\<index> _")
+  where "a_r_congruent G \<equiv> r_congruent \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
 
 definition A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "A'_Mod" 65) where
     --{*Actually defined for groups rather than monoids*}
diff -r 2ae4b7585501 -r 19f1f7066917 src/HOL/Algebra/Congruence.thy
--- a/src/HOL/Algebra/Congruence.thy	Sun Mar 21 06:59:23 2010 +0100
+++ b/src/HOL/Algebra/Congruence.thy	Sun Mar 21 15:57:40 2010 +0100
@@ -19,21 +19,25 @@
 record 'a eq_object = "'a partial_object" +
   eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".=\<index>" 50)
 
-constdefs (structure S)
+definition
   elem :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set \<Rightarrow> bool" (infixl ".\<in>\<index>" 50)
-  "x .\<in> A \<equiv> (\<exists>y \<in> A. x .= y)"
+  where "x .\<in>\<^bsub>S\<^esub> A \<equiv> (\<exists>y \<in> A. x .=\<^bsub>S\<^esub> y)"
 
+definition
   set_eq :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool" (infixl "{.=}\<index>" 50)
-  "A {.=} B == ((\<forall>x \<in> A. x .\<in> B) \<and> (\<forall>x \<in> B. x .\<in> A))"
+  where "A {.=}\<^bsub>S\<^esub> B == ((\<forall>x \<in> A. x .\<in>\<^bsub>S\<^esub> B) \<and> (\<forall>x \<in> B. x .\<in>\<^bsub>S\<^esub> A))"
 
+definition
   eq_class_of :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set" ("class'_of\<index> _")
-  "class_of x == {y \<in> carrier S. x .= y}"
+  where "class_of\<^bsub>S\<^esub> x == {y \<in> carrier S. x .=\<^bsub>S\<^esub> y}"
 
+definition
   eq_closure_of :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set" ("closure'_of\<index> _")
-  "closure_of A == {y \<in> carrier S. y .\<in> A}"
+  where "closure_of\<^bsub>S\<^esub> A == {y \<in> carrier S. y .\<in>\<^bsub>S\<^esub> A}"
 
+definition
   eq_is_closed :: "_ \<Rightarrow> 'a set \<Rightarrow> bool" ("is'_closed\<index> _")
-  "is_closed A == (A \<subseteq> carrier S \<and> closure_of A = A)"
+  where "is_closed\<^bsub>S\<^esub> A == (A \<subseteq> carrier S \<and> closure_of\<^bsub>S\<^esub> A = A)"
 
 abbreviation
   not_eq :: "_ \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl ".\<noteq>\<index>" 50)
diff -r 2ae4b7585501 -r 19f1f7066917 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Sun Mar 21 06:59:23 2010 +0100
+++ b/src/HOL/Algebra/Coset.thy	Sun Mar 21 15:57:40 2010 +0100
@@ -8,21 +8,25 @@
 
 section {*Cosets and Quotient Groups*}
 
-constdefs (structure G)
+definition
   r_coset    :: "[_, 'a set, 'a] \<Rightarrow> 'a set"    (infixl "#>\<index>" 60)
-  "H #> a \<equiv> \<Union>h\<in>H. {h \<otimes> a}"
+  where "H #>\<^bsub>G\<^esub> a \<equiv> \<Union>h\<in>H. {h \<otimes>\<^bsub>G\<^esub> a}"
 
+definition
   l_coset    :: "[_, 'a, 'a set] \<Rightarrow> 'a set"    (infixl "<#\<index>" 60)
-  "a <# H \<equiv> \<Union>h\<in>H. {a \<otimes> h}"
+  where "a <#\<^bsub>G\<^esub> H \<equiv> \<Union>h\<in>H. {a \<otimes>\<^bsub>G\<^esub> h}"
 
+definition
   RCOSETS  :: "[_, 'a set] \<Rightarrow> ('a set)set"   ("rcosets\<index> _" [81] 80)
-  "rcosets H \<equiv> \<Union>a\<in>carrier G. {H #> a}"
+  where "rcosets\<^bsub>G\<^esub> H \<equiv> \<Union>a\<in>carrier G. {H #>\<^bsub>G\<^esub> a}"
 
+definition
   set_mult  :: "[_, 'a set ,'a set] \<Rightarrow> 'a set" (infixl "<#>\<index>" 60)
-  "H <#> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes> k}"
+  where "H <#>\<^bsub>G\<^esub> K \<equiv> \<Union>h\<in>H. \<Union>k\<in>K. {h \<otimes>\<^bsub>G\<^esub> k}"
 
+definition
   SET_INV :: "[_,'a set] \<Rightarrow> 'a set"  ("set'_inv\<index> _" [81] 80)
-  "set_inv H \<equiv> \<Union>h\<in>H. {inv h}"
+  where "set_inv\<^bsub>G\<^esub> H \<equiv> \<Union>h\<in>H. {inv\<^bsub>G\<^esub> h}"
 
 
 locale normal = subgroup + group +
@@ -589,10 +593,9 @@
 
 subsubsection{*An Equivalence Relation*}
 
-constdefs (structure G)
-  r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set"
-                  ("rcong\<index> _")
-   "rcong H \<equiv> {(x,y). x \<in> carrier G & y \<in> carrier G & inv x \<otimes> y \<in> H}"
+definition
+  r_congruent :: "[('a,'b)monoid_scheme, 'a set] \<Rightarrow> ('a*'a)set"  ("rcong\<index> _")
+  where "rcong\<^bsub>G\<^esub> H \<equiv> {(x,y). x \<in> carrier G & y \<in> carrier G & inv\<^bsub>G\<^esub> x \<otimes>\<^bsub>G\<^esub> y \<in> H}"
 
 
 lemma (in subgroup) equiv_rcong:
diff -r 2ae4b7585501 -r 19f1f7066917 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Sun Mar 21 06:59:23 2010 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Sun Mar 21 15:57:40 2010 +0100
@@ -160,30 +160,30 @@
 
 subsubsection {* Function definitions *}
 
-constdefs (structure G)
+definition
   factor :: "[_, 'a, 'a] \<Rightarrow> bool" (infix "divides\<index>" 65)
-  "a divides b == \<exists>c\<in>carrier G. b = a \<otimes> c"
-
-constdefs (structure G)
+  where "a divides\<^bsub>G\<^esub> b == \<exists>c\<in>carrier G. b = a \<otimes>\<^bsub>G\<^esub> c"
+
+definition
   associated :: "[_, 'a, 'a] => bool" (infix "\<sim>\<index>" 55)
-  "a \<sim> b == a divides b \<and> b divides a"
+  where "a \<sim>\<^bsub>G\<^esub> b == a divides\<^bsub>G\<^esub> b \<and> b divides\<^bsub>G\<^esub> a"
 
 abbreviation
   "division_rel G == \<lparr>carrier = carrier G, eq = op \<sim>\<^bsub>G\<^esub>, le = op divides\<^bsub>G\<^esub>\<rparr>"
 
-constdefs (structure G)
+definition
   properfactor :: "[_, 'a, 'a] \<Rightarrow> bool"
-  "properfactor G a b == a divides b \<and> \<not>(b divides a)"
-
-constdefs (structure G)
+  where "properfactor G a b == a divides\<^bsub>G\<^esub> b \<and> \<not>(b divides\<^bsub>G\<^esub> a)"
+
+definition
   irreducible :: "[_, 'a] \<Rightarrow> bool"
-  "irreducible G a == a \<notin> Units G \<and> (\<forall>b\<in>carrier G. properfactor G b a \<longrightarrow> b \<in> Units G)"
-
-constdefs (structure G)
-  prime :: "[_, 'a] \<Rightarrow> bool"
-  "prime G p == p \<notin> Units G \<and> 
-                (\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. p divides (a \<otimes> b) \<longrightarrow> p divides a \<or> p divides b)"
-
+  where "irreducible G a == a \<notin> Units G \<and> (\<forall>b\<in>carrier G. properfactor G b a \<longrightarrow> b \<in> Units G)"
+
+definition
+  prime :: "[_, 'a] \<Rightarrow> bool" where
+  "prime G p ==
+    p \<notin> Units G \<and> 
+    (\<forall>a\<in>carrier G. \<forall>b\<in>carrier G. p divides\<^bsub>G\<^esub> (a \<otimes>\<^bsub>G\<^esub> b) \<longrightarrow> p divides\<^bsub>G\<^esub> a \<or> p divides\<^bsub>G\<^esub> b)"
 
 
 subsubsection {* Divisibility *}
@@ -1041,20 +1041,21 @@
 
 subsubsection {* Function definitions *}
 
-constdefs (structure G)
+definition
   factors :: "[_, 'a list, 'a] \<Rightarrow> bool"
-  "factors G fs a == (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>) fs \<one> = a"
-
+  where "factors G fs a == (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>\<^bsub>G\<^esub>) fs \<one>\<^bsub>G\<^esub> = a"
+
+definition
   wfactors ::"[_, 'a list, 'a] \<Rightarrow> bool"
-  "wfactors G fs a == (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>) fs \<one> \<sim> a"
+  where "wfactors G fs a == (\<forall>x \<in> (set fs). irreducible G x) \<and> foldr (op \<otimes>\<^bsub>G\<^esub>) fs \<one>\<^bsub>G\<^esub> \<sim>\<^bsub>G\<^esub> a"
 
 abbreviation
-  list_assoc :: "('a,_) monoid_scheme \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "[\<sim>]\<index>" 44) where
-  "list_assoc G == list_all2 (op \<sim>\<^bsub>G\<^esub>)"
-
-constdefs (structure G)
+  list_assoc :: "('a,_) monoid_scheme \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "[\<sim>]\<index>" 44)
+  where "list_assoc G == list_all2 (op \<sim>\<^bsub>G\<^esub>)"
+
+definition
   essentially_equal :: "[_, 'a list, 'a list] \<Rightarrow> bool"
-  "essentially_equal G fs1 fs2 == (\<exists>fs1'. fs1 <~~> fs1' \<and> fs1' [\<sim>] fs2)"
+  where "essentially_equal G fs1 fs2 == (\<exists>fs1'. fs1 <~~> fs1' \<and> fs1' [\<sim>]\<^bsub>G\<^esub> fs2)"
 
 
 locale factorial_monoid = comm_monoid_cancel +
@@ -1901,7 +1902,7 @@
 abbreviation
   "assocs G x == eq_closure_of (division_rel G) {x}"
 
-constdefs (structure G)
+definition
   "fmset G as \<equiv> multiset_of (map (\<lambda>a. assocs G a) as)"
 
 
@@ -2615,23 +2616,25 @@
 
 subsubsection {* Definitions *}
 
-constdefs (structure G)
+definition
   isgcd :: "[('a,_) monoid_scheme, 'a, 'a, 'a] \<Rightarrow> bool"  ("(_ gcdof\<index> _ _)" [81,81,81] 80)
-  "x gcdof a b \<equiv> x divides a \<and> x divides b \<and> 
-                 (\<forall>y\<in>carrier G. (y divides a \<and> y divides b \<longrightarrow> y divides x))"
-
+  where "x gcdof\<^bsub>G\<^esub> a b \<equiv> x divides\<^bsub>G\<^esub> a \<and> x divides\<^bsub>G\<^esub> b \<and> 
+    (\<forall>y\<in>carrier G. (y divides\<^bsub>G\<^esub> a \<and> y divides\<^bsub>G\<^esub> b \<longrightarrow> y divides\<^bsub>G\<^esub> x))"
+
+definition
   islcm :: "[_, 'a, 'a, 'a] \<Rightarrow> bool"  ("(_ lcmof\<index> _ _)" [81,81,81] 80)
-  "x lcmof a b \<equiv> a divides x \<and> b divides x \<and> 
-                 (\<forall>y\<in>carrier G. (a divides y \<and> b divides y \<longrightarrow> x divides y))"
-
-constdefs (structure G)
+  where "x lcmof\<^bsub>G\<^esub> a b \<equiv> a divides\<^bsub>G\<^esub> x \<and> b divides\<^bsub>G\<^esub> x \<and> 
+    (\<forall>y\<in>carrier G. (a divides\<^bsub>G\<^esub> y \<and> b divides\<^bsub>G\<^esub> y \<longrightarrow> x divides\<^bsub>G\<^esub> y))"
+
+definition
   somegcd :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
-  "somegcd G a b == SOME x. x \<in> carrier G \<and> x gcdof a b"
-
+  where "somegcd G a b == SOME x. x \<in> carrier G \<and> x gcdof\<^bsub>G\<^esub> a b"
+
+definition
   somelcm :: "('a,_) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
-  "somelcm G a b == SOME x. x \<in> carrier G \<and> x lcmof a b"
-
-constdefs (structure G)
+  where "somelcm G a b == SOME x. x \<in> carrier G \<and> x lcmof\<^bsub>G\<^esub> a b"
+
+definition
   "SomeGcd G A == inf (division_rel G) A"
 
 
diff -r 2ae4b7585501 -r 19f1f7066917 src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Sun Mar 21 06:59:23 2010 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy	Sun Mar 21 15:57:40 2010 +0100
@@ -285,11 +285,12 @@
 
 subsubsection {* Products over Finite Sets *}
 
-constdefs (structure G)
-  finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b"
-  "finprod G f A == if finite A
-      then foldD (carrier G) (mult G o f) \<one> A
-      else undefined"
+definition
+  finprod :: "[('b, 'm) monoid_scheme, 'a => 'b, 'a set] => 'b" where
+  "finprod G f A ==
+    if finite A
+    then foldD (carrier G) (mult G o f) \<one>\<^bsub>G\<^esub> A
+    else undefined"
 
 syntax
   "_finprod" :: "index => idt => 'a set => 'b => 'b"
diff -r 2ae4b7585501 -r 19f1f7066917 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Sun Mar 21 06:59:23 2010 +0100
+++ b/src/HOL/Algebra/Group.thy	Sun Mar 21 15:57:40 2010 +0100
@@ -22,13 +22,14 @@
   mult    :: "['a, 'a] \<Rightarrow> 'a" (infixl "\<otimes>\<index>" 70)
   one     :: 'a ("\<one>\<index>")
 
-constdefs (structure G)
+definition
   m_inv :: "('a, 'b) monoid_scheme => 'a => 'a" ("inv\<index> _" [81] 80)
-  "inv x == (THE y. y \<in> carrier G & x \<otimes> y = \<one> & y \<otimes> x = \<one>)"
+  where "inv\<^bsub>G\<^esub> x == (THE y. y \<in> carrier G & x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> & y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)"
 
+definition
   Units :: "_ => 'a set"
   --{*The set of invertible elements*}
-  "Units G == {y. y \<in> carrier G & (\<exists>x \<in> carrier G. x \<otimes> y = \<one> & y \<otimes> x = \<one>)}"
+  where "Units G == {y. y \<in> carrier G & (\<exists>x \<in> carrier G. x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> & y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)}"
 
 consts
   pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
@@ -534,8 +535,8 @@
 
 subsection {* Homomorphisms and Isomorphisms *}
 
-constdefs (structure G and H)
-  hom :: "_ => _ => ('a => 'b) set"
+definition
+  hom :: "_ => _ => ('a => 'b) set" where
   "hom G H ==
     {h. h \<in> carrier G -> carrier H &
       (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}"
diff -r 2ae4b7585501 -r 19f1f7066917 src/HOL/Algebra/Ideal.thy
--- a/src/HOL/Algebra/Ideal.thy	Sun Mar 21 06:59:23 2010 +0100
+++ b/src/HOL/Algebra/Ideal.thy	Sun Mar 21 15:57:40 2010 +0100
@@ -47,9 +47,9 @@
 
 subsubsection (in ring) {* Ideals Generated by a Subset of @{term "carrier R"} *}
 
-constdefs (structure R)
+definition
   genideal :: "('a, 'b) ring_scheme \<Rightarrow> 'a set \<Rightarrow> 'a set"  ("Idl\<index> _" [80] 79)
-  "genideal R S \<equiv> Inter {I. ideal I R \<and> S \<subseteq> I}"
+  where "genideal R S \<equiv> Inter {I. ideal I R \<and> S \<subseteq> I}"
 
 
 subsubsection {* Principal Ideals *}
@@ -451,9 +451,9 @@
 
 text {* Generation of Principal Ideals in Commutative Rings *}
 
-constdefs (structure R)
+definition
   cgenideal :: "('a, 'b) monoid_scheme \<Rightarrow> 'a \<Rightarrow> 'a set"  ("PIdl\<index> _" [80] 79)
-  "cgenideal R a \<equiv> { x \<otimes> a | x. x \<in> carrier R }"
+  where "cgenideal R a \<equiv> {x \<otimes>\<^bsub>R\<^esub> a | x. x \<in> carrier R}"
 
 text {* genhideal (?) really generates an ideal *}
 lemma (in cring) cgenideal_ideal:
diff -r 2ae4b7585501 -r 19f1f7066917 src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Sun Mar 21 06:59:23 2010 +0100
+++ b/src/HOL/Algebra/Lattice.thy	Sun Mar 21 15:57:40 2010 +0100
@@ -25,9 +25,9 @@
     and le_cong:
       "\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w"
 
-constdefs (structure L)
+definition
   lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
-  "x \<sqsubset> y == x \<sqsubseteq> y & x .\<noteq> y"
+  where "x \<sqsubset>\<^bsub>L\<^esub> y == x \<sqsubseteq>\<^bsub>L\<^esub> y & x .\<noteq>\<^bsub>L\<^esub> y"
 
 
 subsubsection {* The order relation *}
@@ -102,12 +102,13 @@
 
 subsubsection {* Upper and lower bounds of a set *}
 
-constdefs (structure L)
+definition
   Upper :: "[_, 'a set] => 'a set"
-  "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter> carrier L"
+  where "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq>\<^bsub>L\<^esub> u)} \<inter> carrier L"
 
+definition
   Lower :: "[_, 'a set] => 'a set"
-  "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter> carrier L"
+  where "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq>\<^bsub>L\<^esub> x)} \<inter> carrier L"
 
 lemma Upper_closed [intro!, simp]:
   "Upper L A \<subseteq> carrier L"
@@ -275,12 +276,13 @@
 
 subsubsection {* Least and greatest, as predicate *}
 
-constdefs (structure L)
+definition
   least :: "[_, 'a, 'a set] => bool"
-  "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)"
+  where "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq>\<^bsub>L\<^esub> x)"
 
+definition
   greatest :: "[_, 'a, 'a set] => bool"
-  "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
+  where "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq>\<^bsub>L\<^esub> g)"
 
 text (in weak_partial_order) {* Could weaken these to @{term "l \<in> carrier L \<and> l
   .\<in> A"} and @{term "g \<in> carrier L \<and> g .\<in> A"}. *}
@@ -400,18 +402,21 @@
 
 text {* Supremum and infimum *}
 
-constdefs (structure L)
+definition
   sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
-  "\<Squnion>A == SOME x. least L x (Upper L A)"
+  where "\<Squnion>\<^bsub>L\<^esub>A == SOME x. least L x (Upper L A)"
 
+definition
   inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
-  "\<Sqinter>A == SOME x. greatest L x (Lower L A)"
+  where "\<Sqinter>\<^bsub>L\<^esub>A == SOME x. greatest L x (Lower L A)"
 
+definition
   join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
-  "x \<squnion> y == \<Squnion> {x, y}"
+  where "x \<squnion>\<^bsub>L\<^esub> y == \<Squnion>\<^bsub>L\<^esub>{x, y}"
 
+definition
   meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
-  "x \<sqinter> y == \<Sqinter> {x, y}"
+  where "x \<sqinter>\<^bsub>L\<^esub> y == \<Sqinter>\<^bsub>L\<^esub>{x, y}"
 
 
 subsection {* Lattices *}
@@ -981,12 +986,13 @@
   shows "weak_complete_lattice L"
   proof qed (auto intro: sup_exists inf_exists)
 
-constdefs (structure L)
+definition
   top :: "_ => 'a" ("\<top>\<index>")
-  "\<top> == sup L (carrier L)"
+  where "\<top>\<^bsub>L\<^esub> == sup L (carrier L)"
 
+definition
   bottom :: "_ => 'a" ("\<bottom>\<index>")
-  "\<bottom> == inf L (carrier L)"
+  where "\<bottom>\<^bsub>L\<^esub> == inf L (carrier L)"
 
 
 lemma (in weak_complete_lattice) supI:
diff -r 2ae4b7585501 -r 19f1f7066917 src/HOL/Algebra/QuotRing.thy
--- a/src/HOL/Algebra/QuotRing.thy	Sun Mar 21 06:59:23 2010 +0100
+++ b/src/HOL/Algebra/QuotRing.thy	Sun Mar 21 15:57:40 2010 +0100
@@ -11,10 +11,10 @@
 
 subsection {* Multiplication on Cosets *}
 
-constdefs (structure R)
+definition
   rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \<Rightarrow> 'a set"
     ("[mod _:] _ \<Otimes>\<index> _" [81,81,81] 80)
-  "rcoset_mult R I A B \<equiv> \<Union>a\<in>A. \<Union>b\<in>B. I +> (a \<otimes> b)"
+  where "rcoset_mult R I A B \<equiv> \<Union>a\<in>A. \<Union>b\<in>B. I +>\<^bsub>R\<^esub> (a \<otimes>\<^bsub>R\<^esub> b)"
 
 
 text {* @{const "rcoset_mult"} fulfils the properties required by
@@ -89,11 +89,10 @@
 
 subsection {* Quotient Ring Definition *}
 
-constdefs (structure R)
-  FactRing :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) ring"
-     (infixl "Quot" 65)
-  "FactRing R I \<equiv>
-    \<lparr>carrier = a_rcosets I, mult = rcoset_mult R I, one = (I +> \<one>), zero = I, add = set_add R\<rparr>"
+definition
+  FactRing :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) ring"  (infixl "Quot" 65)
+  where "FactRing R I \<equiv>
+    \<lparr>carrier = a_rcosets\<^bsub>R\<^esub> I, mult = rcoset_mult R I, one = (I +>\<^bsub>R\<^esub> \<one>\<^bsub>R\<^esub>), zero = I, add = set_add R\<rparr>"
 
 
 subsection {* Factorization over General Ideals *}
diff -r 2ae4b7585501 -r 19f1f7066917 src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Sun Mar 21 06:59:23 2010 +0100
+++ b/src/HOL/Algebra/Ring.thy	Sun Mar 21 15:57:40 2010 +0100
@@ -6,7 +6,8 @@
 
 theory Ring
 imports FiniteProduct
-uses ("ringsimp.ML") begin
+uses ("ringsimp.ML")
+begin
 
 
 section {* The Algebraic Hierarchy of Rings *}
@@ -19,12 +20,13 @@
 
 text {* Derived operations. *}
 
-constdefs (structure R)
+definition
   a_inv :: "[('a, 'm) ring_scheme, 'a ] => 'a" ("\<ominus>\<index> _" [81] 80)
-  "a_inv R == m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
+  where "a_inv R == m_inv (| carrier = carrier R, mult = add R, one = zero R |)"
 
+definition
   a_minus :: "[('a, 'm) ring_scheme, 'a, 'a] => 'a" (infixl "\<ominus>\<index>" 65)
-  "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus> y == x \<oplus> (\<ominus> y)"
+  where "[| x \<in> carrier R; y \<in> carrier R |] ==> x \<ominus>\<^bsub>R\<^esub> y == x \<oplus>\<^bsub>R\<^esub> (\<ominus>\<^bsub>R\<^esub> y)"
 
 locale abelian_monoid =
   fixes G (structure)
@@ -728,12 +730,13 @@
 
 subsection {* Morphisms *}
 
-constdefs (structure R S)
+definition
   ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set"
-  "ring_hom R S == {h. h \<in> carrier R -> carrier S &
+  where "ring_hom R S ==
+    {h. h \<in> carrier R -> carrier S &
       (ALL x y. x \<in> carrier R & y \<in> carrier R -->
-        h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y & h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y) &
-      h \<one> = \<one>\<^bsub>S\<^esub>}"
+        h (x \<otimes>\<^bsub>R\<^esub> y) = h x \<otimes>\<^bsub>S\<^esub> h y & h (x \<oplus>\<^bsub>R\<^esub> y) = h x \<oplus>\<^bsub>S\<^esub> h y) &
+      h \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>}"
 
 lemma ring_hom_memI:
   fixes R (structure) and S (structure)