doc-src/IsarImplementation/Thy/document/locale.tex
author paulson
Wed, 19 Jul 2006 11:55:26 +0200
changeset 20153 6ff5d35749b0
parent 18537 2681f9e34390
child 20451 27ea2ba48fa3
permissions -rw-r--r--
Fixed the bugs introduced by the last commit! Output is now *identical* to that produced by the old version, based on a-lists.

%
\begin{isabellebody}%
\def\isabellecontext{locale}%
%
\isadelimtheory
\isanewline
\isanewline
\isanewline
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ {\isachardoublequoteopen}locale{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupchapter{Structured specifications%
}
\isamarkuptrue%
%
\isamarkupsection{Specification elements%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{Locales%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
FIXME%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: