# HG changeset patch
# User huffman
# Date 1215666919 -7200
# Node ID 9a5d4a8d4aac0eff19bcd269fb31d52ed7e46a6e
# Parent  13137fcd49aa94c4b23a06c914fb22bb9e5bbf3a
by intro_locales -> ..

diff -r 13137fcd49aa -r 9a5d4a8d4aac src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Thu Jul 10 07:07:54 2008 +0200
+++ b/src/HOL/OrderedGroup.thy	Thu Jul 10 07:15:19 2008 +0200
@@ -487,8 +487,7 @@
   ab_group_add + pordered_ab_semigroup_add
 begin
 
-subclass pordered_cancel_ab_semigroup_add
-  by intro_locales
+subclass pordered_cancel_ab_semigroup_add ..
 
 subclass pordered_ab_semigroup_add_imp_le
 proof unfold_locales
@@ -499,8 +498,7 @@
   thus "a \<le> b" by simp
 qed
 
-subclass pordered_comm_monoid_add
-  by intro_locales
+subclass pordered_comm_monoid_add ..
 
 lemma max_diff_distrib_left:
   shows "max x y - z = max (x - z) (y - z)"
@@ -645,8 +643,7 @@
   linorder + pordered_cancel_ab_semigroup_add
 begin
 
-subclass ordered_ab_semigroup_add
-  by intro_locales
+subclass ordered_ab_semigroup_add ..
 
 subclass pordered_ab_semigroup_add_imp_le
 proof unfold_locales
@@ -673,8 +670,7 @@
   linorder + pordered_ab_group_add
 begin
 
-subclass ordered_cancel_ab_semigroup_add 
-  by intro_locales
+subclass ordered_cancel_ab_semigroup_add ..
 
 lemma neg_less_eq_nonneg:
   "- a \<le> a \<longleftrightarrow> 0 \<le> a"
@@ -963,8 +959,8 @@
 class lordered_ab_group_add = pordered_ab_group_add + lattice
 begin
 
-subclass lordered_ab_group_add_meet by intro_locales
-subclass lordered_ab_group_add_join by intro_locales
+subclass lordered_ab_group_add_meet ..
+subclass lordered_ab_group_add_join ..
 
 lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
 
diff -r 13137fcd49aa -r 9a5d4a8d4aac src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Thu Jul 10 07:07:54 2008 +0200
+++ b/src/HOL/Ring_and_Field.thy	Thu Jul 10 07:15:19 2008 +0200
@@ -80,14 +80,14 @@
 class comm_semiring_0 = comm_semiring + comm_monoid_add + mult_zero
 begin
 
-subclass semiring_0 by intro_locales
+subclass semiring_0 ..
 
 end
 
 class comm_semiring_0_cancel = comm_semiring + comm_monoid_add + cancel_ab_semigroup_add
 begin
 
-subclass semiring_0_cancel by intro_locales
+subclass semiring_0_cancel ..
 
 end
 
@@ -106,7 +106,7 @@
   (*previously almost_semiring*)
 begin
 
-subclass semiring_1 by intro_locales
+subclass semiring_1 ..
 
 end
 
@@ -117,9 +117,9 @@
   + cancel_ab_semigroup_add + monoid_mult
 begin
 
-subclass semiring_0_cancel by intro_locales
+subclass semiring_0_cancel ..
 
-subclass semiring_1 by intro_locales
+subclass semiring_1 ..
 
 end
 
@@ -127,16 +127,16 @@
   + zero_neq_one + cancel_ab_semigroup_add
 begin
 
-subclass semiring_1_cancel by intro_locales
-subclass comm_semiring_0_cancel by intro_locales
-subclass comm_semiring_1 by intro_locales
+subclass semiring_1_cancel ..
+subclass comm_semiring_0_cancel ..
+subclass comm_semiring_1 ..
 
 end
 
 class ring = semiring + ab_group_add
 begin
 
-subclass semiring_0_cancel by intro_locales
+subclass semiring_0_cancel ..
 
 text {* Distribution rules *}
 
@@ -185,15 +185,15 @@
 class comm_ring = comm_semiring + ab_group_add
 begin
 
-subclass ring by intro_locales
-subclass comm_semiring_0 by intro_locales
+subclass ring ..
+subclass comm_semiring_0 ..
 
 end
 
 class ring_1 = ring + zero_neq_one + monoid_mult
 begin
 
-subclass semiring_1_cancel by intro_locales
+subclass semiring_1_cancel ..
 
 end
 
@@ -201,8 +201,8 @@
   (*previously ring*)
 begin
 
-subclass ring_1 by intro_locales
-subclass comm_semiring_1_cancel by intro_locales
+subclass ring_1 ..
+subclass comm_semiring_1_cancel ..
 
 end
 
@@ -263,7 +263,7 @@
 class idom = comm_ring_1 + no_zero_divisors
 begin
 
-subclass ring_1_no_zero_divisors by intro_locales
+subclass ring_1_no_zero_divisors ..
 
 end
 
@@ -394,7 +394,7 @@
   thus "a * inverse a = 1" by (simp only: mult_commute)
 qed
 
-subclass idom by intro_locales
+subclass idom ..
 
 lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b"
 proof
@@ -464,8 +464,8 @@
   + semiring + comm_monoid_add + cancel_ab_semigroup_add
 begin
 
-subclass semiring_0_cancel by intro_locales
-subclass pordered_semiring by intro_locales
+subclass semiring_0_cancel ..
+subclass pordered_semiring ..
 
 lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
   by (drule mult_left_mono [of zero b], auto)
@@ -484,9 +484,9 @@
 class ordered_semiring = semiring + comm_monoid_add + ordered_cancel_ab_semigroup_add + mult_mono
 begin
 
-subclass pordered_cancel_semiring by intro_locales
+subclass pordered_cancel_semiring ..
 
-subclass pordered_comm_monoid_add by intro_locales
+subclass pordered_comm_monoid_add ..
 
 lemma mult_left_less_imp_less:
   "c * a < c * b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a < b"
@@ -503,7 +503,7 @@
   assumes mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
 begin
 
-subclass semiring_0_cancel by intro_locales
+subclass semiring_0_cancel ..
 
 subclass ordered_semiring
 proof unfold_locales
@@ -637,8 +637,8 @@
   + pordered_ab_semigroup_add + mult_mono1
 begin
 
-subclass pordered_comm_semiring by intro_locales
-subclass pordered_cancel_semiring by intro_locales
+subclass pordered_comm_semiring ..
+subclass pordered_cancel_semiring ..
 
 end
 
@@ -668,7 +668,7 @@
 class pordered_ring = ring + pordered_cancel_semiring 
 begin
 
-subclass pordered_ab_group_add by intro_locales
+subclass pordered_ab_group_add ..
 
 lemmas ring_simps = ring_simps group_simps
 
@@ -723,7 +723,7 @@
   + ordered_ab_group_add + abs_if
 begin
 
-subclass pordered_ring by intro_locales
+subclass pordered_ring ..
 
 subclass pordered_ab_group_add_abs
 proof unfold_locales
@@ -744,7 +744,7 @@
   + ordered_ab_group_add + abs_if
 begin
 
-subclass ordered_ring by intro_locales
+subclass ordered_ring ..
 
 lemma mult_strict_left_mono_neg:
   "b < a \<Longrightarrow> c < 0 \<Longrightarrow> c * a < c * b"
@@ -888,8 +888,8 @@
 class pordered_comm_ring = comm_ring + pordered_comm_semiring
 begin
 
-subclass pordered_ring by intro_locales
-subclass pordered_cancel_comm_semiring by intro_locales
+subclass pordered_ring ..
+subclass pordered_cancel_comm_semiring ..
 
 end
 
@@ -925,9 +925,9 @@
   (*previously ordered_ring*)
 begin
 
-subclass ordered_ring_strict by intro_locales
-subclass pordered_comm_ring by intro_locales
-subclass idom by intro_locales
+subclass ordered_ring_strict ..
+subclass pordered_comm_ring ..
+subclass idom ..
 
 subclass ordered_semidom
 proof unfold_locales
@@ -1983,8 +1983,8 @@
 class lordered_ring = pordered_ring + lordered_ab_group_add_abs
 begin
 
-subclass lordered_ab_group_add_meet by intro_locales
-subclass lordered_ab_group_add_join by intro_locales
+subclass lordered_ab_group_add_meet ..
+subclass lordered_ab_group_add_join ..
 
 end