doc-src/TutorialI/isabelle.sty
changeset 8751 9ed0548177fb
child 8771 026f37a86ea7
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/isabelle.sty	Wed Apr 19 13:40:42 2000 +0200
@@ -0,0 +1,50 @@
+%%
+%% $Id$
+%%
+%% macros for Isabelle generated LaTeX output
+%%
+
+%%% Simple document preparation (based on theory token language)
+
+% isabelle environments
+
+\newcommand{\isabelledefaultstyle}{\small\tt\slshape}
+\newcommand{\isabellestyle}{}
+
+\newdimen\isa@parindent\newdimen\isa@parskip
+\newenvironment{isabelle}{%
+\isa@parindent\parindent\parindent0pt%
+\isa@parskip\parskip\parskip0pt%
+\isabelledefaultstyle\isabellestyle}{}
+
+\newcommand{\isa}[1]{\emph{\isabelledefaultstyle\isabellestyle #1}}
+
+\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}}