doc-src/TutorialI/isabelle.sty
changeset 8824 ff207088cf0c
parent 8771 026f37a86ea7
child 9673 1b2d4f995b13
equal deleted inserted replaced
8823:bd8f8dbda512 8824:ff207088cf0c
     6 
     6 
     7 %%% Simple document preparation (based on theory token language)
     7 %%% Simple document preparation (based on theory token language)
     8 
     8 
     9 % isabelle environments
     9 % isabelle environments
    10 
    10 
    11 \newcommand{\isabelledefaultstyle}{\small\tt\slshape}
    11 \newcommand{\isabellestyle}{\small\tt\slshape}
    12 \newcommand{\isabellestyle}{}
       
    13 
    12 
    14 \newdimen\isa@parindent\newdimen\isa@parskip
    13 \newdimen\isa@parindent\newdimen\isa@parskip
    15 \newenvironment{isabelle}{%
    14 \newenvironment{isabelle}{%
    16 \isa@parindent\parindent\parindent0pt%
    15 \isa@parindent\parindent\parindent0pt%
    17 \isa@parskip\parskip\parskip0pt%
    16 \isa@parskip\parskip\parskip0pt%
    18 \isabelledefaultstyle\isabellestyle}{}
    17 \isabellestyle}{}
    19 
    18 
    20 \newcommand{\isa}[1]{\emph{\isabelledefaultstyle\isabellestyle #1}}
    19 \newcommand{\isa}[1]{\emph{\isabellestyle #1}}
    21 
    20 
    22 \newenvironment{isabellequote}%
    21 \newenvironment{isabellequote}%
    23 {\begin{quote}\begin{isabelle}\noindent}{\end{isabelle}\end{quote}}
    22 {\begin{quote}\begin{isabelle}\noindent}{\end{isabelle}\end{quote}}
    24 
    23 
    25 \newcommand{\isanewline}{\mbox{}\\\mbox{}}
    24 \newcommand{\isanewline}{\mbox{}\\\mbox{}}