lib/texinputs/isabelle.sty
author wenzelm
Fri Oct 08 15:04:32 1999 +0200 (1999-10-08)
changeset 7797 38a46d9ea08a
parent 7788 825b8b1ad136
child 7811 eaf9e022eef3
permissions -rw-r--r--
improved special chars;
wenzelm@7709
     1
%%
wenzelm@7709
     2
%% $Id$
wenzelm@7709
     3
%%
wenzelm@7709
     4
%% macros for Isabelle generated LaTeX output
wenzelm@7709
     5
%%
wenzelm@7709
     6
wenzelm@7709
     7
%%% Simple document preparation (based on theory token language)
wenzelm@7709
     8
wenzelm@7788
     9
% basic environment
wenzelm@7788
    10
wenzelm@7709
    11
\newenvironment{isabellesimple}{\small\tt\slshape\mbox{}}{}
wenzelm@7709
    12
\newcommand{\isanewline}{\mbox{}\\\mbox{}}
wenzelm@7752
    13
wenzelm@7797
    14
\chardef\isabraceleft=`\{
wenzelm@7797
    15
\chardef\isabraceright=`\}
wenzelm@7797
    16
\chardef\isatilde=`\~
wenzelm@7797
    17
\chardef\isacircum=`\^
wenzelm@7797
    18
\chardef\isabackslash=`\\
wenzelm@7788
    19
wenzelm@7797
    20
wenzelm@7797
    21
% keyword and section markup
wenzelm@7788
    22
wenzelm@7709
    23
\newcommand{\isacommand}[1]{{\bf #1}}
wenzelm@7709
    24
\newcommand{\isakeyword}[1]{{\bf #1}}
wenzelm@7797
    25
\newcommand{\isabeginblock}{\isakeyword{\{}}
wenzelm@7797
    26
\newcommand{\isaendblock}{\isakeyword{\}}}
wenzelm@7758
    27
wenzelm@7758
    28
\newcommand{\isapar}[1]{{\par\medskip #1\par\smallskip}}
wenzelm@7771
    29
\newcommand{\isamarkupheader}[1]{#1}
wenzelm@7758
    30
wenzelm@7752
    31
\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
wenzelm@7752
    32
\newcommand{\isamarkupsection}[1]{\section{#1}}
wenzelm@7752
    33
\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
wenzelm@7752
    34
\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
wenzelm@7758
    35
\newcommand{\isamarkuptext}[1]{\isapar{\normalsize\rm #1}}
wenzelm@7752
    36
wenzelm@7752
    37
\newcommand{\isamarkupsect}[1]{\section{#1}}
wenzelm@7752
    38
\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
wenzelm@7752
    39
\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
wenzelm@7758
    40
\newcommand{\isamarkuptxt}[1]{\isapar{\rm #1}}
wenzelm@7758
    41
\newcommand{\isamarkupcmt}[1]{{\rm--- #1}}