--- 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
--- 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}
*}
--- 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}%
--- 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}%