author wenzelm Wed, 10 Oct 2012 15:39:01 +0200 changeset 49756 28e37eab4e6f parent 49755 b286e8f47560 child 49806 acb6fa98e310
 src/FOL/ex/Locale_Test/Locale_Test1.thy file | annotate | diff | comparison | revisions src/HOL/Decision_Procs/Dense_Linear_Order.thy file | annotate | diff | comparison | revisions src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions src/HOL/ex/Tarski.thy file | annotate | diff | comparison | revisions
```--- 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