--- a/doc-src/Locales/Locales/Examples.thy Wed Jun 04 16:44:08 2008 +0200
+++ b/doc-src/Locales/Locales/Examples.thy Wed Jun 04 16:44:31 2008 +0200
@@ -1,12 +1,11 @@
-(*<*)
+(* $Id$ *)
+
theory Examples
imports GCD
begin
-hide const Lattices.lattice
-pretty_setmargin 65
-
-(*>*)
+hide %invisible const Lattices.lattice
+pretty_setmargin %invisible 65
(*
text {* The following presentation will use notation of
@@ -678,6 +677,4 @@
text {* The locale hierarchy is now as shown in Figure~\ref{fig:lattices}(c). *}
-(*<*)
end
-(*>*)
--- a/doc-src/Locales/Locales/Examples1.thy Wed Jun 04 16:44:08 2008 +0200
+++ b/doc-src/Locales/Locales/Examples1.thy Wed Jun 04 16:44:31 2008 +0200
@@ -1,10 +1,9 @@
-(*<*)
+(* $Id$ *)
+
theory Examples1
imports Examples
begin
-(*>*)
-
section {* Use of Locales in Theories and Proofs *}
text {* Locales enable to prove theorems abstractly, relative to
@@ -87,6 +86,4 @@
\isakeyword{inductive}, \isakeyword{fun} and \isakeyword{function}.}
*}
-(*<*)
end
-(*>*)
--- a/doc-src/Locales/Locales/Examples2.thy Wed Jun 04 16:44:08 2008 +0200
+++ b/doc-src/Locales/Locales/Examples2.thy Wed Jun 04 16:44:31 2008 +0200
@@ -1,10 +1,9 @@
-(*<*)
+(* $Id$ *)
+
theory Examples2
imports Examples
begin
-(*>*)
-
text {* This is achieved by unfolding suitable equations during
interpretation. These equations are given after the keyword
\isakeyword{where} and require proofs. The revised command,
@@ -29,6 +28,4 @@
"partial_order.less_def"} is obtained manually with @{text OF}.
*}
-(*<*)
end
-(*>*)
\ No newline at end of file
--- a/doc-src/Locales/Locales/Examples3.thy Wed Jun 04 16:44:08 2008 +0200
+++ b/doc-src/Locales/Locales/Examples3.thy Wed Jun 04 16:44:31 2008 +0200
@@ -1,10 +1,9 @@
-(*<*)
+(* $Id$ *)
+
theory Examples3
imports Examples
begin
-(*>*)
-
subsection {* Third Version: Local Interpretation *}
text {* In the above example, the fact that @{text \<le>} is a partial
@@ -540,6 +539,4 @@
Christian Sternagel and Makarius Wenzel have made useful comments on
a draft of this document. *}
-(*<*)
end
-(*>*)