# HG changeset patch
# User haftmann
# Date 1269246748 -3600
# Node ID 76c7374a0fa62bfa7fee6ec74cf8cfaab5164f3c
# Parent  28e73b3e7b6cc70675b4cd57467be4ee2aa93d82# Parent  9d0d545bcb5d5917e33f8f886b25a515f80aa12b
merged

diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/AbelCoset.thy
--- a/src/HOL/Algebra/AbelCoset.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/AbelCoset.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -1,13 +1,11 @@
-(*
-  Title:     HOL/Algebra/AbelCoset.thy
-  Author:    Stephan Hohe, TU Muenchen
+(*  Title:      HOL/Algebra/AbelCoset.thy
+    Author:     Stephan Hohe, TU Muenchen
 *)
 
 theory AbelCoset
 imports Coset Ring
 begin
 
-
 subsection {* More Lifting from Groups to Abelian Groups *}
 
 subsubsection {* Definitions *}
@@ -17,36 +15,41 @@
 
 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 = 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 = 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 = 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 = 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 = 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 = 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
+definition
+  A_FactGroup :: "[('a,'b) ring_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "A'_Mod" 65)
     --{*Actually defined for groups rather than monoids*}
-  "A_FactGroup G H \<equiv> FactGroup \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
+  where "A_FactGroup G H = FactGroup \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
 
-definition a_kernel :: "('a, 'm) ring_scheme \<Rightarrow> ('b, 'n) ring_scheme \<Rightarrow> 
-             ('a \<Rightarrow> 'b) \<Rightarrow> 'a set" where 
+definition
+  a_kernel :: "('a, 'm) ring_scheme \<Rightarrow> ('b, 'n) ring_scheme \<Rightarrow>  ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
     --{*the kernel of a homomorphism (additive)*}
-  "a_kernel G H h \<equiv> kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
-                              \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
+  where "a_kernel G H h =
+    kernel \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>
+      \<lparr>carrier = carrier H, mult = add H, one = zero H\<rparr> h"
 
 locale abelian_group_hom = G: abelian_group G + H: abelian_group H
     for G (structure) and H (structure) +
@@ -515,6 +518,7 @@
 text {* The isomorphism theorems have been omitted from lifting, at
   least for now *}
 
+
 subsubsection{*The First Isomorphism Theorem*}
 
 text{*The quotient by the kernel of a homomorphism is isomorphic to the 
@@ -524,7 +528,7 @@
   a_kernel_def kernel_def
 
 lemma a_kernel_def':
-  "a_kernel R S h \<equiv> {x \<in> carrier R. h x = \<zero>\<^bsub>S\<^esub>}"
+  "a_kernel R S h = {x \<in> carrier R. h x = \<zero>\<^bsub>S\<^esub>}"
 by (rule a_kernel_def[unfolded kernel_def, simplified ring_record_simps])
 
 
@@ -637,6 +641,7 @@
 by (rule group_hom.FactGroup_iso[OF a_group_hom,
     folded a_kernel_def A_FactGroup_def, simplified ring_record_simps])
 
+
 subsubsection {* Cosets *}
 
 text {* Not eveything from \texttt{CosetExt.thy} is lifted here. *}
@@ -721,7 +726,6 @@
     folded A_RCOSETS_def, simplified monoid_record_simps])
 
 
-
 subsubsection {* Addition of Subgroups *}
 
 lemma (in abelian_monoid) set_add_closed:
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/Bij.thy
--- a/src/HOL/Algebra/Bij.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/Bij.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -2,17 +2,20 @@
     Author:     Florian Kammueller, with new proofs by L C Paulson
 *)
 
-theory Bij imports Group begin
-
+theory Bij
+imports Group
+begin
 
 section {* Bijections of a Set, Permutation and Automorphism Groups *}
 
-definition Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set" where
+definition
+  Bij :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) set"
     --{*Only extensional functions, since otherwise we get too many.*}
-  "Bij S \<equiv> extensional S \<inter> {f. bij_betw f S S}"
+   where "Bij S = extensional S \<inter> {f. bij_betw f S S}"
 
-definition BijGroup :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) monoid" where
-  "BijGroup S \<equiv>
+definition
+  BijGroup :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a) monoid"
+  where "BijGroup S =
     \<lparr>carrier = Bij S,
      mult = \<lambda>g \<in> Bij S. \<lambda>f \<in> Bij S. compose S g f,
      one = \<lambda>x \<in> S. x\<rparr>"
@@ -69,11 +72,13 @@
 done
 
 
-definition auto :: "('a, 'b) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) set" where
-  "auto G \<equiv> hom G G \<inter> Bij (carrier G)"
+definition
+  auto :: "('a, 'b) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) set"
+  where "auto G = hom G G \<inter> Bij (carrier G)"
 
-definition AutoGroup :: "('a, 'c) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) monoid" where
-  "AutoGroup G \<equiv> BijGroup (carrier G) \<lparr>carrier := auto G\<rparr>"
+definition
+  AutoGroup :: "('a, 'c) monoid_scheme \<Rightarrow> ('a \<Rightarrow> 'a) monoid"
+  where "AutoGroup G = BijGroup (carrier G) \<lparr>carrier := auto G\<rparr>"
 
 lemma (in group) id_in_auto: "(\<lambda>x \<in> carrier G. x) \<in> auto G"
   by (simp add: auto_def hom_def restrictI group.axioms id_Bij)
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/Congruence.thy
--- a/src/HOL/Algebra/Congruence.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/Congruence.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -1,10 +1,11 @@
-(*
-  Title:  Algebra/Congruence.thy
-  Author: Clemens Ballarin, started 3 January 2008
-  Copyright: Clemens Ballarin
+(*  Title:      Algebra/Congruence.thy
+    Author:     Clemens Ballarin, started 3 January 2008
+    Copyright:  Clemens Ballarin
 *)
 
-theory Congruence imports Main begin
+theory Congruence
+imports Main
+begin
 
 section {* Objects *}
 
@@ -19,21 +20,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 \<longleftrightarrow> (\<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 \<longleftrightarrow> ((\<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 \<longleftrightarrow> 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 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/Coset.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -1,28 +1,34 @@
 (*  Title:      HOL/Algebra/Coset.thy
-    Author:     Florian Kammueller, with new proofs by L C Paulson, and
-                Stephan Hohe
+    Author:     Florian Kammueller
+    Author:     L C Paulson
+    Author:     Stephan Hohe
 *)
 
-theory Coset imports Group begin
-
+theory Coset
+imports Group
+begin
 
 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 = (\<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 = (\<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 = (\<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 = (\<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 = (\<Union>h\<in>H. {inv\<^bsub>G\<^esub> h})"
 
 
 locale normal = subgroup + group +
@@ -589,10 +595,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 = {(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:
@@ -650,6 +655,7 @@
   show ?thesis by (force simp add: r_congruent_def l_coset_def m_assoc [symmetric] a ) 
 qed
 
+
 subsubsection{*Two Distinct Right Cosets are Disjoint*}
 
 lemma (in group) rcos_equation:
@@ -675,6 +681,7 @@
     done
 qed
 
+
 subsection {* Further lemmas for @{text "r_congruent"} *}
 
 text {* The relation is a congruence *}
@@ -751,8 +758,9 @@
 
 subsection {*Order of a Group and Lagrange's Theorem*}
 
-definition order :: "('a, 'b) monoid_scheme \<Rightarrow> nat" where
-  "order S \<equiv> card (carrier S)"
+definition
+  order :: "('a, 'b) monoid_scheme \<Rightarrow> nat"
+  where "order S = card (carrier S)"
 
 lemma (in group) rcosets_part_G:
   assumes "subgroup H G"
@@ -821,10 +829,10 @@
 
 subsection {*Quotient Groups: Factorization of a Group*}
 
-definition FactGroup :: "[('a,'b) monoid_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "Mod" 65) where
+definition
+  FactGroup :: "[('a,'b) monoid_scheme, 'a set] \<Rightarrow> ('a set) monoid" (infixl "Mod" 65)
     --{*Actually defined for groups rather than monoids*}
-  "FactGroup G H \<equiv>
-    \<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
+   where "FactGroup G H = \<lparr>carrier = rcosets\<^bsub>G\<^esub> H, mult = set_mult G, one = H\<rparr>"
 
 lemma (in normal) setmult_closed:
      "\<lbrakk>K1 \<in> rcosets H; K2 \<in> rcosets H\<rbrakk> \<Longrightarrow> K1 <#> K2 \<in> rcosets H"
@@ -887,10 +895,10 @@
 text{*The quotient by the kernel of a homomorphism is isomorphic to the 
   range of that homomorphism.*}
 
-definition kernel :: "('a, 'm) monoid_scheme \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow> 
-             ('a \<Rightarrow> 'b) \<Rightarrow> 'a set" where 
+definition
+  kernel :: "('a, 'm) monoid_scheme \<Rightarrow> ('b, 'n) monoid_scheme \<Rightarrow>  ('a \<Rightarrow> 'b) \<Rightarrow> 'a set"
     --{*the kernel of a homomorphism*}
-  "kernel G H h \<equiv> {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}"
+  where "kernel G H h = {x. x \<in> carrier G & h x = \<one>\<^bsub>H\<^esub>}"
 
 lemma (in group_hom) subgroup_kernel: "subgroup (kernel G H h) G"
 apply (rule subgroup.intro) 
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -1,6 +1,5 @@
-(*
-  Title:     Divisibility in monoids and rings
-  Author:    Clemens Ballarin, started 18 July 2008
+(*  Title:      Divisibility in monoids and rings
+    Author:     Clemens Ballarin, started 18 July 2008
 
 Based on work by Stephan Hohe.
 *)
@@ -156,34 +155,35 @@
       show "a \<in> Units G" by (simp add: Units_def, fast)
 qed
 
+
 subsection {* Divisibility and Association *}
 
 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 \<longleftrightarrow> (\<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 \<longleftrightarrow> 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 \<longleftrightarrow> 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 \<longleftrightarrow> 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 \<longleftrightarrow>
+    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 \<longleftrightarrow> (\<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 \<longleftrightarrow> (\<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 \<longleftrightarrow> (\<exists>fs1'. fs1 <~~> fs1' \<and> fs1' [\<sim>]\<^bsub>G\<^esub> fs2)"
 
 
 locale factorial_monoid = comm_monoid_cancel +
@@ -1901,8 +1902,8 @@
 abbreviation
   "assocs G x == eq_closure_of (division_rel G) {x}"
 
-constdefs (structure G)
-  "fmset G as \<equiv> multiset_of (map (\<lambda>a. assocs G a) as)"
+definition
+  "fmset G as = multiset_of (map (\<lambda>a. assocs G a) as)"
 
 
 text {* Helper lemmas *}
@@ -2615,24 +2616,26 @@
 
 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 \<longleftrightarrow> 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 \<longleftrightarrow> 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)
-  "SomeGcd G A == inf (division_rel G) A"
+  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"
 
 
 locale gcd_condition_monoid = comm_monoid_cancel +
@@ -3630,9 +3633,10 @@
 
 text {* Number of factors for wellfoundedness *}
 
-definition factorcount :: "_ \<Rightarrow> 'a \<Rightarrow> nat" where
-  "factorcount G a == THE c. (ALL as. set as \<subseteq> carrier G \<and> 
-                                      wfactors G as a \<longrightarrow> c = length as)"
+definition
+  factorcount :: "_ \<Rightarrow> 'a \<Rightarrow> nat" where
+  "factorcount G a =
+    (THE c. (ALL as. set as \<subseteq> carrier G \<and> wfactors G as a \<longrightarrow> c = length as))"
 
 lemma (in monoid) ee_length:
   assumes ee: "essentially_equal G as bs"
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/Exponent.thy
--- a/src/HOL/Algebra/Exponent.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/Exponent.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -1,7 +1,8 @@
 (*  Title:      HOL/Algebra/Exponent.thy
-    Author:     Florian Kammueller, with new proofs by L C Paulson
+    Author:     Florian Kammueller
+    Author:     L C Paulson
 
-    exponent p s   yields the greatest power of p that divides s.
+exponent p s   yields the greatest power of p that divides s.
 *)
 
 theory Exponent
@@ -12,8 +13,9 @@
 
 subsection {*The Combinatorial Argument Underlying the First Sylow Theorem*}
 
-definition exponent :: "nat => nat => nat" where
-"exponent p s == if prime p then (GREATEST r. p^r dvd s) else 0"
+definition
+  exponent :: "nat => nat => nat"
+  where "exponent p s = (if prime p then (GREATEST r. p^r dvd s) else 0)"
 
 
 text{*Prime Theorems*}
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -4,8 +4,9 @@
 This file is largely based on HOL/Finite_Set.thy.
 *)
 
-theory FiniteProduct imports Group begin
-
+theory FiniteProduct
+imports Group
+begin
 
 subsection {* Product Operator for Commutative Monoids *}
 
@@ -26,8 +27,9 @@
 
 inductive_cases empty_foldSetDE [elim!]: "({}, x) \<in> foldSetD D f e"
 
-definition foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a" where
-  "foldD D f e A == THE x. (A, x) \<in> foldSetD D f e"
+definition
+  foldD :: "['a set, 'b => 'a => 'a, 'a, 'b set] => 'a"
+  where "foldD D f e A = (THE x. (A, x) \<in> foldSetD D f e)"
 
 lemma foldSetD_closed:
   "[| (A, z) \<in> foldSetD D f e ; e \<in> D; !!x y. [| x \<in> A; y \<in> D |] ==> f x y \<in> D 
@@ -285,11 +287,12 @@
 
 subsubsection {* Products over Finite Sets *}
 
-constdefs (structure G)
+definition
   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"
+  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 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/Group.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -1,6 +1,5 @@
-(*
-  Title:  HOL/Algebra/Group.thy
-  Author: Clemens Ballarin, started 4 February 2003
+(*  Title:      HOL/Algebra/Group.thy
+    Author:     Clemens Ballarin, started 4 February 2003
 
 Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
 *)
@@ -9,7 +8,6 @@
 imports Lattice FuncSet
 begin
 
-
 section {* Monoids and Groups *}
 
 subsection {* Definitions *}
@@ -22,22 +20,29 @@
   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)
+  pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a"  (infixr "'(^')\<index>" 75)
+
+overloading nat_pow == "pow :: [_, 'a, nat] => 'a"
+begin
+  definition "nat_pow G a n = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n"
+end
 
-defs (overloaded)
-  nat_pow_def: "pow G a n == nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n"
-  int_pow_def: "pow G a z ==
-    let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
-    in if neg z then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z)"
+overloading int_pow == "pow :: [_, 'a, int] => 'a"
+begin
+  definition "int_pow G a z =
+   (let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
+    in if neg z then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z))"
+end
 
 locale monoid =
   fixes G (structure)
@@ -478,10 +483,12 @@
 
 subsection {* Direct Products *}
 
-definition DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid" (infixr "\<times>\<times>" 80) where
-  "G \<times>\<times> H \<equiv> \<lparr>carrier = carrier G \<times> carrier H,
-                mult = (\<lambda>(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')),
-                one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)\<rparr>"
+definition
+  DirProd :: "_ \<Rightarrow> _ \<Rightarrow> ('a \<times> 'b) monoid" (infixr "\<times>\<times>" 80) where
+  "G \<times>\<times> H =
+    \<lparr>carrier = carrier G \<times> carrier H,
+     mult = (\<lambda>(g, h) (g', h'). (g \<otimes>\<^bsub>G\<^esub> g', h \<otimes>\<^bsub>H\<^esub> h')),
+     one = (\<one>\<^bsub>G\<^esub>, \<one>\<^bsub>H\<^esub>)\<rparr>"
 
 lemma DirProd_monoid:
   assumes "monoid G" and "monoid H"
@@ -534,9 +541,9 @@
 
 subsection {* Homomorphisms and Isomorphisms *}
 
-constdefs (structure G and H)
-  hom :: "_ => _ => ('a => 'b) set"
-  "hom G H ==
+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)}"
 
@@ -544,8 +551,9 @@
   "[|h \<in> hom G H; i \<in> hom H I|] ==> compose (carrier G) i h \<in> hom G I"
 by (fastsimp simp add: hom_def compose_def)
 
-definition iso :: "_ => _ => ('a => 'b) set" (infixr "\<cong>" 60) where
-  "G \<cong> H == {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
+definition
+  iso :: "_ => _ => ('a => 'b) set" (infixr "\<cong>" 60)
+  where "G \<cong> H = {h. h \<in> hom G H & bij_betw h (carrier G) (carrier H)}"
 
 lemma iso_refl: "(%x. x) \<in> G \<cong> G"
 by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/Ideal.thy
--- a/src/HOL/Algebra/Ideal.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/Ideal.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -1,6 +1,5 @@
-(*
-  Title:     HOL/Algebra/CIdeal.thy
-  Author:    Stephan Hohe, TU Muenchen
+(*  Title:      HOL/Algebra/CIdeal.thy
+    Author:     Stephan Hohe, TU Muenchen
 *)
 
 theory Ideal
@@ -45,11 +44,12 @@
   done
 qed
 
+
 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 = Inter {I. ideal I R \<and> S \<subseteq> I}"
 
 
 subsubsection {* Principal Ideals *}
@@ -71,6 +71,7 @@
   show ?thesis  by (intro principalideal.intro principalideal_axioms.intro) (rule is_ideal, rule generate)
 qed
 
+
 subsubsection {* Maximal Ideals *}
 
 locale maximalideal = ideal +
@@ -93,6 +94,7 @@
     (rule is_ideal, rule I_notcarr, rule I_maximal)
 qed
 
+
 subsubsection {* Prime Ideals *}
 
 locale primeideal = ideal + cring +
@@ -139,6 +141,7 @@
     done
 qed
 
+
 subsection {* Special Ideals *}
 
 lemma (in ring) zeroideal:
@@ -451,9 +454,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 = {x \<otimes>\<^bsub>R\<^esub> a | x. x \<in> carrier R}"
 
 text {* genhideal (?) really generates an ideal *}
 lemma (in cring) cgenideal_ideal:
@@ -867,6 +870,7 @@
   qed
 qed
 
+
 subsection {* Derived Theorems *}
 
 --"A non-zero cring that has only the two trivial ideals is a field"
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/IntRing.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -1,13 +1,11 @@
-(*
-  Title:     HOL/Algebra/IntRing.thy
-  Author:    Stephan Hohe, TU Muenchen
+(*  Title:      HOL/Algebra/IntRing.thy
+    Author:     Stephan Hohe, TU Muenchen
 *)
 
 theory IntRing
 imports QuotRing Lattice Int "~~/src/HOL/Old_Number_Theory/Primes"
 begin
 
-
 section {* The Ring of Integers *}
 
 subsection {* Some properties of @{typ int} *}
@@ -22,8 +20,9 @@
 
 subsection {* @{text "\<Z>"}: The Set of Integers as Algebraic Structure *}
 
-definition int_ring :: "int ring" ("\<Z>") where
-  "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
+definition
+  int_ring :: "int ring" ("\<Z>") where
+  "int_ring = \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
 
 lemma int_Zcarr [intro!, simp]:
   "k \<in> carrier \<Z>"
@@ -48,6 +47,8 @@
  apply (unfold int_ring_def, simp+)
 done
 *)
+
+
 subsection {* Interpretations *}
 
 text {* Since definitions of derived operations are global, their
@@ -323,8 +324,9 @@
 
 subsection {* Ideals and the Modulus *}
 
-definition ZMod :: "int => int => int set" where
-  "ZMod k r == (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
+definition
+  ZMod :: "int => int => int set"
+  where "ZMod k r = (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
 
 lemmas ZMod_defs =
   ZMod_def genideal_def
@@ -405,8 +407,9 @@
 
 subsection {* Factorization *}
 
-definition ZFact :: "int \<Rightarrow> int set ring" where
-  "ZFact k == \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
+definition
+  ZFact :: "int \<Rightarrow> int set ring"
+  where "ZFact k = \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
 
 lemmas ZFact_defs = ZFact_def FactRing_def
 
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/Lattice.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -1,12 +1,13 @@
-(*
-  Title:     HOL/Algebra/Lattice.thy
-  Author:    Clemens Ballarin, started 7 November 2003
-  Copyright: Clemens Ballarin
+(*  Title:      HOL/Algebra/Lattice.thy
+    Author:     Clemens Ballarin, started 7 November 2003
+    Copyright:  Clemens Ballarin
 
 Most congruence rules by Stephan Hohe.
 *)
 
-theory Lattice imports Congruence begin
+theory Lattice
+imports Congruence
+begin
 
 section {* Orders and Lattices *}
 
@@ -25,9 +26,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 \<longleftrightarrow> x \<sqsubseteq>\<^bsub>L\<^esub> y & x .\<noteq>\<^bsub>L\<^esub> y"
 
 
 subsubsection {* The order relation *}
@@ -102,12 +103,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 +277,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 \<longleftrightarrow> 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 \<longleftrightarrow> 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 +403,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 +987,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 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/Module.thy
--- a/src/HOL/Algebra/Module.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/Module.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -3,8 +3,9 @@
     Copyright:  Clemens Ballarin
 *)
 
-theory Module imports Ring begin
-
+theory Module
+imports Ring
+begin
 
 section {* Modules over an Abelian Group *}
 
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/QuotRing.thy
--- a/src/HOL/Algebra/QuotRing.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/QuotRing.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -1,6 +1,5 @@
-(*
-  Title:     HOL/Algebra/QuotRing.thy
-  Author:    Stephan Hohe
+(*  Title:      HOL/Algebra/QuotRing.thy
+    Author:     Stephan Hohe
 *)
 
 theory QuotRing
@@ -11,10 +10,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 = (\<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 +88,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 =
+    \<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 *}
@@ -181,6 +179,7 @@
 done
 qed
 
+
 subsection {* Factorization over Prime Ideals *}
 
 text {* The quotient ring generated by a prime ideal is a domain *}
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/README.html
--- a/src/HOL/Algebra/README.html	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/README.html	Mon Mar 22 09:32:28 2010 +0100
@@ -1,7 +1,5 @@
 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
 
-<!-- $Id$ -->
-
 <HTML>
 
 <HEAD>
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/ROOT.ML
--- a/src/HOL/Algebra/ROOT.ML	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/ROOT.ML	Mon Mar 22 09:32:28 2010 +0100
@@ -1,7 +1,6 @@
-(*
-    The Isabelle Algebraic Library
-    $Id$
-    Author: Clemens Ballarin, started 24 September 1999
+(*  Author: Clemens Ballarin, started 24 September 1999
+
+The Isabelle Algebraic Library.
 *)
 
 (* Preliminaries from set and number theory *)
@@ -23,8 +22,7 @@
 ];
 
 
-(*** Old development, based on axiomatic type classes.
-     Will be withdrawn in future. ***)
+(*** Old development, based on axiomatic type classes ***)
 
 no_document use_thys [
   "abstract/Abstract",  (*The ring theory*)
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/Ring.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -1,13 +1,12 @@
-(*
-  Title:     The algebraic hierarchy of rings
-  Author:    Clemens Ballarin, started 9 December 1996
-  Copyright: Clemens Ballarin
+(*  Title:      The algebraic hierarchy of rings
+    Author:     Clemens Ballarin, started 9 December 1996
+    Copyright:  Clemens Ballarin
 *)
 
 theory Ring
 imports FiniteProduct
-uses ("ringsimp.ML") begin
-
+uses ("ringsimp.ML")
+begin
 
 section {* The Algebraic Hierarchy of Rings *}
 
@@ -19,12 +18,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)
@@ -198,9 +198,9 @@
   This definition makes it easy to lift lemmas from @{term finprod}.
 *}
 
-definition finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b" where
-  "finsum G f A == finprod (| carrier = carrier G,
-     mult = add G, one = zero G |) f A"
+definition
+  finsum :: "[('b, 'm) ring_scheme, 'a => 'b, 'a set] => 'b" where
+  "finsum G f A = finprod (| carrier = carrier G, mult = add G, one = zero G |) f A"
 
 syntax
   "_finsum" :: "index => idt => 'a set => 'b => 'b"
@@ -599,6 +599,7 @@
   from R show ?thesis by algebra
 qed
 
+
 subsubsection {* Sums over Finite Sets *}
 
 lemma (in ring) finsum_ldistr:
@@ -728,12 +729,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)
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/RingHom.thy
--- a/src/HOL/Algebra/RingHom.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/RingHom.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -1,6 +1,5 @@
-(*
-  Title:     HOL/Algebra/RingHom.thy
-  Author:    Stephan Hohe, TU Muenchen
+(*  Title:      HOL/Algebra/RingHom.thy
+    Author:     Stephan Hohe, TU Muenchen
 *)
 
 theory RingHom
@@ -100,6 +99,7 @@
     (rule R.is_cring, rule S.is_cring, rule homh)
 qed
 
+
 subsection {* The Kernel of a Ring Homomorphism *}
 
 --"the kernel of a ring homomorphism is an ideal"
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/Sylow.thy
--- a/src/HOL/Algebra/Sylow.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/Sylow.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -1,9 +1,10 @@
 (*  Title:      HOL/Algebra/Sylow.thy
-    ID:         $Id$
     Author:     Florian Kammueller, with new proofs by L C Paulson
 *)
 
-theory Sylow imports Coset Exponent begin
+theory Sylow
+imports Coset Exponent
+begin
 
 text {*
   See also \cite{Kammueller-Paulson:1999}.
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -1,7 +1,6 @@
-(*
-  Title:     HOL/Algebra/UnivPoly.thy
-  Author:    Clemens Ballarin, started 9 December 1996
-  Copyright: Clemens Ballarin
+(*  Title:      HOL/Algebra/UnivPoly.thy
+    Author:     Clemens Ballarin, started 9 December 1996
+    Copyright:  Clemens Ballarin
 
 Contributions, in particular on long division, by Jesus Aransay.
 *)
@@ -10,7 +9,6 @@
 imports Module RingHom
 begin
 
-
 section {* Univariate Polynomials *}
 
 text {*
@@ -54,11 +52,12 @@
   monom :: "['a, nat] => 'p"
   coeff :: "['p, nat] => 'a"
 
-definition up :: "('a, 'm) ring_scheme => (nat => 'a) set"
-  where up_def: "up R == {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero>\<^bsub>R\<^esub> n f)}"
+definition
+  up :: "('a, 'm) ring_scheme => (nat => 'a) set"
+  where "up R = {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero>\<^bsub>R\<^esub> n f)}"
 
 definition UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
-  where UP_def: "UP R == (|
+  where "UP R = (|
    carrier = up R,
    mult = (%p:up R. %q:up R. %n. \<Oplus>\<^bsub>R\<^esub>i \<in> {..n}. p i \<otimes>\<^bsub>R\<^esub> q (n-i)),
    one = (%i. if i=0 then \<one>\<^bsub>R\<^esub> else \<zero>\<^bsub>R\<^esub>),
@@ -428,7 +427,8 @@
     using l [of "(\<lambda>i. coeff P p i)" "(\<lambda>i. coeff P q i)" "n"] by (simp add: Pi_def m_comm)
 qed (simp_all add: R1 R2)
 
-subsection{*Polynomials over a commutative ring for a commutative ring*}
+
+subsection {*Polynomials over a commutative ring for a commutative ring*}
 
 theorem UP_cring:
   "cring P" using UP_ring unfolding cring_def by (auto intro!: comm_monoidI UP_m_assoc UP_m_comm)
@@ -711,8 +711,9 @@
 
 subsection {* The Degree Function *}
 
-definition deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
-  where "deg R p == LEAST n. bound \<zero>\<^bsub>R\<^esub> n (coeff (UP R) p)"
+definition
+  deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
+  where "deg R p = (LEAST n. bound \<zero>\<^bsub>R\<^esub> n (coeff (UP R) p))"
 
 context UP_ring
 begin
@@ -1173,8 +1174,8 @@
 definition
   eval :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme,
            'a => 'b, 'b, nat => 'a] => 'b"
-  where "eval R S phi s == \<lambda>p \<in> carrier (UP R).
-    \<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i"
+  where "eval R S phi s = (\<lambda>p \<in> carrier (UP R).
+    \<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
 
 context UP
 begin
@@ -1472,6 +1473,7 @@
 lemma lcoeff_nonzero2: assumes p_in_R: "p \<in> carrier P" and p_not_zero: "p \<noteq> \<zero>\<^bsub>P\<^esub>" shows "lcoeff p \<noteq> \<zero>" 
   using lcoeff_nonzero [OF p_not_zero p_in_R] .
 
+
 subsection{*The long division algorithm: some previous facts.*}
 
 lemma coeff_minus [simp]:
@@ -1854,11 +1856,11 @@
   by (auto intro!: UP_pre_univ_prop.intro ring_hom_cring.intro
     ring_hom_cring_axioms.intro UP_cring.intro)
 
-definition  INTEG :: "int ring"
-  where INTEG_def: "INTEG == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
+definition
+  INTEG :: "int ring"
+  where "INTEG = (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
 
-lemma INTEG_cring:
-  "cring INTEG"
+lemma INTEG_cring: "cring INTEG"
   by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
     zadd_zminus_inverse2 zadd_zmult_distrib)
 
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/abstract/Abstract.thy
--- a/src/HOL/Algebra/abstract/Abstract.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/abstract/Abstract.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -1,7 +1,6 @@
-(*
-    Summary theory of the development of abstract algebra
-    $Id$
-    Author: Clemens Ballarin, started 17 July 1997
+(*  Author: Clemens Ballarin, started 17 July 1997
+
+Summary theory of the development of abstract algebra.
 *)
 
 theory Abstract
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/abstract/Factor.thy
--- a/src/HOL/Algebra/abstract/Factor.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/abstract/Factor.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -1,10 +1,11 @@
-(*
-    Factorisation within a factorial domain
-    $Id$
-    Author: Clemens Ballarin, started 25 November 1997
+(*  Author: Clemens Ballarin, started 25 November 1997
+
+Factorisation within a factorial domain.
 *)
 
-theory Factor imports Ring2 begin
+theory Factor
+imports Ring2
+begin
 
 definition
   Factorisation :: "['a::ring, 'a list, 'a] => bool" where
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/abstract/Field.thy
--- a/src/HOL/Algebra/abstract/Field.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/abstract/Field.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -1,9 +1,11 @@
-(*
-    Properties of abstract class field
-    Author: Clemens Ballarin, started 15 November 1997
+(*  Author: Clemens Ballarin, started 15 November 1997
+
+Properties of abstract class field.
 *)
 
-theory Field imports Factor PID begin
+theory Field
+imports Factor PID
+begin
 
 instance field < "domain"
   apply intro_classes
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/abstract/Ideal2.thy
--- a/src/HOL/Algebra/abstract/Ideal2.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/abstract/Ideal2.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -1,9 +1,11 @@
-(*
-    Ideals for commutative rings
-    Author: Clemens Ballarin, started 24 September 1999
+(*  Author: Clemens Ballarin, started 24 September 1999
+
+Ideals for commutative rings.
 *)
 
-theory Ideal2 imports Ring2 begin
+theory Ideal2
+imports Ring2
+begin
 
 definition
   is_ideal :: "('a::ring) set => bool" where
@@ -28,8 +30,8 @@
 (* is_ideal *)
 
 lemma is_idealI:
-  "!! I. [| !! a b. [| a:I; b:I |] ==> a + b : I;  
-      !! a. a:I ==> - a : I; 0 : I;  
+  "!! I. [| !! a b. [| a:I; b:I |] ==> a + b : I;
+      !! a. a:I ==> - a : I; 0 : I;
       !! a r. a:I ==> a * r : I |] ==> is_ideal I"
   unfolding is_ideal_def by blast
 
@@ -241,7 +243,7 @@
   apply force
   done
 
-lemma chain_is_ideal: "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |]  
+lemma chain_is_ideal: "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |]
     ==> is_ideal (Union (I`UNIV))"
   apply (rule is_idealI)
      apply auto
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/abstract/PID.thy
--- a/src/HOL/Algebra/abstract/PID.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/abstract/PID.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -1,9 +1,11 @@
-(*
-    Principle ideal domains
-    Author: Clemens Ballarin, started 5 October 1999
+(*  Author: Clemens Ballarin, started 5 October 1999
+
+Principle ideal domains.
 *)
 
-theory PID imports Ideal2 begin
+theory PID
+imports Ideal2
+begin
 
 instance pid < factorial
   apply intro_classes
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/abstract/Ring2.thy
--- a/src/HOL/Algebra/abstract/Ring2.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/abstract/Ring2.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -30,16 +30,17 @@
   and divide_def:       "a / b = a * inverse b"
 begin
 
-definition assoc :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "assoc" 50) where
-  assoc_def: "a assoc b \<longleftrightarrow> a dvd b & b dvd a"
+definition
+  assoc :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "assoc" 50)
+  where "a assoc b \<longleftrightarrow> a dvd b & b dvd a"
 
-definition irred :: "'a \<Rightarrow> bool" where
-  irred_def: "irred a \<longleftrightarrow> a ~= 0 & ~ a dvd 1
-                          & (ALL d. d dvd a --> d dvd 1 | a dvd d)"
+definition
+  irred :: "'a \<Rightarrow> bool" where
+  "irred a \<longleftrightarrow> a ~= 0 & ~ a dvd 1 & (ALL d. d dvd a --> d dvd 1 | a dvd d)"
 
-definition prime :: "'a \<Rightarrow> bool" where
-  prime_def: "prime p \<longleftrightarrow> p ~= 0 & ~ p dvd 1
-                          & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
+definition
+  prime :: "'a \<Rightarrow> bool" where
+  "prime p \<longleftrightarrow> p ~= 0 & ~ p dvd 1 & (ALL a b. p dvd (a*b) --> p dvd a | p dvd b)"
 
 end
 
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/abstract/RingHomo.thy
--- a/src/HOL/Algebra/abstract/RingHomo.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/abstract/RingHomo.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -1,7 +1,6 @@
-(*
-    Ring homomorphism
-    $Id$
-    Author: Clemens Ballarin, started 15 April 1997
+(*  Author: Clemens Ballarin, started 15 April 1997
+
+Ring homomorphism.
 *)
 
 header {* Ring homomorphism *}
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/document/root.tex
--- a/src/HOL/Algebra/document/root.tex	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/document/root.tex	Mon Mar 22 09:32:28 2010 +0100
@@ -1,5 +1,3 @@
-% $Id$
-
 \documentclass[11pt,a4paper]{article}
 \usepackage{graphicx}
 \usepackage{isabelle,isabellesym}
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/poly/LongDiv.thy
--- a/src/HOL/Algebra/poly/LongDiv.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/poly/LongDiv.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -1,9 +1,11 @@
-(*
-    Experimental theory: long division of polynomials
-    Author: Clemens Ballarin, started 23 June 1999
+(*  Author: Clemens Ballarin, started 23 June 1999
+
+Experimental theory: long division of polynomials.
 *)
 
-theory LongDiv imports PolyHomo begin
+theory LongDiv
+imports PolyHomo
+begin
 
 definition
   lcoeff :: "'a::ring up => 'a" where
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/poly/PolyHomo.thy
--- a/src/HOL/Algebra/poly/PolyHomo.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/poly/PolyHomo.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -1,10 +1,11 @@
-(*
-    Universal property and evaluation homomorphism of univariate polynomials
-    $Id$
-    Author: Clemens Ballarin, started 15 April 1997
+(*  Author: Clemens Ballarin, started 15 April 1997
+
+Universal property and evaluation homomorphism of univariate polynomials.
 *)
 
-theory PolyHomo imports UnivPoly2 begin
+theory PolyHomo
+imports UnivPoly2
+begin
 
 definition
   EVAL2 :: "['a::ring => 'b, 'b, 'a up] => 'b::ring" where
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/poly/Polynomial.thy
--- a/src/HOL/Algebra/poly/Polynomial.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/poly/Polynomial.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -1,7 +1,6 @@
-(*
-    Summary theory of the development of (not instantiated) polynomials
-    $Id$
-    Author: Clemens Ballarin, started 17 July 1997
+(*  Author: Clemens Ballarin, started 17 July 1997
+
+Summary theory of the development of (not instantiated) polynomials.
 *)
 
 theory Polynomial
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Mon Mar 22 09:32:28 2010 +0100
@@ -1,7 +1,6 @@
-(*
-  Title:     Univariate Polynomials
-  Author:    Clemens Ballarin, started 9 December 1996
-  Copyright: Clemens Ballarin
+(*  Title:      Univariate Polynomials
+    Author:     Clemens Ballarin, started 9 December 1996
+    Copyright:  Clemens Ballarin
 *)
 
 header {* Univariate Polynomials *}
@@ -15,6 +14,7 @@
 
 declare strong_setsum_cong [cong]
 
+
 section {* Definition of type up *}
 
 definition
@@ -47,16 +47,16 @@
 section {* Constants *}
 
 definition
-  coeff :: "['a up, nat] => ('a::zero)" where
-  "coeff p n = Rep_UP p n"
+  coeff :: "['a up, nat] => ('a::zero)"
+  where "coeff p n = Rep_UP p n"
 
 definition
-  monom :: "['a::zero, nat] => 'a up"  ("(3_*X^/_)" [71, 71] 70) where
-  "monom a n = Abs_UP (%i. if i=n then a else 0)"
+  monom :: "['a::zero, nat] => 'a up"  ("(3_*X^/_)" [71, 71] 70)
+  where "monom a n = Abs_UP (%i. if i=n then a else 0)"
 
 definition
-  smult :: "['a::{zero, times}, 'a up] => 'a up"  (infixl "*s" 70) where
-  "a *s p = Abs_UP (%i. a * Rep_UP p i)"
+  smult :: "['a::{zero, times}, 'a up] => 'a up"  (infixl "*s" 70)
+  where "a *s p = Abs_UP (%i. a * Rep_UP p i)"
 
 lemma coeff_bound_ex: "EX n. bound n (coeff p)"
 proof -
@@ -132,7 +132,7 @@
 begin
 
 definition
-  up_mult_def:  "p * q = Abs_UP (%n::nat. setsum
+  up_mult_def: "p * q = Abs_UP (%n::nat. setsum
                      (%i. Rep_UP p i * Rep_UP q (n-i)) {..n})"
 
 instance ..
@@ -149,7 +149,7 @@
                      THE x. a * x = 1 else 0)"
 
 definition
-  up_divide_def:  "(a :: 'a up) / b = a * inverse b"
+  up_divide_def: "(a :: 'a up) / b = a * inverse b"
 
 instance ..
 
@@ -479,11 +479,12 @@
   finally show ?thesis .
 qed
 
+
 section {* The degree function *}
 
 definition
-  deg :: "('a::zero) up => nat" where
-  "deg p = (LEAST n. bound n (coeff p))"
+  deg :: "('a::zero) up => nat"
+  where "deg p = (LEAST n. bound n (coeff p))"
 
 lemma deg_aboveI:
   "(!!m. n < m ==> coeff p m = 0) ==> deg p <= n"
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Algebra/ringsimp.ML
--- a/src/HOL/Algebra/ringsimp.ML	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Algebra/ringsimp.ML	Mon Mar 22 09:32:28 2010 +0100
@@ -1,4 +1,4 @@
-(*  Author:    Clemens Ballarin
+(*  Author:     Clemens Ballarin
 
 Normalisation method for locales ring and cring.
 *)
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Boogie/Tools/boogie_loader.ML
--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Mon Mar 22 09:32:28 2010 +0100
@@ -241,7 +241,7 @@
   let val (used, new) = mark_axioms thy (name_axioms axs)
   in
     thy
-    |> PureThy.add_axioms (map (rpair [] o apfst Binding.name) new)
+    |> fold_map (Drule.add_axiom o apfst Binding.name) new
     |-> Context.theory_map o fold Boogie_Axioms.add_thm
     |> log verbose "The following axioms were added:" (map fst new)
     |> (fn thy' => log verbose "The following axioms already existed:"
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Mon Mar 22 09:32:28 2010 +0100
@@ -182,8 +182,8 @@
          val new_defs = map new_def assms
          val (definition, thy') = thy
           |> Sign.add_consts_i [(Binding.name constname, constT, NoSyn)]
-          |> PureThy.add_axioms (map_index
-              (fn (i, t) => ((Binding.name (constname ^ "_def" ^ string_of_int i), t), [])) new_defs)
+          |> fold_map Drule.add_axiom (map_index
+              (fn (i, t) => (Binding.name (constname ^ "_def" ^ string_of_int i), t)) new_defs)
         in
           (lhs, ((full_constname, definition) :: defs, thy'))
         end
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOL/Tools/choice_specification.ML	Mon Mar 22 09:32:28 2010 +0100
@@ -44,9 +44,9 @@
         let
             fun process [] (thy,tm) =
                 let
-                    val (thms, thy') = PureThy.add_axioms [((Binding.name axname, HOLogic.mk_Trueprop tm),[])] thy
+                    val (thm, thy') = Drule.add_axiom (Binding.name axname, HOLogic.mk_Trueprop tm) thy
                 in
-                    (thy',hd thms)
+                    (thy', thm)
                 end
               | process ((thname,cname,covld)::cos) (thy,tm) =
                 case tm of
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/HOLCF/Tools/Domain/domain_axioms.ML
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Mon Mar 22 09:32:28 2010 +0100
@@ -54,13 +54,8 @@
     val abs_iso_bind = Binding.qualified true "abs_iso" dbind;
     val rep_iso_bind = Binding.qualified true "rep_iso" dbind;
 
-    val (abs_iso_thm, thy) =
-        yield_singleton PureThy.add_axioms
-        ((abs_iso_bind, abs_iso_eqn), []) thy;
-
-    val (rep_iso_thm, thy) =
-        yield_singleton PureThy.add_axioms
-        ((rep_iso_bind, rep_iso_eqn), []) thy;
+    val (abs_iso_thm, thy) = Drule.add_axiom (abs_iso_bind, abs_iso_eqn) thy;
+    val (rep_iso_thm, thy) = Drule.add_axiom (rep_iso_bind, rep_iso_eqn) thy;
 
     val result =
         {
@@ -88,9 +83,7 @@
 
     val lub_take_bind = Binding.qualified true "lub_take" dbind;
 
-    val (lub_take_thm, thy) =
-        yield_singleton PureThy.add_axioms
-        ((lub_take_bind, lub_take_eqn), []) thy;
+    val (lub_take_thm, thy) = Drule.add_axiom (lub_take_bind, lub_take_eqn) thy;
   in
     (lub_take_thm, thy)
   end;
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Mon Mar 22 09:32:28 2010 +0100
@@ -14,7 +14,7 @@
   val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
   val print_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
   val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
-  val add_axioms: ((binding * string) * Attrib.src list) list -> theory -> theory
+  val add_axioms: (Attrib.binding * string) list -> theory -> theory
   val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
   val declaration: bool -> Symbol_Pos.text * Position.T -> local_theory -> local_theory
   val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list ->
@@ -164,16 +164,14 @@
   in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false body_pos txt)) end;
 
 
-(* axioms *)
+(* old-style axioms *)
 
-fun add_axms f args thy =
-  f (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute thy) srcs)) args) thy;
+val add_axioms = fold (fn (b, ax) => snd o Specification.axiomatization_cmd [] [(b, [ax])]);
 
-val add_axioms = add_axms (snd oo PureThy.add_axioms_cmd);
-
-fun add_defs ((unchecked, overloaded), args) =
-  add_axms
-    (snd oo (if unchecked then PureThy.add_defs_unchecked_cmd else PureThy.add_defs_cmd) overloaded) args;
+fun add_defs ((unchecked, overloaded), args) thy =
+  thy |> (if unchecked then PureThy.add_defs_unchecked_cmd else PureThy.add_defs_cmd) overloaded
+    (map (fn ((b, ax), srcs) => ((b, ax), map (Attrib.attribute thy) srcs)) args)
+  |> snd;
 
 
 (* declarations *)
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Mon Mar 22 09:32:28 2010 +0100
@@ -178,11 +178,9 @@
 
 (* axioms and definitions *)
 
-val named_spec = SpecParse.thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y));
-
 val _ =
   OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
-    (Scan.repeat1 named_spec >> (Toplevel.theory o IsarCmd.add_axioms));
+    (Scan.repeat1 SpecParse.spec >> (Toplevel.theory o IsarCmd.add_axioms));
 
 val opt_unchecked_overloaded =
   Scan.optional (P.$$$ "(" |-- P.!!!
@@ -191,7 +189,8 @@
 
 val _ =
   OuterSyntax.command "defs" "define constants" K.thy_decl
-    (opt_unchecked_overloaded -- Scan.repeat1 named_spec
+    (opt_unchecked_overloaded --
+      Scan.repeat1 (SpecParse.thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y)))
       >> (Toplevel.theory o IsarCmd.add_defs));
 
 
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/Pure/axclass.ML	Mon Mar 22 09:32:28 2010 +0100
@@ -467,7 +467,7 @@
 
     (* definition *)
 
-    val conjs = map (curry Logic.mk_of_class (Term.aT [])) super @ flat axiomss;
+    val conjs = Logic.mk_of_sort (Term.aT [], super) @ flat axiomss;
     val class_eq =
       Logic.mk_equals (Logic.mk_of_class (Term.aT [], class), Logic.mk_conjunction_balanced conjs);
 
@@ -521,7 +521,7 @@
     val names = name args;
   in
     thy
-    |> PureThy.add_axioms (map (rpair []) (map Binding.name names ~~ specs))
+    |> fold_map Drule.add_axiom (map Binding.name names ~~ specs)
     |-> fold add
   end;
 
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/Pure/drule.ML	Mon Mar 22 09:32:28 2010 +0100
@@ -77,6 +77,7 @@
   val flexflex_unique: thm -> thm
   val export_without_context: thm -> thm
   val export_without_context_open: thm -> thm
+  val add_axiom: (binding * term) -> theory -> thm * theory
   val store_thm: binding -> thm -> thm
   val store_standard_thm: binding -> thm -> thm
   val store_thm_open: binding -> thm -> thm
@@ -320,6 +321,12 @@
   #> Thm.close_derivation;
 
 
+(* old-style axioms *)
+
+fun add_axiom (b, prop) =
+  Thm.add_axiom (b, prop) #-> (fn thm => PureThy.add_thm ((b, export_without_context thm), []));
+
+
 (*Convert all Vars in a theorem to Frees.  Also return a function for
   reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.
   Similar code in type/freeze_thaw*)
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/Pure/logic.ML	Mon Mar 22 09:32:28 2010 +0100
@@ -38,6 +38,7 @@
   val class_of_const: string -> class
   val mk_of_class: typ * class -> term
   val dest_of_class: term -> typ * class
+  val mk_of_sort: typ * sort -> term list
   val name_classrel: string * string -> string
   val mk_classrel: class * class -> term
   val dest_classrel: term -> class * class
@@ -217,7 +218,7 @@
   handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []);
 
 
-(* class membership *)
+(* class/sort membership *)
 
 fun mk_of_class (ty, c) =
   Const (const_of_class c, Term.itselfT ty --> propT) $ mk_type ty;
@@ -225,6 +226,8 @@
 fun dest_of_class (Const (c_class, _) $ ty) = (dest_type ty, class_of_const c_class)
   | dest_of_class t = raise TERM ("dest_of_class", [t]);
 
+fun mk_of_sort (ty, S) = map (fn c => mk_of_class (ty, c)) S;
+
 
 (* class relations *)
 
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/Pure/more_thm.ML	Mon Mar 22 09:32:28 2010 +0100
@@ -322,24 +322,33 @@
 
 (* rules *)
 
+fun stripped_sorts thy t =
+  let
+    val tfrees = rev (map TFree (Term.add_tfrees t []));
+    val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees));
+    val strip = tfrees ~~ tfrees';
+    val recover = map (pairself (Thm.ctyp_of thy o Logic.varifyT_global) o swap) strip;
+    val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t;
+  in (strip, recover, t') end;
+
 fun add_axiom (b, prop) thy =
   let
-    val b' = if Binding.is_empty b then Binding.name ("axiom_" ^ serial_string ()) else b;
-    val thy' = thy |> Theory.add_axioms_i [(b', prop)];
-    val axm = unvarify_global (Thm.axiom thy' (Sign.full_name thy' b'));
-  in (axm, thy') end;
+    val b' = if Binding.is_empty b then Binding.name ("unnamed_axiom_" ^ serial_string ()) else b;
+    val (strip, recover, prop') = stripped_sorts thy prop;
+    val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
+    val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of thy T, S)) strip;
+    val thy' =
+      Theory.add_axiom (b', Logic.list_implies (maps Logic.mk_of_sort constraints, prop')) thy;
+    val axm' = Thm.axiom thy' (Sign.full_name thy' b');
+    val thm = unvarify_global (Thm.instantiate (recover, []) axm') |> fold elim_implies of_sorts;
+  in (thm, thy') end;
 
 fun add_def unchecked overloaded (b, prop) thy =
   let
-    val tfrees = rev (map TFree (Term.add_tfrees prop []));
-    val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees));
-    val strip_sorts = tfrees ~~ tfrees';
-    val recover_sorts = map (pairself (Thm.ctyp_of thy o Logic.varifyT_global)) (tfrees' ~~ tfrees);
-
-    val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop;
+    val (strip, recover, prop') = stripped_sorts thy prop;
     val thy' = Theory.add_defs_i unchecked overloaded [(b, prop')] thy;
     val axm' = Thm.axiom thy' (Sign.full_name thy' b);
-    val thm = unvarify_global (Thm.instantiate (recover_sorts, []) axm');
+    val thm = unvarify_global (Thm.instantiate (recover, []) axm');
   in (thm, thy') end;
 
 
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/Pure/proofterm.ML	Mon Mar 22 09:32:28 2010 +0100
@@ -812,24 +812,24 @@
 val f = Free ("f", aT --> bT);
 val g = Free ("g", aT --> bT);
 
-local open Logic in
-
 val equality_axms =
-  [("reflexive", mk_equals (x, x)),
-   ("symmetric", mk_implies (mk_equals (x, y), mk_equals (y, x))),
-   ("transitive", list_implies ([mk_equals (x, y), mk_equals (y, z)], mk_equals (x, z))),
-   ("equal_intr", list_implies ([mk_implies (A, B), mk_implies (B, A)], mk_equals (A, B))),
-   ("equal_elim", list_implies ([mk_equals (A, B), A], B)),
-   ("abstract_rule", mk_implies
-      (all x (mk_equals (f $ x, g $ x)), mk_equals (lambda x (f $ x), lambda x (g $ x)))),
-   ("combination", list_implies
-      ([mk_equals (f, g), mk_equals (x, y)], mk_equals (f $ x, g $ y)))];
+ [("reflexive", Logic.mk_equals (x, x)),
+  ("symmetric", Logic.mk_implies (Logic.mk_equals (x, y), Logic.mk_equals (y, x))),
+  ("transitive",
+    Logic.list_implies ([Logic.mk_equals (x, y), Logic.mk_equals (y, z)], Logic.mk_equals (x, z))),
+  ("equal_intr",
+    Logic.list_implies ([Logic.mk_implies (A, B), Logic.mk_implies (B, A)], Logic.mk_equals (A, B))),
+  ("equal_elim", Logic.list_implies ([Logic.mk_equals (A, B), A], B)),
+  ("abstract_rule",
+    Logic.mk_implies
+      (Logic.all x
+        (Logic.mk_equals (f $ x, g $ x)), Logic.mk_equals (lambda x (f $ x), lambda x (g $ x)))),
+  ("combination", Logic.list_implies
+    ([Logic.mk_equals (f, g), Logic.mk_equals (x, y)], Logic.mk_equals (f $ x, g $ y)))];
 
 val [reflexive_axm, symmetric_axm, transitive_axm, equal_intr_axm,
   equal_elim_axm, abstract_rule_axm, combination_axm] =
-    map (fn (s, t) => PAxm ("Pure." ^ s, varify_global t, NONE)) equality_axms;
-
-end;
+    map (fn (s, t) => PAxm ("Pure." ^ s, Logic.varify_global t, NONE)) equality_axms;
 
 val reflexive = reflexive_axm % NONE;
 
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/Pure/pure_thy.ML	Mon Mar 22 09:32:28 2010 +0100
@@ -32,8 +32,6 @@
   val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
   val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list
     -> theory -> (string * thm list) list * theory
-  val add_axioms: ((binding * term) * attribute list) list -> theory -> thm list * theory
-  val add_axioms_cmd: ((binding * string) * attribute list) list -> theory -> thm list * theory
   val add_defs: bool -> ((binding * term) * attribute list) list ->
     theory -> thm list * theory
   val add_defs_unchecked: bool -> ((binding * term) * attribute list) list ->
@@ -202,21 +200,16 @@
 (* store axioms as theorems *)
 
 local
-  fun get_ax thy (b, _) = Thm.axiom thy (Sign.full_name thy b);
-  fun get_axs thy named_axs = map (Thm.forall_elim_vars 0 o get_ax thy) named_axs;
-  fun add_axm add = fold_map (fn ((b, ax), atts) => fn thy =>
+  fun add_axm add = fold_map (fn ((b, prop), atts) => fn thy =>
     let
-      val named_ax = [(b, ax)];
-      val thy' = add named_ax thy;
-      val thm = hd (get_axs thy' named_ax);
+      val thy' = add [(b, prop)] thy;
+      val thm = Thm.forall_elim_vars 0 (Thm.axiom thy' (Sign.full_name thy' b));
     in apfst hd (gen_add_thms (K I) [((b, thm), atts)] thy') end);
 in
   val add_defs               = add_axm o Theory.add_defs_i false;
   val add_defs_unchecked     = add_axm o Theory.add_defs_i true;
-  val add_axioms             = add_axm Theory.add_axioms_i;
   val add_defs_cmd           = add_axm o Theory.add_defs false;
   val add_defs_unchecked_cmd = add_axm o Theory.add_defs true;
-  val add_axioms_cmd         = add_axm Theory.add_axioms;
 end;
 
 
@@ -369,6 +362,6 @@
   #> Sign.hide_const false "Pure.sort_constraint"
   #> Sign.hide_const false "Pure.conjunction"
   #> add_thmss [((Binding.name "nothing", []), [])] #> snd
-  #> Theory.add_axioms_i (map (apfst Binding.name) Proofterm.equality_axms)));
+  #> fold (fn (a, prop) => snd o Thm.add_axiom (Binding.name a, prop)) Proofterm.equality_axms));
 
 end;
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/Pure/theory.ML	Mon Mar 22 09:32:28 2010 +0100
@@ -28,8 +28,7 @@
   val at_end: (theory -> theory option) -> theory -> theory
   val begin_theory: string -> theory list -> theory
   val end_theory: theory -> theory
-  val add_axioms_i: (binding * term) list -> theory -> theory
-  val add_axioms: (binding * string) list -> theory -> theory
+  val add_axiom: binding * term -> theory -> theory
   val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
   val add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory
   val add_defs: bool -> bool -> (binding * string) list -> theory -> theory
@@ -171,23 +170,14 @@
     cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b));
 
 
-(* add_axioms(_i) *)
+(* add_axiom *)
 
-local
-
-fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
+fun add_axiom raw_axm thy = thy |> map_axioms (fn axioms =>
   let
-    val axms = map (apsnd Logic.varify_global o prep_axm thy) raw_axms;
-    val axioms' = fold (#2 oo Name_Space.define true (Sign.naming_of thy)) axms axioms;
+    val axm = apsnd Logic.varify_global (cert_axm thy raw_axm);
+    val (_, axioms') = Name_Space.define true (Sign.naming_of thy) axm axioms;
   in axioms' end);
 
-in
-
-val add_axioms_i = gen_add_axioms cert_axm;
-val add_axioms = gen_add_axioms read_axm;
-
-end;
-
 
 
 (** add constant definitions **)
@@ -269,7 +259,7 @@
   let val axms = map (prep_axm thy) raw_axms in
     thy
     |> map_defs (fold (check_def thy unchecked overloaded) axms)
-    |> add_axioms_i axms
+    |> fold add_axiom axms
   end;
 
 in
diff -r 9d0d545bcb5d -r 76c7374a0fa6 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Mar 21 08:46:50 2010 +0100
+++ b/src/Pure/thm.ML	Mon Mar 22 09:32:28 2010 +0100
@@ -1231,7 +1231,7 @@
       raise THM ("unconstrainT: not a type variable", 0, [th]);
     val T' = TVar ((x, i), []);
     val unconstrain = Term.map_types (Term.map_atyps (fn U => if U = T then T' else U));
-    val constraints = map (curry Logic.mk_of_class T') S;
+    val constraints = Logic.mk_of_sort (T', S);
   in
     Thm (deriv_rule0 (Pt.PAxm ("Pure.unconstrainT", prop, SOME [])),
      {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),