doc-src/IsarImplementation/Thy/document/Syntax.tex
author wenzelm
Wed, 02 Dec 2009 12:04:07 +0100
changeset 33930 6a973bd43949
parent 30124 b956bf0dc87c
child 35001 31f8d9eaceff
permissions -rw-r--r--
slightly less ambitious settings, to avoid potential out-of-memory problem;

%
\begin{isabellebody}%
\def\isabellecontext{Syntax}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Syntax\isanewline
\isakeyword{imports}\ Base\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupchapter{Syntax and type-checking%
}
\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: