--- a/doc-src/IsarAdvanced/Codegen/Thy/document/isabelle.sty Thu May 15 20:02:40 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,215 +0,0 @@
-%%
-%%
-%%
-%% macros for Isabelle generated LaTeX output
-%%
-
-%%% Simple document preparation (based on theory token language and symbols)
-
-% isabelle environments
-
-\newcommand{\isabellecontext}{UNKNOWN}
-
-\newcommand{\isastyle}{\UNDEF}
-\newcommand{\isastyleminor}{\UNDEF}
-\newcommand{\isastylescript}{\UNDEF}
-\newcommand{\isastyletext}{\normalsize\rm}
-\newcommand{\isastyletxt}{\rm}
-\newcommand{\isastylecmt}{\rm}
-
-%symbol markup -- \emph achieves decent spacing via italic corrections
-\newcommand{\isamath}[1]{\emph{$#1$}}
-\newcommand{\isatext}[1]{\emph{#1}}
-\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
-\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
-\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
-\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
-\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
-\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isastylescript}
-\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
-\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isastylescript}
-\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
-\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
-\newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
-\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
-
-
-\newdimen\isa@parindent\newdimen\isa@parskip
-
-\newenvironment{isabellebody}{%
-\isamarkuptrue\par%
-\isa@parindent\parindent\parindent0pt%
-\isa@parskip\parskip\parskip0pt%
-\isastyle}{\par}
-
-\newenvironment{isabelle}
-{\begin{trivlist}\begin{isabellebody}\item\relax}
-{\end{isabellebody}\end{trivlist}}
-
-\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
-
-\newcommand{\isaindent}[1]{\hphantom{#1}}
-\newcommand{\isanewline}{\mbox{}\par\mbox{}}
-\newcommand{\isasep}{}
-\newcommand{\isadigit}[1]{#1}
-
-\newcommand{\isachardefaults}{%
-\chardef\isacharbang=`\!%
-\chardef\isachardoublequote=`\"%
-\chardef\isachardoublequoteopen=`\"%
-\chardef\isachardoublequoteclose=`\"%
-\chardef\isacharhash=`\#%
-\chardef\isachardollar=`\$%
-\chardef\isacharpercent=`\%%
-\chardef\isacharampersand=`\&%
-\chardef\isacharprime=`\'%
-\chardef\isacharparenleft=`\(%
-\chardef\isacharparenright=`\)%
-\chardef\isacharasterisk=`\*%
-\chardef\isacharplus=`\+%
-\chardef\isacharcomma=`\,%
-\chardef\isacharminus=`\-%
-\chardef\isachardot=`\.%
-\chardef\isacharslash=`\/%
-\chardef\isacharcolon=`\:%
-\chardef\isacharsemicolon=`\;%
-\chardef\isacharless=`\<%
-\chardef\isacharequal=`\=%
-\chardef\isachargreater=`\>%
-\chardef\isacharquery=`\?%
-\chardef\isacharat=`\@%
-\chardef\isacharbrackleft=`\[%
-\chardef\isacharbackslash=`\\%
-\chardef\isacharbrackright=`\]%
-\chardef\isacharcircum=`\^%
-\chardef\isacharunderscore=`\_%
-\def\isacharunderscorekeyword{\_}%
-\chardef\isacharbackquote=`\`%
-\chardef\isacharbackquoteopen=`\`%
-\chardef\isacharbackquoteclose=`\`%
-\chardef\isacharbraceleft=`\{%
-\chardef\isacharbar=`\|%
-\chardef\isacharbraceright=`\}%
-\chardef\isachartilde=`\~%
-\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
-\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
-}
-
-
-% keyword and section markup
-
-\newcommand{\isakeyword}[1]
-{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
-\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
-\newcommand{\isacommand}[1]{\isakeyword{#1}}
-
-\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}}
-
-\newif\ifisamarkup
-\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
-\newcommand{\isaendpar}{\par\medskip}
-\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
-\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
-\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
-\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
-
-
-% styles
-
-\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
-
-\newcommand{\isabellestyledefault}{%
-\renewcommand{\isastyle}{\small\tt\slshape}%
-\renewcommand{\isastyleminor}{\small\tt\slshape}%
-\renewcommand{\isastylescript}{\footnotesize\tt\slshape}%
-\isachardefaults%
-}
-\isabellestyledefault
-
-\newcommand{\isabellestylett}{%
-\renewcommand{\isastyle}{\small\tt}%
-\renewcommand{\isastyleminor}{\small\tt}%
-\renewcommand{\isastylescript}{\footnotesize\tt}%
-\isachardefaults%
-}
-
-\newcommand{\isabellestyleit}{%
-\renewcommand{\isastyle}{\small\it}%
-\renewcommand{\isastyleminor}{\it}%
-\renewcommand{\isastylescript}{\footnotesize\it}%
-\renewcommand{\isacharunderscorekeyword}{\mbox{-}}%
-\renewcommand{\isacharbang}{\isamath{!}}%
-\renewcommand{\isachardoublequote}{}%
-\renewcommand{\isachardoublequoteopen}{}%
-\renewcommand{\isachardoublequoteclose}{}%
-\renewcommand{\isacharhash}{\isamath{\#}}%
-\renewcommand{\isachardollar}{\isamath{\$}}%
-\renewcommand{\isacharpercent}{\isamath{\%}}%
-\renewcommand{\isacharampersand}{\isamath{\&}}%
-\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
-\renewcommand{\isacharparenleft}{\isamath{(}}%
-\renewcommand{\isacharparenright}{\isamath{)}}%
-\renewcommand{\isacharasterisk}{\isamath{*}}%
-\renewcommand{\isacharplus}{\isamath{+}}%
-\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
-\renewcommand{\isacharminus}{\isamath{-}}%
-\renewcommand{\isachardot}{\isamath{\mathord.}}%
-\renewcommand{\isacharslash}{\isamath{/}}%
-\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
-\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
-\renewcommand{\isacharless}{\isamath{<}}%
-\renewcommand{\isacharequal}{\isamath{=}}%
-\renewcommand{\isachargreater}{\isamath{>}}%
-\renewcommand{\isacharat}{\isamath{@}}%
-\renewcommand{\isacharbrackleft}{\isamath{[}}%
-\renewcommand{\isacharbackslash}{\isamath{\backslash}}%
-\renewcommand{\isacharbrackright}{\isamath{]}}%
-\renewcommand{\isacharunderscore}{\mbox{-}}%
-\renewcommand{\isacharbraceleft}{\isamath{\{}}%
-\renewcommand{\isacharbar}{\isamath{\mid}}%
-\renewcommand{\isacharbraceright}{\isamath{\}}}%
-\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
-\renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
-\renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
-\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}%
-\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}%
-}
-
-\newcommand{\isabellestylesl}{%
-\isabellestyleit%
-\renewcommand{\isastyle}{\small\sl}%
-\renewcommand{\isastyleminor}{\sl}%
-\renewcommand{\isastylescript}{\footnotesize\sl}%
-}
-
-
-% tagged regions
-
-%plain TeX version of comment package -- much faster!
-\let\isafmtname\fmtname\def\fmtname{plain}
-\usepackage{comment}
-\let\fmtname\isafmtname
-
-\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
-
-\newcommand{\isakeeptag}[1]%
-{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
-\newcommand{\isadroptag}[1]%
-{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
-\newcommand{\isafoldtag}[1]%
-{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
-
-\isakeeptag{theory}
-\isakeeptag{proof}
-\isakeeptag{ML}
-\isakeeptag{visible}
-\isadroptag{invisible}
-
-\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}