# HG changeset patch
# User haftmann
# Date 1172846601 -3600
# Node ID 378f34b1e38095ed930736adb8a8fa8b8c4a5acc
# Parent  bdf16741d0398c86c9fbf6353911aaecd20968ce
now using "class"

diff -r bdf16741d039 -r 378f34b1e380 src/HOL/FixedPoint.thy
--- a/src/HOL/FixedPoint.thy	Fri Mar 02 15:43:20 2007 +0100
+++ b/src/HOL/FixedPoint.thy	Fri Mar 02 15:43:21 2007 +0100
@@ -28,9 +28,9 @@
   bot :: "'a::order" where
   "bot == Sup {}"
 *)
-axclass comp_lat < order
-  Meet_lower: "x \<in> A \<Longrightarrow> Meet A <= x"
-  Meet_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z <= x) \<Longrightarrow> z <= Meet A"
+class comp_lat = order +
+  assumes Meet_lower: "x \<in> A \<Longrightarrow> Meet A \<sqsubseteq> x"
+  assumes Meet_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> Meet A"
 
 theorem Sup_upper: "(x::'a::comp_lat) \<in> A \<Longrightarrow> x <= Sup A"
   by (auto simp: Sup_def intro: Meet_greatest)
diff -r bdf16741d039 -r 378f34b1e380 src/HOL/Library/Parity.thy
--- a/src/HOL/Library/Parity.thy	Fri Mar 02 15:43:20 2007 +0100
+++ b/src/HOL/Library/Parity.thy	Fri Mar 02 15:43:21 2007 +0100
@@ -9,21 +9,18 @@
 imports Main
 begin
 
-axclass even_odd < type
-
-consts
-  even :: "'a::even_odd => bool"
-
-instance int :: even_odd ..
-instance nat :: even_odd ..
-
-defs (overloaded)
-  even_def: "even (x::int) == x mod 2 = 0"
-  even_nat_def: "even (x::nat) == even (int x)"
+class even_odd =
+  fixes even :: "'a \<Rightarrow> bool"
 
 abbreviation
-  odd :: "'a::even_odd => bool" where
-  "odd x == \<not> even x"
+  odd :: "'a\<Colon>even_odd \<Rightarrow> bool" where
+  "odd x \<equiv> \<not> even x"
+
+instance int :: even_odd
+  even_def: "even x \<equiv> x mod 2 = 0" ..
+
+instance nat :: even_odd
+  even_nat_def: "even x \<equiv> even (int x)" ..
 
 
 subsection {* Even and odd are mutually exclusive *}
diff -r bdf16741d039 -r 378f34b1e380 src/HOL/Library/Quotient.thy
--- a/src/HOL/Library/Quotient.thy	Fri Mar 02 15:43:20 2007 +0100
+++ b/src/HOL/Library/Quotient.thy	Fri Mar 02 15:43:21 2007 +0100
@@ -11,7 +11,7 @@
 
 text {*
  We introduce the notion of quotient types over equivalence relations
- via axiomatic type classes.
+ via type classes.
 *}
 
 subsection {* Equivalence relations and quotient types *}
@@ -21,14 +21,13 @@
  "\<sim> :: 'a => 'a => bool"}.
 *}
 
-axclass eqv \<subseteq> type
-consts
-  eqv :: "('a::eqv) => 'a => bool"    (infixl "\<sim>" 50)
+class eqv =
+  fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<^loc>\<sim>" 50)
 
-axclass equiv \<subseteq> eqv
-  equiv_refl [intro]: "x \<sim> x"
-  equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
-  equiv_sym [sym]: "x \<sim> y ==> y \<sim> x"
+class equiv = eqv +
+  assumes equiv_refl [intro]: "x \<^loc>\<sim> x"
+  assumes equiv_trans [trans]: "x \<^loc>\<sim> y \<Longrightarrow> y \<^loc>\<sim> z \<Longrightarrow> x \<^loc>\<sim> z"
+  assumes equiv_sym [sym]: "x \<^loc>\<sim> y \<Longrightarrow> y \<^loc>\<sim> x"
 
 lemma equiv_not_sym [sym]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))"
 proof -
diff -r bdf16741d039 -r 378f34b1e380 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Fri Mar 02 15:43:20 2007 +0100
+++ b/src/HOL/OrderedGroup.thy	Fri Mar 02 15:43:21 2007 +0100
@@ -25,73 +25,71 @@
 *}
 
 subsection {* Semigroups, Groups *}
- 
-axclass semigroup_add \<subseteq> plus
-  add_assoc: "(a + b) + c = a + (b + c)"
 
-axclass ab_semigroup_add \<subseteq> semigroup_add
-  add_commute: "a + b = b + a"
+class semigroup_add = plus +
+  assumes add_assoc: "(a \<^loc>+ b) \<^loc>+ c = a \<^loc>+ (b \<^loc>+ c)"
+
+class ab_semigroup_add = semigroup_add +
+  assumes add_commute: "a \<^loc>+ b = b \<^loc>+ a"
 
 lemma add_left_commute: "a + (b + c) = b + (a + (c::'a::ab_semigroup_add))"
   by (rule mk_left_commute [of "op +", OF add_assoc add_commute])
 
 theorems add_ac = add_assoc add_commute add_left_commute
 
-axclass semigroup_mult \<subseteq> times
-  mult_assoc: "(a * b) * c = a * (b * c)"
+class semigroup_mult = times +
+  assumes mult_assoc: "(a \<^loc>* b) \<^loc>* c = a \<^loc>* (b \<^loc>* c)"
 
-axclass ab_semigroup_mult \<subseteq> semigroup_mult
-  mult_commute: "a * b = b * a"
+class ab_semigroup_mult = semigroup_mult +
+  assumes mult_commute: "a \<^loc>* b = b \<^loc>* a"
 
 lemma mult_left_commute: "a * (b * c) = b * (a * (c::'a::ab_semigroup_mult))"
   by (rule mk_left_commute [of "op *", OF mult_assoc mult_commute])
 
 theorems mult_ac = mult_assoc mult_commute mult_left_commute
 
-axclass comm_monoid_add \<subseteq> zero, ab_semigroup_add
-  add_0[simp]: "0 + a = a"
+class comm_monoid_add = zero + ab_semigroup_add +
+  assumes add_0 [simp]: "\<^loc>0 \<^loc>+ a = a"
 
-axclass monoid_mult \<subseteq> one, semigroup_mult
-  mult_1_left[simp]: "1 * a  = a"
-  mult_1_right[simp]: "a * 1 = a"
+class monoid_mult = one + semigroup_mult +
+  assumes mult_1_left [simp]: "\<^loc>1 \<^loc>* a  = a"
+  assumes mult_1_right [simp]: "a \<^loc>* \<^loc>1 = a"
 
-axclass comm_monoid_mult \<subseteq> one, ab_semigroup_mult
-  mult_1: "1 * a = a"
+class comm_monoid_mult = one + ab_semigroup_mult +
+  assumes mult_1: "\<^loc>1 \<^loc>* a = a"
 
 instance comm_monoid_mult \<subseteq> monoid_mult
-by (intro_classes, insert mult_1, simp_all add: mult_commute, auto)
+  by intro_classes (insert mult_1, simp_all add: mult_commute, auto)
 
-axclass cancel_semigroup_add \<subseteq> semigroup_add
-  add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
-  add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c"
+class cancel_semigroup_add = semigroup_add +
+  assumes add_left_imp_eq: "a \<^loc>+ b = a \<^loc>+ c \<Longrightarrow> b = c"
+  assumes add_right_imp_eq: "b \<^loc>+ a = c \<^loc>+ a \<Longrightarrow> b = c"
 
-axclass cancel_ab_semigroup_add \<subseteq> ab_semigroup_add
-  add_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
+class cancel_ab_semigroup_add = ab_semigroup_add +
+  assumes add_imp_eq: "a \<^loc>+ b = a \<^loc>+ c \<Longrightarrow> b = c"
 
 instance cancel_ab_semigroup_add \<subseteq> cancel_semigroup_add
-proof
-  {
-    fix a b c :: 'a
-    assume "a + b = a + c"
-    thus "b = c" by (rule add_imp_eq)
-  }
-  note f = this
+proof intro_classes
+  fix a b c :: 'a
+  assume "a + b = a + c" 
+  then show "b = c" by (rule add_imp_eq)
+next
   fix a b c :: 'a
   assume "b + a = c + a"
-  hence "a + b = a + c" by (simp only: add_commute)
-  thus "b = c" by (rule f)
+  then have "a + b = a + c" by (simp only: add_commute)
+  then show "b = c" by (rule add_imp_eq)
 qed
 
-axclass ab_group_add \<subseteq> minus, comm_monoid_add
-  left_minus[simp]: " - a + a = 0"
-  diff_minus: "a - b = a + (-b)"
+class ab_group_add = minus + comm_monoid_add +
+  assumes left_minus [simp]: "uminus a \<^loc>+ a = \<^loc>0"
+  assumes diff_minus: "a \<^loc>- b = a \<^loc>+ (uminus b)"
 
 instance ab_group_add \<subseteq> cancel_ab_semigroup_add
-proof 
+proof intro_classes
   fix a b c :: 'a
   assume "a + b = a + c"
-  hence "-a + a + b = -a + a + c" by (simp only: add_assoc)
-  thus "b = c" by simp 
+  then have "uminus a + a + b = uminus a + a + c" unfolding add_assoc by simp
+  then show "b = c" by simp 
 qed
 
 lemma add_0_right [simp]: "a + 0 = (a::'a::comm_monoid_add)"
@@ -105,11 +103,11 @@
   and add_zero_right = add_0_right
 
 lemma add_left_cancel [simp]:
-     "(a + b = a + c) = (b = (c::'a::cancel_semigroup_add))"
-by (blast dest: add_left_imp_eq) 
+  "a + b = a + c \<longleftrightarrow> b = (c \<Colon> 'a\<Colon>cancel_semigroup_add)"
+  by (blast dest: add_left_imp_eq) 
 
 lemma add_right_cancel [simp]:
-     "(b + a = c + a) = (b = (c::'a::cancel_semigroup_add))"
+  "b + a = c + a \<longleftrightarrow> b = (c \<Colon> 'a\<Colon>cancel_semigroup_add)"
   by (blast dest: add_right_imp_eq)
 
 lemma right_minus [simp]: "a + -(a::'a::ab_group_add) = 0"
@@ -196,17 +194,18 @@
 
 subsection {* (Partially) Ordered Groups *} 
 
-axclass pordered_ab_semigroup_add \<subseteq> order, ab_semigroup_add
-  add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b"
+class pordered_ab_semigroup_add = order + ab_semigroup_add +
+  assumes add_left_mono: "a \<sqsubseteq> b \<Longrightarrow> c \<^loc>+ a \<sqsubseteq> c \<^loc>+ b"
 
-axclass pordered_cancel_ab_semigroup_add \<subseteq> pordered_ab_semigroup_add, cancel_ab_semigroup_add
+class pordered_cancel_ab_semigroup_add =
+  pordered_ab_semigroup_add + cancel_ab_semigroup_add
 
 instance pordered_cancel_ab_semigroup_add \<subseteq> pordered_ab_semigroup_add ..
 
-axclass pordered_ab_semigroup_add_imp_le \<subseteq> pordered_cancel_ab_semigroup_add
-  add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b"
+class pordered_ab_semigroup_add_imp_le = pordered_cancel_ab_semigroup_add +
+  assumes add_le_imp_le_left: "c \<^loc>+ a \<sqsubseteq> c + b \<Longrightarrow> a \<sqsubseteq> b"
 
-axclass pordered_ab_group_add \<subseteq> ab_group_add, pordered_ab_semigroup_add
+class pordered_ab_group_add = ab_group_add + pordered_ab_semigroup_add
 
 instance pordered_ab_group_add \<subseteq> pordered_ab_semigroup_add_imp_le
 proof
@@ -217,7 +216,7 @@
   thus "a \<le> b" by simp
 qed
 
-axclass ordered_cancel_ab_semigroup_add \<subseteq> pordered_cancel_ab_semigroup_add, linorder
+class ordered_cancel_ab_semigroup_add = pordered_cancel_ab_semigroup_add + linorder
 
 instance ordered_cancel_ab_semigroup_add \<subseteq> pordered_ab_semigroup_add_imp_le
 proof
@@ -239,7 +238,7 @@
 qed
 
 lemma add_right_mono: "a \<le> (b::'a::pordered_ab_semigroup_add) ==> a + c \<le> b + c"
-by (simp add: add_commute[of _ c] add_left_mono)
+  by (simp add: add_commute [of _ c] add_left_mono)
 
 text {* non-strict, in both arguments *}
 lemma add_mono:
diff -r bdf16741d039 -r 378f34b1e380 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Fri Mar 02 15:43:20 2007 +0100
+++ b/src/HOL/Power.thy	Fri Mar 02 15:43:21 2007 +0100
@@ -13,9 +13,9 @@
 
 subsection{*Powers for Arbitrary Monoids*}
 
-axclass recpower \<subseteq> monoid_mult, power
-  power_0 [simp]: "a ^ 0       = 1"
-  power_Suc:      "a ^ (Suc n) = a * (a ^ n)"
+class recpower = monoid_mult + power +
+  assumes power_0 [simp]: "a \<^loc>^ 0       = \<^loc>1"
+  assumes power_Suc:      "a \<^loc>^ Suc n = a \<^loc>* (a \<^loc>^ n)"
 
 lemma power_0_Suc [simp]: "(0::'a::{recpower,semiring_0}) ^ (Suc n) = 0"
 by (simp add: power_Suc)
diff -r bdf16741d039 -r 378f34b1e380 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Fri Mar 02 15:43:20 2007 +0100
+++ b/src/HOL/Ring_and_Field.thy	Fri Mar 02 15:43:21 2007 +0100
@@ -23,17 +23,17 @@
   \end{itemize}
 *}
 
-axclass semiring \<subseteq> ab_semigroup_add, semigroup_mult
-  left_distrib: "(a + b) * c = a * c + b * c"
-  right_distrib: "a * (b + c) = a * b + a * c"
+class semiring = ab_semigroup_add + semigroup_mult +
+  assumes left_distrib: "(a \<^loc>+ b) \<^loc>* c = a \<^loc>* c \<^loc>+ b \<^loc>* c"
+  assumes right_distrib: "a \<^loc>* (b \<^loc>+ c) = a \<^loc>* b \<^loc>+ a \<^loc>* c"
 
-axclass mult_zero \<subseteq> times, zero
-  mult_zero_left [simp]: "0 * a = 0"
-  mult_zero_right [simp]: "a * 0 = 0"
+class mult_zero = times + zero +
+  assumes mult_zero_left [simp]: "\<^loc>0 \<^loc>* a = \<^loc>0"
+  assumes mult_zero_right [simp]: "a \<^loc>* \<^loc>0 = \<^loc>0"
 
-axclass semiring_0 \<subseteq> semiring, comm_monoid_add, mult_zero
+class semiring_0 = semiring + comm_monoid_add + mult_zero
 
-axclass semiring_0_cancel \<subseteq> semiring, comm_monoid_add, cancel_ab_semigroup_add
+class semiring_0_cancel = semiring + comm_monoid_add + cancel_ab_semigroup_add
 
 instance semiring_0_cancel \<subseteq> semiring_0
 proof
@@ -49,8 +49,8 @@
     by (simp only: add_left_cancel)
 qed
 
-axclass comm_semiring \<subseteq> ab_semigroup_add, ab_semigroup_mult  
-  distrib: "(a + b) * c = a * c + b * c"
+class comm_semiring = ab_semigroup_add + ab_semigroup_mult +
+  assumes distrib: "(a \<^loc>+ b) \<^loc>* c = a \<^loc>* c \<^loc>+ b \<^loc>* c"
 
 instance comm_semiring \<subseteq> semiring
 proof
@@ -62,37 +62,38 @@
   finally show "a * (b + c) = a * b + a * c" by blast
 qed
 
-axclass comm_semiring_0 \<subseteq> comm_semiring, comm_monoid_add, mult_zero
+class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero
 
 instance comm_semiring_0 \<subseteq> semiring_0 ..
 
-axclass comm_semiring_0_cancel \<subseteq> comm_semiring, comm_monoid_add, cancel_ab_semigroup_add
+class comm_semiring_0_cancel = comm_semiring + comm_monoid_add + cancel_ab_semigroup_add
 
 instance comm_semiring_0_cancel \<subseteq> semiring_0_cancel ..
 
 instance comm_semiring_0_cancel \<subseteq> comm_semiring_0 ..
 
-axclass zero_neq_one \<subseteq> zero, one
-  zero_neq_one [simp]: "0 \<noteq> 1"
+class zero_neq_one = zero + one +
+  assumes zero_neq_one [simp]: "\<^loc>0 \<noteq> \<^loc>1"
 
-axclass semiring_1 \<subseteq> zero_neq_one, semiring_0, monoid_mult
+class semiring_1 = zero_neq_one + semiring_0 + monoid_mult
 
-axclass comm_semiring_1 \<subseteq> zero_neq_one, comm_semiring_0, comm_monoid_mult (* previously almost_semiring *)
+class comm_semiring_1 = zero_neq_one + comm_semiring_0 + comm_monoid_mult
+  (*previously almost_semiring*)
 
 instance comm_semiring_1 \<subseteq> semiring_1 ..
 
-axclass no_zero_divisors \<subseteq> zero, times
-  no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
+class no_zero_divisors = zero + times +
+  assumes no_zero_divisors: "a \<noteq> \<^loc>0 \<Longrightarrow> b \<noteq> \<^loc>0 \<Longrightarrow> a \<^loc>* b \<noteq> \<^loc>0"
 
-axclass semiring_1_cancel \<subseteq> semiring, comm_monoid_add, zero_neq_one, cancel_ab_semigroup_add, monoid_mult
+class semiring_1_cancel = semiring + comm_monoid_add + zero_neq_one
+  + cancel_ab_semigroup_add + monoid_mult
 
 instance semiring_1_cancel \<subseteq> semiring_0_cancel ..
 
 instance semiring_1_cancel \<subseteq> semiring_1 ..
 
-axclass comm_semiring_1_cancel \<subseteq> 
-  comm_semiring, comm_monoid_add, comm_monoid_mult,
-  zero_neq_one, cancel_ab_semigroup_add
+class comm_semiring_1_cancel = comm_semiring + comm_monoid_add + comm_monoid_mult
+  + zero_neq_one + cancel_ab_semigroup_add
 
 instance comm_semiring_1_cancel \<subseteq> semiring_1_cancel ..
 
@@ -100,38 +101,40 @@
 
 instance comm_semiring_1_cancel \<subseteq> comm_semiring_1 ..
 
-axclass ring \<subseteq> semiring, ab_group_add
+class ring = semiring + ab_group_add
 
 instance ring \<subseteq> semiring_0_cancel ..
 
-axclass comm_ring \<subseteq> comm_semiring, ab_group_add
+class comm_ring = comm_semiring + ab_group_add
 
 instance comm_ring \<subseteq> ring ..
 
 instance comm_ring \<subseteq> comm_semiring_0_cancel ..
 
-axclass ring_1 \<subseteq> ring, zero_neq_one, monoid_mult
+class ring_1 = ring + zero_neq_one + monoid_mult
 
 instance ring_1 \<subseteq> semiring_1_cancel ..
 
-axclass comm_ring_1 \<subseteq> comm_ring, zero_neq_one, comm_monoid_mult (* previously ring *)
+class comm_ring_1 = comm_ring + zero_neq_one + comm_monoid_mult
+  (*previously ring*)
 
 instance comm_ring_1 \<subseteq> ring_1 ..
 
 instance comm_ring_1 \<subseteq> comm_semiring_1_cancel ..
 
-axclass idom \<subseteq> comm_ring_1, no_zero_divisors
+class idom = comm_ring_1 + no_zero_divisors
 
-axclass division_ring \<subseteq> ring_1, inverse
-  left_inverse [simp]:  "a \<noteq> 0 ==> inverse a * a = 1"
-  right_inverse [simp]: "a \<noteq> 0 ==> a * inverse a = 1"
+class division_ring = ring_1 + inverse +
+  assumes left_inverse [simp]:  "a \<noteq> \<^loc>0 \<Longrightarrow> inverse a \<^loc>* a = \<^loc>1"
+  assumes right_inverse [simp]: "a \<noteq> \<^loc>0 \<Longrightarrow> a \<^loc>* inverse a = \<^loc>1"
 
-axclass field \<subseteq> comm_ring_1, inverse
-  field_left_inverse: "a \<noteq> 0 ==> inverse a * a = 1"
-  divide_inverse:     "a / b = a * inverse b"
+class field = comm_ring_1 + inverse +
+  assumes field_left_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a \<^loc>* a = \<^loc>1"
+  assumes divide_inverse:     "a \<^loc>/ b = a \<^loc>* inverse b"
 
 lemma field_right_inverse:
-      assumes not0: "a \<noteq> 0" shows "a * inverse (a::'a::field) = 1"
+  assumes not0: "a \<noteq> 0"
+  shows "a * inverse (a::'a::field) = 1"
 proof -
   have "a * inverse a = inverse a * a" by (rule mult_commute)
   also have "... = 1" using not0 by (rule field_left_inverse)
@@ -156,8 +159,8 @@
 instance field \<subseteq> idom
 by (intro_classes, simp)
 
-axclass division_by_zero \<subseteq> zero, inverse
-  inverse_zero [simp]: "inverse 0 = 0"
+class division_by_zero = zero + inverse +
+  assumes inverse_zero [simp]: "inverse \<^loc>0 = \<^loc>0"
 
 subsection {* Distribution rules *}
 
@@ -192,24 +195,23 @@
 by (simp add: left_distrib diff_minus 
               minus_mult_left [symmetric] minus_mult_right [symmetric]) 
 
-axclass mult_mono \<subseteq> times, zero, ord
-  mult_left_mono: "a <= b \<Longrightarrow> 0 <= c \<Longrightarrow> c * a <= c * b"
-  mult_right_mono: "a <= b \<Longrightarrow> 0 <= c \<Longrightarrow> a * c <= b * c"
+class mult_mono = times + zero + ord +
+  assumes mult_left_mono: "a \<sqsubseteq> b \<Longrightarrow> \<^loc>0 \<sqsubseteq> c \<Longrightarrow> c \<^loc>* a \<sqsubseteq> c \<^loc>* b"
+  assumes mult_right_mono: "a \<sqsubseteq> b \<Longrightarrow> \<^loc>0 \<sqsubseteq> c \<Longrightarrow> a \<^loc>* c \<sqsubseteq> b \<^loc>* c"
 
-axclass pordered_semiring \<subseteq> mult_mono, semiring_0, pordered_ab_semigroup_add 
+class pordered_semiring = mult_mono + semiring_0 + pordered_ab_semigroup_add 
 
-axclass pordered_cancel_semiring \<subseteq> 
-  mult_mono, pordered_ab_semigroup_add,
-  semiring, comm_monoid_add, 
-  pordered_ab_semigroup_add, cancel_ab_semigroup_add
+class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add
+  + semiring + comm_monoid_add + pordered_ab_semigroup_add
+  + cancel_ab_semigroup_add
 
 instance pordered_cancel_semiring \<subseteq> semiring_0_cancel ..
 
 instance pordered_cancel_semiring \<subseteq> pordered_semiring .. 
 
-axclass ordered_semiring_strict \<subseteq> semiring, comm_monoid_add, ordered_cancel_ab_semigroup_add
-  mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
-  mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
+class ordered_semiring_strict = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add +
+  assumes mult_strict_left_mono: "a \<sqsubset> b \<Longrightarrow> \<^loc>0 \<sqsubset> c \<Longrightarrow> c \<^loc>* a \<sqsubset> c \<^loc>* b"
+  assumes mult_strict_right_mono: "a \<sqsubset> b \<Longrightarrow> \<^loc>0 \<sqsubset> c \<Longrightarrow> a \<^loc>* c \<sqsubset> b \<^loc>* c"
 
 instance ordered_semiring_strict \<subseteq> semiring_0_cancel ..
 
@@ -221,18 +223,19 @@
 apply (simp add: mult_strict_right_mono)
 done
 
-axclass mult_mono1 \<subseteq> times, zero, ord
-  mult_mono: "a <= b \<Longrightarrow> 0 <= c \<Longrightarrow> c * a <= c * b"
+class mult_mono1 = times + zero + ord +
+  assumes mult_mono: "a \<sqsubseteq> b \<Longrightarrow> \<^loc>0 \<sqsubseteq> c \<Longrightarrow> c \<^loc>* a \<sqsubseteq> c \<^loc>* b"
 
-axclass pordered_comm_semiring \<subseteq> comm_semiring_0, pordered_ab_semigroup_add, mult_mono1
+class pordered_comm_semiring = comm_semiring_0
+  + pordered_ab_semigroup_add + mult_mono1
 
-axclass pordered_cancel_comm_semiring \<subseteq> 
-  comm_semiring_0_cancel, pordered_ab_semigroup_add, mult_mono1
+class pordered_cancel_comm_semiring = comm_semiring_0_cancel
+  + pordered_ab_semigroup_add + mult_mono1
   
 instance pordered_cancel_comm_semiring \<subseteq> pordered_comm_semiring ..
 
-axclass ordered_comm_semiring_strict \<subseteq> comm_semiring_0, ordered_cancel_ab_semigroup_add
-  mult_strict_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
+class ordered_comm_semiring_strict = comm_semiring_0 + ordered_cancel_ab_semigroup_add +
+  assumes mult_strict_mono: "a \<sqsubset> b \<Longrightarrow> \<^loc>0 \<sqsubset> c \<Longrightarrow> c \<^loc>* a \<sqsubset> c \<^loc>* b"
 
 instance pordered_comm_semiring \<subseteq> pordered_semiring
 proof
@@ -258,7 +261,7 @@
 apply (auto simp add: mult_strict_left_mono order_le_less)
 done
 
-axclass pordered_ring \<subseteq> ring, pordered_cancel_semiring 
+class pordered_ring = ring + pordered_cancel_semiring 
 
 instance pordered_ring \<subseteq> pordered_ab_group_add ..
 
@@ -268,26 +271,28 @@
 
 instance lordered_ring \<subseteq> lordered_ab_group_join ..
 
-axclass abs_if \<subseteq> minus, ord, zero
-  abs_if: "abs a = (if (a < 0) then (-a) else a)"
+class abs_if = minus + ord + zero +
+  assumes abs_if: "abs a = (if a \<sqsubset> 0 then (uminus a) else a)"
 
-axclass ordered_ring_strict \<subseteq> ring, ordered_semiring_strict, abs_if
+class ordered_ring_strict = ring + ordered_semiring_strict + abs_if
 
 instance ordered_ring_strict \<subseteq> lordered_ab_group ..
 
 instance ordered_ring_strict \<subseteq> lordered_ring
-by (intro_classes, simp add: abs_if join_eq_if)
+  by (intro_classes, simp add: abs_if join_eq_if)
 
-axclass pordered_comm_ring \<subseteq> comm_ring, pordered_comm_semiring
+class pordered_comm_ring = comm_ring + pordered_comm_semiring
 
-axclass ordered_semidom \<subseteq> comm_semiring_1_cancel, ordered_comm_semiring_strict (* previously ordered_semiring *)
-  zero_less_one [simp]: "0 < 1"
+class ordered_semidom = comm_semiring_1_cancel + ordered_comm_semiring_strict +
+  (*previously ordered_semiring*)
+  assumes zero_less_one [simp]: "\<^loc>0 \<sqsubset> \<^loc>1"
 
-axclass ordered_idom \<subseteq> comm_ring_1, ordered_comm_semiring_strict, abs_if (* previously ordered_ring *)
+class ordered_idom = comm_ring_1 + ordered_comm_semiring_strict + abs_if
+  (*previously ordered_ring*)
 
 instance ordered_idom \<subseteq> ordered_ring_strict ..
 
-axclass ordered_field \<subseteq> field, ordered_idom
+class ordered_field = field + ordered_idom
 
 lemmas linorder_neqE_ordered_idom =
  linorder_neqE[where 'a = "?'b::ordered_idom"]
diff -r bdf16741d039 -r 378f34b1e380 src/HOL/Wellfounded_Recursion.thy
--- a/src/HOL/Wellfounded_Recursion.thy	Fri Mar 02 15:43:20 2007 +0100
+++ b/src/HOL/Wellfounded_Recursion.thy	Fri Mar 02 15:43:21 2007 +0100
@@ -40,8 +40,8 @@
 abbreviation acyclicP :: "('a => 'a => bool) => bool" where
   "acyclicP r == acyclic (Collect2 r)"
 
-axclass wellorder \<subseteq> linorder
-  wf: "wf {(x,y::'a::ord). x<y}"
+class wellorder = linorder +
+  assumes wf: "wf {(x, y). x \<sqsubset> y}"
 
 
 lemma wfP_wf_eq [pred_set_conv]: "wfP (member2 r) = wf r"