# HG changeset patch
# User wenzelm
# Date 1212590671 -7200
# Node ID 6d2a458be1b6ef7a8e2c2d282fc4b53c373d6492
# Parent  0ee3854332478693f01a94094948e8e7c06d2437
replaced (*<*)(*>*) by invisibility tags;

diff -r 0ee385433247 -r 6d2a458be1b6 doc-src/Locales/Locales/Examples.thy
--- 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
-(*>*)
diff -r 0ee385433247 -r 6d2a458be1b6 doc-src/Locales/Locales/Examples1.thy
--- 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
-(*>*)
diff -r 0ee385433247 -r 6d2a458be1b6 doc-src/Locales/Locales/Examples2.thy
--- 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
diff -r 0ee385433247 -r 6d2a458be1b6 doc-src/Locales/Locales/Examples3.thy
--- 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
-(*>*)