# 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 \} is a partial @@ -540,6 +539,4 @@ Christian Sternagel and Makarius Wenzel have made useful comments on a draft of this document. *} -(*<*) end -(*>*)