lib/texinputs/isabelle.sty
author wenzelm
Thu, 14 Oct 1999 15:14:14 +0200
changeset 7868 0cb6508f190c
parent 7811 eaf9e022eef3
child 7907 258f136864db
permissions -rw-r--r--
support thumbpdf;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7709
545637744a85 macros for Isabelle generated LaTeX output;
wenzelm
parents:
diff changeset
     1
%%
545637744a85 macros for Isabelle generated LaTeX output;
wenzelm
parents:
diff changeset
     2
%% $Id$
545637744a85 macros for Isabelle generated LaTeX output;
wenzelm
parents:
diff changeset
     3
%%
545637744a85 macros for Isabelle generated LaTeX output;
wenzelm
parents:
diff changeset
     4
%% macros for Isabelle generated LaTeX output
545637744a85 macros for Isabelle generated LaTeX output;
wenzelm
parents:
diff changeset
     5
%%
545637744a85 macros for Isabelle generated LaTeX output;
wenzelm
parents:
diff changeset
     6
545637744a85 macros for Isabelle generated LaTeX output;
wenzelm
parents:
diff changeset
     7
%%% Simple document preparation (based on theory token language)
545637744a85 macros for Isabelle generated LaTeX output;
wenzelm
parents:
diff changeset
     8
7788
825b8b1ad136 removed verbatim markups;
wenzelm
parents: 7771
diff changeset
     9
% basic environment
825b8b1ad136 removed verbatim markups;
wenzelm
parents: 7771
diff changeset
    10
7709
545637744a85 macros for Isabelle generated LaTeX output;
wenzelm
parents:
diff changeset
    11
\newenvironment{isabellesimple}{\small\tt\slshape\mbox{}}{}
545637744a85 macros for Isabelle generated LaTeX output;
wenzelm
parents:
diff changeset
    12
\newcommand{\isanewline}{\mbox{}\\\mbox{}}
7752
7ee322caf59c accomodate markup commands;
wenzelm
parents: 7709
diff changeset
    13
7797
38a46d9ea08a improved special chars;
wenzelm
parents: 7788
diff changeset
    14
\chardef\isabraceleft=`\{
38a46d9ea08a improved special chars;
wenzelm
parents: 7788
diff changeset
    15
\chardef\isabraceright=`\}
38a46d9ea08a improved special chars;
wenzelm
parents: 7788
diff changeset
    16
\chardef\isatilde=`\~
38a46d9ea08a improved special chars;
wenzelm
parents: 7788
diff changeset
    17
\chardef\isacircum=`\^
38a46d9ea08a improved special chars;
wenzelm
parents: 7788
diff changeset
    18
\chardef\isabackslash=`\\
7788
825b8b1ad136 removed verbatim markups;
wenzelm
parents: 7771
diff changeset
    19
7797
38a46d9ea08a improved special chars;
wenzelm
parents: 7788
diff changeset
    20
38a46d9ea08a improved special chars;
wenzelm
parents: 7788
diff changeset
    21
% keyword and section markup
7788
825b8b1ad136 removed verbatim markups;
wenzelm
parents: 7771
diff changeset
    22
7709
545637744a85 macros for Isabelle generated LaTeX output;
wenzelm
parents:
diff changeset
    23
\newcommand{\isacommand}[1]{{\bf #1}}
7811
eaf9e022eef3 \isakeyword: italic correction;
wenzelm
parents: 7797
diff changeset
    24
\newcommand{\isakeyword}[1]{\/{\bf #1}\/}
7797
38a46d9ea08a improved special chars;
wenzelm
parents: 7788
diff changeset
    25
\newcommand{\isabeginblock}{\isakeyword{\{}}
38a46d9ea08a improved special chars;
wenzelm
parents: 7788
diff changeset
    26
\newcommand{\isaendblock}{\isakeyword{\}}}
7758
d36c19045493 tuned markup commands;
wenzelm
parents: 7752
diff changeset
    27
d36c19045493 tuned markup commands;
wenzelm
parents: 7752
diff changeset
    28
\newcommand{\isapar}[1]{{\par\medskip #1\par\smallskip}}
7771
cc8e2263be65 verbatim: no markup;
wenzelm
parents: 7758
diff changeset
    29
\newcommand{\isamarkupheader}[1]{#1}
7758
d36c19045493 tuned markup commands;
wenzelm
parents: 7752
diff changeset
    30
7752
7ee322caf59c accomodate markup commands;
wenzelm
parents: 7709
diff changeset
    31
\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
7ee322caf59c accomodate markup commands;
wenzelm
parents: 7709
diff changeset
    32
\newcommand{\isamarkupsection}[1]{\section{#1}}
7ee322caf59c accomodate markup commands;
wenzelm
parents: 7709
diff changeset
    33
\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
7ee322caf59c accomodate markup commands;
wenzelm
parents: 7709
diff changeset
    34
\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
7758
d36c19045493 tuned markup commands;
wenzelm
parents: 7752
diff changeset
    35
\newcommand{\isamarkuptext}[1]{\isapar{\normalsize\rm #1}}
7752
7ee322caf59c accomodate markup commands;
wenzelm
parents: 7709
diff changeset
    36
7ee322caf59c accomodate markup commands;
wenzelm
parents: 7709
diff changeset
    37
\newcommand{\isamarkupsect}[1]{\section{#1}}
7ee322caf59c accomodate markup commands;
wenzelm
parents: 7709
diff changeset
    38
\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
7ee322caf59c accomodate markup commands;
wenzelm
parents: 7709
diff changeset
    39
\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
7758
d36c19045493 tuned markup commands;
wenzelm
parents: 7752
diff changeset
    40
\newcommand{\isamarkuptxt}[1]{\isapar{\rm #1}}
d36c19045493 tuned markup commands;
wenzelm
parents: 7752
diff changeset
    41
\newcommand{\isamarkupcmt}[1]{{\rm--- #1}}