author | wenzelm |
Thu, 01 Sep 2005 00:45:24 +0200 | |
changeset 17214 | af174eeafba1 |
parent 17175 | 1eced27ee0e1 |
child 17536 | 1b7c2f7df2e6 |
permissions | -rw-r--r-- |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
1 |
%% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
2 |
%% Author: Markus Wenzel, TU Muenchen |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
3 |
%% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
4 |
%% macros for Isabelle generated LaTeX output |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
5 |
%% |
17175 | 6 |
%% |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
7 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
8 |
%%% Simple document preparation (based on theory token language and symbols) |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
9 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
10 |
% isabelle environments |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
11 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
12 |
\newcommand{\isabellecontext}{UNKNOWN} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
13 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
14 |
\newcommand{\isastyle}{\small\tt\slshape} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
15 |
\newcommand{\isastyleminor}{\small\tt\slshape} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
16 |
\newcommand{\isastylescript}{\footnotesize\tt\slshape} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
17 |
\newcommand{\isastyletext}{\normalsize\rm} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
18 |
\newcommand{\isastyletxt}{\rm} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
19 |
\newcommand{\isastylecmt}{\rm} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
20 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
21 |
%symbol markup -- \emph achieves decent spacing via italic corrections |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
22 |
\newcommand{\isamath}[1]{\emph{$#1$}} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
23 |
\newcommand{\isatext}[1]{\emph{#1}} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
24 |
\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}} |
17214 | 25 |
\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} |
26 |
\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} |
|
27 |
\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} |
|
28 |
\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
29 |
\newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
30 |
\newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
31 |
\newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
32 |
\newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
33 |
\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}} |
17175 | 34 |
\newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}} |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
35 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
36 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
37 |
\newdimen\isa@parindent\newdimen\isa@parskip |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
38 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
39 |
\newenvironment{isabellebody}{% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
40 |
\isamarkuptrue\par% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
41 |
\isa@parindent\parindent\parindent0pt% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
42 |
\isa@parskip\parskip\parskip0pt% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
43 |
\isastyle}{\par} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
44 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
45 |
\newenvironment{isabelle} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
46 |
{\begin{trivlist}\begin{isabellebody}\item\relax} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
47 |
{\end{isabellebody}\end{trivlist}} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
48 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
49 |
\newcommand{\isa}[1]{\emph{\isastyleminor #1}} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
50 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
51 |
\newcommand{\isaindent}[1]{\hphantom{#1}} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
52 |
\newcommand{\isanewline}{\mbox{}\par\mbox{}} |
17175 | 53 |
\newcommand{\isasep}{} |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
54 |
\newcommand{\isadigit}[1]{#1} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
55 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
56 |
\chardef\isacharbang=`\! |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
57 |
\chardef\isachardoublequote=`\" |
17175 | 58 |
\chardef\isachardoublequoteopen=`\" |
59 |
\chardef\isachardoublequoteclose=`\" |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
60 |
\chardef\isacharhash=`\# |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
61 |
\chardef\isachardollar=`\$ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
62 |
\chardef\isacharpercent=`\% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
63 |
\chardef\isacharampersand=`\& |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
64 |
\chardef\isacharprime=`\' |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
65 |
\chardef\isacharparenleft=`\( |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
66 |
\chardef\isacharparenright=`\) |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
67 |
\chardef\isacharasterisk=`\* |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
68 |
\chardef\isacharplus=`\+ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
69 |
\chardef\isacharcomma=`\, |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
70 |
\chardef\isacharminus=`\- |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
71 |
\chardef\isachardot=`\. |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
72 |
\chardef\isacharslash=`\/ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
73 |
\chardef\isacharcolon=`\: |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
74 |
\chardef\isacharsemicolon=`\; |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
75 |
\chardef\isacharless=`\< |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
76 |
\chardef\isacharequal=`\= |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
77 |
\chardef\isachargreater=`\> |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
78 |
\chardef\isacharquery=`\? |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
79 |
\chardef\isacharat=`\@ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
80 |
\chardef\isacharbrackleft=`\[ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
81 |
\chardef\isacharbackslash=`\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
82 |
\chardef\isacharbrackright=`\] |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
83 |
\chardef\isacharcircum=`\^ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
84 |
\chardef\isacharunderscore=`\_ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
85 |
\chardef\isacharbackquote=`\` |
17175 | 86 |
\chardef\isacharbackquoteopen=`\` |
87 |
\chardef\isacharbackquoteclose=`\` |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
88 |
\chardef\isacharbraceleft=`\{ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
89 |
\chardef\isacharbar=`\| |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
90 |
\chardef\isacharbraceright=`\} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
91 |
\chardef\isachartilde=`\~ |
17214 | 92 |
\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk} |
93 |
\def\isacharverbatimclose{\isacharasterisk\isacharbraceright} |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
94 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
95 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
96 |
% keyword and section markup |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
97 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
98 |
\newcommand{\isakeywordcharunderscore}{\_} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
99 |
\newcommand{\isakeyword}[1] |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
100 |
{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isakeywordcharunderscore}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
101 |
\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
102 |
\newcommand{\isacommand}[1]{\isakeyword{#1}} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
103 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
104 |
\newcommand{\isamarkupheader}[1]{\section{#1}} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
105 |
\newcommand{\isamarkupchapter}[1]{\chapter{#1}} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
106 |
\newcommand{\isamarkupsection}[1]{\section{#1}} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
107 |
\newcommand{\isamarkupsubsection}[1]{\subsection{#1}} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
108 |
\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
109 |
\newcommand{\isamarkupsect}[1]{\section{#1}} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
110 |
\newcommand{\isamarkupsubsect}[1]{\subsection{#1}} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
111 |
\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
112 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
113 |
\newif\ifisamarkup |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
114 |
\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
115 |
\newcommand{\isaendpar}{\par\medskip} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
116 |
\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar} |
17214 | 117 |
\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}} |
118 |
\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}} |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
119 |
\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
120 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
121 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
122 |
% alternative styles |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
123 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
124 |
\newcommand{\isabellestyle}{} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
125 |
\def\isabellestyle#1{\csname isabellestyle#1\endcsname} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
126 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
127 |
\newcommand{\isabellestylett}{% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
128 |
\renewcommand{\isastyle}{\small\tt}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
129 |
\renewcommand{\isastyleminor}{\small\tt}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
130 |
\renewcommand{\isastylescript}{\footnotesize\tt}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
131 |
} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
132 |
\newcommand{\isabellestyleit}{% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
133 |
\renewcommand{\isastyle}{\small\it}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
134 |
\renewcommand{\isastyleminor}{\it}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
135 |
\renewcommand{\isastylescript}{\footnotesize\it}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
136 |
\renewcommand{\isakeywordcharunderscore}{\mbox{-}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
137 |
\renewcommand{\isacharbang}{\isamath{!}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
138 |
\renewcommand{\isachardoublequote}{}% |
17175 | 139 |
\renewcommand{\isachardoublequoteopen}{}% |
140 |
\renewcommand{\isachardoublequoteclose}{}% |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
141 |
\renewcommand{\isacharhash}{\isamath{\#}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
142 |
\renewcommand{\isachardollar}{\isamath{\$}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
143 |
\renewcommand{\isacharpercent}{\isamath{\%}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
144 |
\renewcommand{\isacharampersand}{\isamath{\&}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
145 |
\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
146 |
\renewcommand{\isacharparenleft}{\isamath{(}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
147 |
\renewcommand{\isacharparenright}{\isamath{)}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
148 |
\renewcommand{\isacharasterisk}{\isamath{*}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
149 |
\renewcommand{\isacharplus}{\isamath{+}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
150 |
\renewcommand{\isacharcomma}{\isamath{\mathord,}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
151 |
\renewcommand{\isacharminus}{\isamath{-}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
152 |
\renewcommand{\isachardot}{\isamath{\mathord.}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
153 |
\renewcommand{\isacharslash}{\isamath{/}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
154 |
\renewcommand{\isacharcolon}{\isamath{\mathord:}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
155 |
\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
156 |
\renewcommand{\isacharless}{\isamath{<}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
157 |
\renewcommand{\isacharequal}{\isamath{=}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
158 |
\renewcommand{\isachargreater}{\isamath{>}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
159 |
\renewcommand{\isacharat}{\isamath{@}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
160 |
\renewcommand{\isacharbrackleft}{\isamath{[}}% |
17125 | 161 |
\renewcommand{\isacharbackslash}{\isamath{\backslash}}% |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
162 |
\renewcommand{\isacharbrackright}{\isamath{]}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
163 |
\renewcommand{\isacharunderscore}{\mbox{-}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
164 |
\renewcommand{\isacharbraceleft}{\isamath{\{}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
165 |
\renewcommand{\isacharbar}{\isamath{\mid}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
166 |
\renewcommand{\isacharbraceright}{\isamath{\}}}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
167 |
\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}% |
17175 | 168 |
\renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}% |
169 |
\renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}% |
|
17214 | 170 |
\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}% |
171 |
\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}% |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
172 |
} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
173 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
174 |
\newcommand{\isabellestylesl}{% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
175 |
\isabellestyleit% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
176 |
\renewcommand{\isastyle}{\small\sl}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
177 |
\renewcommand{\isastyleminor}{\sl}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
178 |
\renewcommand{\isastylescript}{\footnotesize\sl}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
179 |
} |
17125 | 180 |
|
181 |
||
182 |
% tagged regions |
|
183 |
||
184 |
%plain TeX version of comment package -- much faster! |
|
185 |
\let\isafmtname\fmtname\def\fmtname{plain} |
|
186 |
\usepackage{comment} |
|
187 |
\let\fmtname\isafmtname |
|
188 |
||
189 |
\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}} |
|
190 |
||
191 |
\newcommand{\isakeeptag}[1]% |
|
192 |
{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}} |
|
193 |
\newcommand{\isadroptag}[1]% |
|
194 |
{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}} |
|
195 |
\newcommand{\isafoldtag}[1]% |
|
196 |
{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}} |
|
197 |
||
198 |
\isakeeptag{theory} |
|
199 |
\isakeeptag{proof} |
|
200 |
\isakeeptag{ML} |
|
201 |
\isakeeptag{visible} |
|
202 |
\isadroptag{invisible} |
|
203 |
||
204 |
\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{} |