doc-src/TutorialI/isabelle.sty
author paulson
Mon, 08 May 2000 16:57:53 +0200
changeset 8832 bcceda950cd0
parent 8824 ff207088cf0c
child 9673 1b2d4f995b13
permissions -rw-r--r--
more details

%%
%% $Id$
%%
%% macros for Isabelle generated LaTeX output
%%

%%% Simple document preparation (based on theory token language)

% isabelle environments

\newcommand{\isabellestyle}{\small\tt\slshape}

\newdimen\isa@parindent\newdimen\isa@parskip
\newenvironment{isabelle}{%
\isa@parindent\parindent\parindent0pt%
\isa@parskip\parskip\parskip0pt%
\isabellestyle}{}

\newcommand{\isa}[1]{\emph{\isabellestyle #1}}

\newenvironment{isabellequote}%
{\begin{quote}\begin{isabelle}\noindent}{\end{isabelle}\end{quote}}

\newcommand{\isanewline}{\mbox{}\\\mbox{}}

\chardef\isabraceleft=`\{
\chardef\isabraceright=`\}
\chardef\isatilde=`\~
\chardef\isacircum=`\^
\chardef\isabackslash=`\\


% keyword and section markup

\newcommand{\isacommand}[1]{\emph{\bf #1}}
\newcommand{\isakeyword}[1]{\emph{\bf #1}}
\newcommand{\isabeginblock}{\isakeyword{\{}}
\newcommand{\isaendblock}{\isakeyword{\}}}

\newcommand{\isamarkupheader}[1]{\section{#1}}
\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
\newcommand{\isamarkupsection}[1]{\section{#1}}
\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
\newcommand{\isamarkupsect}[1]{\section{#1}}
\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}

\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\par\medskip}{\par\smallskip}
\newenvironment{isamarkuptext}{\normalsize\rm\begin{isapar}}{\end{isapar}}
\newenvironment{isamarkuptxt}{\rm\begin{isapar}}{\end{isapar}}
\newcommand{\isamarkupcmt}[1]{{\rm--- #1}}