# HG changeset patch
# User ballarin
# Date 1229681349 -3600
# Node ID e190bc2a53992f4e23431e9d4024e2d4b5a0a8f0
# Parent  3adc06d6504f2ef6fba41e309d06293cef2757aa
More porting to new locales

diff -r 3adc06d6504f -r e190bc2a5399 src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Thu Dec 18 20:19:49 2008 +0100
+++ b/src/HOL/Algebra/IntRing.thy	Fri Dec 19 11:09:09 2008 +0100
@@ -328,7 +328,7 @@
 next
   assume "UNIV = {uu. EX x. uu = x * p}"
   from this obtain x 
-      where "1 = x * p" by fast
+      where "1 = x * p" by best
   from this [symmetric]
       have "p * x = 1" by (subst zmult_commute)
   hence "\<bar>p * x\<bar> = 1" by simp
diff -r 3adc06d6504f -r e190bc2a5399 src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Thu Dec 18 20:19:49 2008 +0100
+++ b/src/HOL/Algebra/Lattice.thy	Fri Dec 19 11:09:09 2008 +0100
@@ -919,7 +919,7 @@
 
 text {* Total orders are lattices. *}
 
-sublocale weak_total_order < weak_lattice
+sublocale weak_total_order < weak: weak_lattice
 proof
   fix x y
   assume L: "x \<in> carrier L"  "y \<in> carrier L"
@@ -1125,14 +1125,14 @@
   assumes sup_of_two_exists:
     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
 
-sublocale upper_semilattice < weak_upper_semilattice
+sublocale upper_semilattice < weak: weak_upper_semilattice
   proof qed (rule sup_of_two_exists)
 
 locale lower_semilattice = partial_order +
   assumes inf_of_two_exists:
     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
 
-sublocale lower_semilattice < weak_lower_semilattice
+sublocale lower_semilattice < weak: weak_lower_semilattice
   proof qed (rule inf_of_two_exists)
 
 locale lattice = upper_semilattice + lower_semilattice
@@ -1183,7 +1183,7 @@
 locale total_order = partial_order +
   assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
 
-sublocale total_order < weak_total_order
+sublocale total_order < weak: weak_total_order
   proof qed (rule total_order_total)
 
 text {* Introduction rule: the usual definition of total order *}
@@ -1195,7 +1195,7 @@
 
 text {* Total orders are lattices. *}
 
-sublocale total_order < lattice
+sublocale total_order < weak: lattice
   proof qed (auto intro: sup_of_two_exists inf_of_two_exists)
 
 
@@ -1207,7 +1207,7 @@
     and inf_exists:
     "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
 
-sublocale complete_lattice < weak_complete_lattice
+sublocale complete_lattice < weak: weak_complete_lattice
   proof qed (auto intro: sup_exists inf_exists)
 
 text {* Introduction rule: the usual definition of complete lattice *}
diff -r 3adc06d6504f -r e190bc2a5399 src/HOL/Algebra/QuotRing.thy
--- a/src/HOL/Algebra/QuotRing.thy	Thu Dec 18 20:19:49 2008 +0100
+++ b/src/HOL/Algebra/QuotRing.thy	Fri Dec 19 11:09:09 2008 +0100
@@ -175,9 +175,9 @@
   interpret cring R by fact
   show ?thesis apply (rule ring_hom_cringI)
   apply (rule rcos_ring_hom_ring)
- apply (rule R.is_cring)
+ apply (rule is_cring)
 apply (rule quotient_is_cring)
-apply (rule R.is_cring)
+apply (rule is_cring)
 done
 qed