lib/texinputs/isabelle.sty
author wenzelm
Thu, 10 Feb 2000 20:54:40 +0100
changeset 8232 6b19ee96546c
parent 7918 2979b3b75dbd
child 8474 ae32be343647
permissions -rw-r--r--
\isabellesimplestyle;
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
8232
6b19ee96546c \isabellesimplestyle;
wenzelm
parents: 7918
diff changeset
    11
\newcommand{\isabellesimplestyle}{}
6b19ee96546c \isabellesimplestyle;
wenzelm
parents: 7918
diff changeset
    12
\newenvironment{isabellesimple}{\small\tt\slshape\isabellesimplestyle\mbox{}}{}
7709
545637744a85 macros for Isabelle generated LaTeX output;
wenzelm
parents:
diff changeset
    13
\newcommand{\isanewline}{\mbox{}\\\mbox{}}
7752
7ee322caf59c accomodate markup commands;
wenzelm
parents: 7709
diff changeset
    14
7797
38a46d9ea08a improved special chars;
wenzelm
parents: 7788
diff changeset
    15
\chardef\isabraceleft=`\{
38a46d9ea08a improved special chars;
wenzelm
parents: 7788
diff changeset
    16
\chardef\isabraceright=`\}
38a46d9ea08a improved special chars;
wenzelm
parents: 7788
diff changeset
    17
\chardef\isatilde=`\~
38a46d9ea08a improved special chars;
wenzelm
parents: 7788
diff changeset
    18
\chardef\isacircum=`\^
38a46d9ea08a improved special chars;
wenzelm
parents: 7788
diff changeset
    19
\chardef\isabackslash=`\\
7788
825b8b1ad136 removed verbatim markups;
wenzelm
parents: 7771
diff changeset
    20
7797
38a46d9ea08a improved special chars;
wenzelm
parents: 7788
diff changeset
    21
38a46d9ea08a improved special chars;
wenzelm
parents: 7788
diff changeset
    22
% keyword and section markup
7788
825b8b1ad136 removed verbatim markups;
wenzelm
parents: 7771
diff changeset
    23
7918
2979b3b75dbd achieve proper italic correction;
wenzelm
parents: 7907
diff changeset
    24
\newcommand{\isacommand}[1]{\emph{\bf #1}}
2979b3b75dbd achieve proper italic correction;
wenzelm
parents: 7907
diff changeset
    25
\newcommand{\isakeyword}[1]{\emph{\bf #1}}
7797
38a46d9ea08a improved special chars;
wenzelm
parents: 7788
diff changeset
    26
\newcommand{\isabeginblock}{\isakeyword{\{}}
38a46d9ea08a improved special chars;
wenzelm
parents: 7788
diff changeset
    27
\newcommand{\isaendblock}{\isakeyword{\}}}
7758
d36c19045493 tuned markup commands;
wenzelm
parents: 7752
diff changeset
    28
d36c19045493 tuned markup commands;
wenzelm
parents: 7752
diff changeset
    29
\newcommand{\isapar}[1]{{\par\medskip #1\par\smallskip}}
7771
cc8e2263be65 verbatim: no markup;
wenzelm
parents: 7758
diff changeset
    30
\newcommand{\isamarkupheader}[1]{#1}
7758
d36c19045493 tuned markup commands;
wenzelm
parents: 7752
diff changeset
    31
7752
7ee322caf59c accomodate markup commands;
wenzelm
parents: 7709
diff changeset
    32
\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
7ee322caf59c accomodate markup commands;
wenzelm
parents: 7709
diff changeset
    33
\newcommand{\isamarkupsection}[1]{\section{#1}}
7ee322caf59c accomodate markup commands;
wenzelm
parents: 7709
diff changeset
    34
\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
7ee322caf59c accomodate markup commands;
wenzelm
parents: 7709
diff changeset
    35
\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
7758
d36c19045493 tuned markup commands;
wenzelm
parents: 7752
diff changeset
    36
\newcommand{\isamarkuptext}[1]{\isapar{\normalsize\rm #1}}
7752
7ee322caf59c accomodate markup commands;
wenzelm
parents: 7709
diff changeset
    37
7ee322caf59c accomodate markup commands;
wenzelm
parents: 7709
diff changeset
    38
\newcommand{\isamarkupsect}[1]{\section{#1}}
7ee322caf59c accomodate markup commands;
wenzelm
parents: 7709
diff changeset
    39
\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
7ee322caf59c accomodate markup commands;
wenzelm
parents: 7709
diff changeset
    40
\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
7758
d36c19045493 tuned markup commands;
wenzelm
parents: 7752
diff changeset
    41
\newcommand{\isamarkuptxt}[1]{\isapar{\rm #1}}
d36c19045493 tuned markup commands;
wenzelm
parents: 7752
diff changeset
    42
\newcommand{\isamarkupcmt}[1]{{\rm--- #1}}