# 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 \}. 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 \}. *} + +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 "\" 50) where "less' \ 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 "\ x \ \ 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}%