# HG changeset patch # User wenzelm # Date 1212590648 -7200 # Node ID 0ee3854332478693f01a94094948e8e7c06d2437 # Parent 61ac01ff0aa96d901e7ab995796c8d18db01b469 updated generated file; diff -r 61ac01ff0aa9 -r 0ee385433247 doc-src/Locales/Locales/document/Examples.tex --- a/doc-src/Locales/Locales/document/Examples.tex Wed Jun 04 16:32:24 2008 +0200 +++ b/doc-src/Locales/Locales/document/Examples.tex Wed Jun 04 16:44:08 2008 +0200 @@ -3,18 +3,41 @@ \def\isabellecontext{Examples}% % \isadelimtheory +\isanewline +\isanewline % \endisadelimtheory % \isatagtheory -% +\isacommand{theory}\isamarkupfalse% +\ Examples\isanewline +\isakeyword{imports}\ GCD\isanewline +\isakeyword{begin}% \endisatagtheory {\isafoldtheory}% % \isadelimtheory +\isanewline % \endisadelimtheory % +\isadeliminvisible +\isanewline +% +\endisadeliminvisible +% +\isataginvisible +\isacommand{hide}\isamarkupfalse% +\ const\ Lattices{\isachardot}lattice\isanewline +\isacommand{pretty{\isacharunderscore}setmargin}\isamarkupfalse% +\ {\isadigit{6}}{\isadigit{5}}% +\endisataginvisible +{\isafoldinvisible}% +% +\isadeliminvisible +% +\endisadeliminvisible +% \isamarkupsection{Introduction% } \isamarkuptrue% @@ -1389,6 +1412,7 @@ \endisadelimtheory % \isatagtheory +\isacommand{end}\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -1396,6 +1420,7 @@ \isadelimtheory % \endisadelimtheory +\isanewline \end{isabellebody}% %%% Local Variables: %%% mode: latex diff -r 61ac01ff0aa9 -r 0ee385433247 doc-src/Locales/Locales/document/Examples1.tex --- a/doc-src/Locales/Locales/document/Examples1.tex Wed Jun 04 16:32:24 2008 +0200 +++ b/doc-src/Locales/Locales/document/Examples1.tex Wed Jun 04 16:44:08 2008 +0200 @@ -3,11 +3,16 @@ \def\isabellecontext{Examples{\isadigit{1}}}% % \isadelimtheory +\isanewline +\isanewline % \endisadelimtheory % \isatagtheory -% +\isacommand{theory}\isamarkupfalse% +\ Examples{\isadigit{1}}\isanewline +\isakeyword{imports}\ Examples\isanewline +\isakeyword{begin}% \endisatagtheory {\isafoldtheory}% % @@ -134,6 +139,7 @@ \endisadelimtheory % \isatagtheory +\isacommand{end}\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -141,6 +147,7 @@ \isadelimtheory % \endisadelimtheory +\isanewline \end{isabellebody}% %%% Local Variables: %%% mode: latex diff -r 61ac01ff0aa9 -r 0ee385433247 doc-src/Locales/Locales/document/Examples2.tex --- a/doc-src/Locales/Locales/document/Examples2.tex Wed Jun 04 16:32:24 2008 +0200 +++ b/doc-src/Locales/Locales/document/Examples2.tex Wed Jun 04 16:44:08 2008 +0200 @@ -3,11 +3,16 @@ \def\isabellecontext{Examples{\isadigit{2}}}% % \isadelimtheory +\isanewline +\isanewline % \endisadelimtheory % \isatagtheory -% +\isacommand{theory}\isamarkupfalse% +\ Examples{\isadigit{2}}\isanewline +\isakeyword{imports}\ Examples\isanewline +\isakeyword{begin}% \endisatagtheory {\isafoldtheory}% % @@ -76,6 +81,7 @@ \endisadelimtheory % \isatagtheory +\isacommand{end}\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -83,6 +89,7 @@ \isadelimtheory % \endisadelimtheory +\isanewline \end{isabellebody}% %%% Local Variables: %%% mode: latex diff -r 61ac01ff0aa9 -r 0ee385433247 doc-src/Locales/Locales/document/Examples3.tex --- a/doc-src/Locales/Locales/document/Examples3.tex Wed Jun 04 16:32:24 2008 +0200 +++ b/doc-src/Locales/Locales/document/Examples3.tex Wed Jun 04 16:44:08 2008 +0200 @@ -3,11 +3,16 @@ \def\isabellecontext{Examples{\isadigit{3}}}% % \isadelimtheory +\isanewline +\isanewline % \endisadelimtheory % \isatagtheory -% +\isacommand{theory}\isamarkupfalse% +\ Examples{\isadigit{3}}\isanewline +\isakeyword{imports}\ Examples\isanewline +\isakeyword{begin}% \endisatagtheory {\isafoldtheory}% % @@ -834,6 +839,7 @@ \endisadelimtheory % \isatagtheory +\isacommand{end}\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -841,6 +847,7 @@ \isadelimtheory % \endisadelimtheory +\isanewline \end{isabellebody}% %%% Local Variables: %%% mode: latex