# HG changeset patch
# User wenzelm
# Date 1236626985 -3600
# Node ID aa6f42252bf639a980d259615746fc6d256823a1
# Parent  9fe4bbb90297c96f3fab9958c24e4d6113086bc5
replaced old locale option by proper "text (in locale)";

diff -r 9fe4bbb90297 -r aa6f42252bf6 doc-src/Locales/Locales/Examples.thy
--- a/doc-src/Locales/Locales/Examples.thy	Mon Mar 09 17:55:03 2009 +0100
+++ b/doc-src/Locales/Locales/Examples.thy	Mon Mar 09 20:29:45 2009 +0100
@@ -109,9 +109,11 @@
   At the same time, the locale is extended by syntax information
   hiding this construction in the context of the locale.  That is,
   @{term "partial_order.less le"} is printed and parsed as infix
-  @{text \<sqsubset>}.  Finally, the conclusion of the definition is added to
-  the locale, @{thm [locale=partial_order, source] less_def}:
-  @{thm [locale=partial_order, display, indent=2] less_def}
+  @{text \<sqsubset>}. *}
+
+text (in partial_order) {* Finally, the conclusion of the definition
+  is added to the locale, @{thm [source] less_def}:
+  @{thm [display, indent=2] less_def}
   *}
 
 text {* As an example of a theorem statement in the locale, here is the
diff -r 9fe4bbb90297 -r aa6f42252bf6 doc-src/Locales/Locales/Examples3.thy
--- a/doc-src/Locales/Locales/Examples3.thy	Mon Mar 09 17:55:03 2009 +0100
+++ b/doc-src/Locales/Locales/Examples3.thy	Mon Mar 09 20:29:45 2009 +0100
@@ -314,8 +314,8 @@
   abbreviation (in order_preserving)
     less' (infixl "\<prec>" 50) where "less' \<equiv> partial_order.less le'"
 
-text {* Now the theorem is displayed nicely as
-  @{thm [locale=order_preserving] le'.less_le_trans}.  *}
+text (in order_preserving) {* Now the theorem is displayed nicely as
+  @{thm le'.less_le_trans}.  *}
 
 text {* Not only names of theorems are qualified.  In fact, all names
   are qualified, in particular names introduced by definitions and
@@ -399,12 +399,12 @@
     then show "\<phi> x \<preceq> \<phi> y" by (simp add: le'.join_connection)
   qed
 
-text {* Theorems and other declarations --- syntax, in particular ---
-  from the locale @{text order_preserving} are now active in @{text
+text (in lattice_hom) {*
+  Theorems and other declarations --- syntax, in particular --- from
+  the locale @{text order_preserving} are now active in @{text
   lattice_hom}, for example
-
-  @{thm [locale=lattice_hom, source] le'.less_le_trans}:
-  @{thm [locale=lattice_hom] le'.less_le_trans}
+  @{thm [source] le'.less_le_trans}:
+  @{thm le'.less_le_trans}
   *}
 
 
diff -r 9fe4bbb90297 -r aa6f42252bf6 doc-src/Locales/Locales/document/Examples.tex
--- a/doc-src/Locales/Locales/document/Examples.tex	Mon Mar 09 17:55:03 2009 +0100
+++ b/doc-src/Locales/Locales/document/Examples.tex	Mon Mar 09 20:29:45 2009 +0100
@@ -142,8 +142,13 @@
   At the same time, the locale is extended by syntax information
   hiding this construction in the context of the locale.  That is,
   \isa{partial{\isacharunderscore}order{\isachardot}less\ le} is printed and parsed as infix
-  \isa{{\isasymsqsubset}}.  Finally, the conclusion of the definition is added to
-  the locale, \isa{less{\isacharunderscore}def}:
+  \isa{{\isasymsqsubset}}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Finally, the conclusion of the definition
+  is added to the locale, \isa{less{\isacharunderscore}def}:
   \begin{isabelle}%
 \ \ {\isacharparenleft}{\isacharquery}x\ {\isasymsqsubset}\ {\isacharquery}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharquery}x\ {\isasymsqsubseteq}\ {\isacharquery}y\ {\isasymand}\ {\isacharquery}x\ {\isasymnoteq}\ {\isacharquery}y{\isacharparenright}%
 \end{isabelle}%
diff -r 9fe4bbb90297 -r aa6f42252bf6 doc-src/Locales/Locales/document/Examples3.tex
--- a/doc-src/Locales/Locales/document/Examples3.tex	Mon Mar 09 17:55:03 2009 +0100
+++ b/doc-src/Locales/Locales/document/Examples3.tex	Mon Mar 09 20:29:45 2009 +0100
@@ -686,9 +686,8 @@
 \endisadelimproof
 %
 \begin{isamarkuptext}%
-Theorems and other declarations --- syntax, in particular ---
-  from the locale \isa{order{\isacharunderscore}preserving} are now active in \isa{lattice{\isacharunderscore}hom}, for example
-
+Theorems and other declarations --- syntax, in particular --- from
+  the locale \isa{order{\isacharunderscore}preserving} are now active in \isa{lattice{\isacharunderscore}hom}, for example
   \isa{le{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}:
   \isa{{\isasymlbrakk}{\isacharquery}x\ {\isasymprec}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymprec}\ {\isacharquery}z}%
 \end{isamarkuptext}%