--- 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
--- 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 *}
--- 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