--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Wed Oct 10 15:27:10 2012 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Wed Oct 10 15:39:01 2012 +0200
@@ -104,7 +104,7 @@
end
print_locale! logic
-locale use_decl = logic + semi "op ||"
+locale use_decl = l: logic + semi "op ||"
print_locale! use_decl thm use_decl_def
locale extra_type =
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Oct 10 15:27:10 2012 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Wed Oct 10 15:39:01 2012 +0200
@@ -452,7 +452,7 @@
assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y"
and between_same: "between x x = x"
-sublocale constr_dense_linorder < dense_linorder
+sublocale constr_dense_linorder < dlo: dense_linorder
apply unfold_locales
using gt_ex lt_ex between_less
apply auto
--- a/src/HOL/Finite_Set.thy Wed Oct 10 15:27:10 2012 +0200
+++ b/src/HOL/Finite_Set.thy Wed Oct 10 15:39:01 2012 +0200
@@ -1771,7 +1771,7 @@
locale folding_image_simple_idem = folding_image_simple +
assumes idem: "x * x = x"
-sublocale folding_image_simple_idem < semilattice proof
+sublocale folding_image_simple_idem < semilattice: semilattice proof
qed (fact idem)
context folding_image_simple_idem
@@ -1912,7 +1912,7 @@
locale folding_one_idem = folding_one +
assumes idem: "x * x = x"
-sublocale folding_one_idem < semilattice proof
+sublocale folding_one_idem < semilattice: semilattice proof
qed (fact idem)
context folding_one_idem
--- a/src/HOL/ex/Tarski.thy Wed Oct 10 15:27:10 2012 +0200
+++ b/src/HOL/ex/Tarski.thy Wed Oct 10 15:39:01 2012 +0200
@@ -119,7 +119,7 @@
locale CL = S +
assumes cl_co: "cl : CompleteLattice"
-sublocale CL < PO
+sublocale CL < po: PO
apply (simp_all add: A_def r_def)
apply unfold_locales
using cl_co unfolding CompleteLattice_def by auto
@@ -130,7 +130,7 @@
assumes f_cl: "(cl,f) : CLF_set" (*was the equivalent "f : CLF_set``{cl}"*)
defines P_def: "P == fix f A"
-sublocale CLF < CL
+sublocale CLF < cl: CL
apply (simp_all add: A_def r_def)
apply unfold_locales
using f_cl unfolding CLF_set_def by auto