author | wenzelm |
Fri, 06 May 2011 20:25:41 +0200 | |
changeset 42712 | 574613b47583 |
parent 42711 | 159c4d1d4c42 |
child 43321 | 0e79cd0b315f |
permissions | -rw-r--r-- |
7709 | 1 |
%% |
2 |
%% macros for Isabelle generated LaTeX output |
|
3 |
%% |
|
4 |
||
9913 | 5 |
%%% Simple document preparation (based on theory token language and symbols) |
7709 | 6 |
|
8714 | 7 |
% isabelle environments |
7788 | 8 |
|
9913 | 9 |
\newcommand{\isabellecontext}{UNKNOWN} |
10 |
||
18860
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
11 |
\newcommand{\isastyle}{\UNDEF} |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
12 |
\newcommand{\isastyleminor}{\UNDEF} |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
13 |
\newcommand{\isastylescript}{\UNDEF} |
9657 | 14 |
\newcommand{\isastyletext}{\normalsize\rm} |
15 |
\newcommand{\isastyletxt}{\rm} |
|
16 |
\newcommand{\isastylecmt}{\rm} |
|
8713 | 17 |
|
10220 | 18 |
%symbol markup -- \emph achieves decent spacing via italic corrections |
19 |
\newcommand{\isamath}[1]{\emph{$#1$}} |
|
20 |
\newcommand{\isatext}[1]{\emph{#1}} |
|
25055
3bb2ad8b1b37
DeclareRobustCommand isascriptstyle (enables sub/superscripts within section headings etc.);
wenzelm
parents:
22647
diff
changeset
|
21 |
\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}} |
17180
5fefe658a6f8
recover original definitions of \isactrlsub etc.;
wenzelm
parents:
17173
diff
changeset
|
22 |
\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} |
5fefe658a6f8
recover original definitions of \isactrlsub etc.;
wenzelm
parents:
17173
diff
changeset
|
23 |
\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} |
5fefe658a6f8
recover original definitions of \isactrlsub etc.;
wenzelm
parents:
17173
diff
changeset
|
24 |
\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} |
5fefe658a6f8
recover original definitions of \isactrlsub etc.;
wenzelm
parents:
17173
diff
changeset
|
25 |
\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} |
25081 | 26 |
\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isastylescript} |
27 |
\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup} |
|
28 |
\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isastylescript} |
|
29 |
\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup} |
|
11573 | 30 |
\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}} |
17173 | 31 |
\newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}} |
27337 | 32 |
|
22647 | 33 |
\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}} |
27337 | 34 |
\newcommand{\isaantiqopen}{\isakeyword{\isacharbraceleft}} |
35 |
\newcommand{\isaantiqclose}{\isakeyword{\isacharbraceright}} |
|
14332
fd3535af90ab
spanning super and sub scripts \<^bsub> .. \<^esub> and \<^bsup> .. \<^esup>
kleing
parents:
14234
diff
changeset
|
36 |
|
8713 | 37 |
\newdimen\isa@parindent\newdimen\isa@parskip |
9657 | 38 |
|
9702
f23bee3c0682
\newenvironment{isabellebody}: version without trivlist;
wenzelm
parents:
9688
diff
changeset
|
39 |
\newenvironment{isabellebody}{% |
11863
87643169ae7d
\newif\ifisamarkup controls spacing of isabeginpar;
wenzelm
parents:
11573
diff
changeset
|
40 |
\isamarkuptrue\par% |
9702
f23bee3c0682
\newenvironment{isabellebody}: version without trivlist;
wenzelm
parents:
9688
diff
changeset
|
41 |
\isa@parindent\parindent\parindent0pt% |
8713 | 42 |
\isa@parskip\parskip\parskip0pt% |
10470 | 43 |
\isastyle}{\par} |
9702
f23bee3c0682
\newenvironment{isabellebody}: version without trivlist;
wenzelm
parents:
9688
diff
changeset
|
44 |
|
f23bee3c0682
\newenvironment{isabellebody}: version without trivlist;
wenzelm
parents:
9688
diff
changeset
|
45 |
\newenvironment{isabelle} |
10422 | 46 |
{\begin{trivlist}\begin{isabellebody}\item\relax} |
47 |
{\end{isabellebody}\end{trivlist}} |
|
8713 | 48 |
|
9669 | 49 |
\newcommand{\isa}[1]{\emph{\isastyleminor #1}} |
8714 | 50 |
|
10949 | 51 |
\newcommand{\isaindent}[1]{\hphantom{#1}} |
13933 | 52 |
\newcommand{\isanewline}{\mbox{}\par\mbox{}} |
17158
d68bf267cbba
added \isachardoublequoteopen/close, \isacharbackquoteopen/close;
wenzelm
parents:
17052
diff
changeset
|
53 |
\newcommand{\isasep}{} |
9669 | 54 |
\newcommand{\isadigit}[1]{#1} |
7752 | 55 |
|
18860
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
56 |
\newcommand{\isachardefaults}{% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
57 |
\chardef\isacharbang=`\!% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
58 |
\chardef\isachardoublequote=`\"% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
59 |
\chardef\isachardoublequoteopen=`\"% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
60 |
\chardef\isachardoublequoteclose=`\"% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
61 |
\chardef\isacharhash=`\#% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
62 |
\chardef\isachardollar=`\$% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
63 |
\chardef\isacharpercent=`\%% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
64 |
\chardef\isacharampersand=`\&% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
65 |
\chardef\isacharprime=`\'% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
66 |
\chardef\isacharparenleft=`\(% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
67 |
\chardef\isacharparenright=`\)% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
68 |
\chardef\isacharasterisk=`\*% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
69 |
\chardef\isacharplus=`\+% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
70 |
\chardef\isacharcomma=`\,% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
71 |
\chardef\isacharminus=`\-% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
72 |
\chardef\isachardot=`\.% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
73 |
\chardef\isacharslash=`\/% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
74 |
\chardef\isacharcolon=`\:% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
75 |
\chardef\isacharsemicolon=`\;% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
76 |
\chardef\isacharless=`\<% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
77 |
\chardef\isacharequal=`\=% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
78 |
\chardef\isachargreater=`\>% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
79 |
\chardef\isacharquery=`\?% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
80 |
\chardef\isacharat=`\@% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
81 |
\chardef\isacharbrackleft=`\[% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
82 |
\chardef\isacharbackslash=`\\% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
83 |
\chardef\isacharbrackright=`\]% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
84 |
\chardef\isacharcircum=`\^% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
85 |
\chardef\isacharunderscore=`\_% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
86 |
\def\isacharunderscorekeyword{\_}% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
87 |
\chardef\isacharbackquote=`\`% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
88 |
\chardef\isacharbackquoteopen=`\`% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
89 |
\chardef\isacharbackquoteclose=`\`% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
90 |
\chardef\isacharbraceleft=`\{% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
91 |
\chardef\isacharbar=`\|% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
92 |
\chardef\isacharbraceright=`\}% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
93 |
\chardef\isachartilde=`\~% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
94 |
\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
95 |
\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
96 |
} |
7788 | 97 |
|
40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39662
diff
changeset
|
98 |
\newcommand{\isaliteral}[2]{#2} |
40407
2ff10e613689
more robust treatment of suppressed quotes concerning replacement text -- for improved copy/paste behaviour;
wenzelm
parents:
40402
diff
changeset
|
99 |
\newcommand{\isanil}{} |
40402
b646316f8b3c
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
wenzelm
parents:
39662
diff
changeset
|
100 |
|
7797 | 101 |
|
102 |
% keyword and section markup |
|
7788 | 103 |
|
9669 | 104 |
\newcommand{\isakeyword}[1] |
18860
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
105 |
{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}% |
9669 | 106 |
\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}} |
107 |
\newcommand{\isacommand}[1]{\isakeyword{#1}} |
|
7758 | 108 |
|
8501 | 109 |
\newcommand{\isamarkupheader}[1]{\section{#1}} |
7752 | 110 |
\newcommand{\isamarkupchapter}[1]{\chapter{#1}} |
111 |
\newcommand{\isamarkupsection}[1]{\section{#1}} |
|
112 |
\newcommand{\isamarkupsubsection}[1]{\subsection{#1}} |
|
113 |
\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}} |
|
114 |
\newcommand{\isamarkupsect}[1]{\section{#1}} |
|
115 |
\newcommand{\isamarkupsubsect}[1]{\subsection{#1}} |
|
116 |
\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}} |
|
8662
f9679ddbc492
isapar, isamarkuptext, isamarkuptxt turned into environments;
wenzelm
parents:
8512
diff
changeset
|
117 |
|
11863
87643169ae7d
\newif\ifisamarkup controls spacing of isabeginpar;
wenzelm
parents:
11573
diff
changeset
|
118 |
\newif\ifisamarkup |
87643169ae7d
\newif\ifisamarkup controls spacing of isabeginpar;
wenzelm
parents:
11573
diff
changeset
|
119 |
\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi} |
10586 | 120 |
\newcommand{\isaendpar}{\par\medskip} |
121 |
\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar} |
|
17215
8b969275a5d2
isamarkuptext/txt: \par before changing sizes prevents spacing anomaly;
wenzelm
parents:
17180
diff
changeset
|
122 |
\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}} |
8b969275a5d2
isamarkuptext/txt: \par before changing sizes prevents spacing anomaly;
wenzelm
parents:
17180
diff
changeset
|
123 |
\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}} |
9657 | 124 |
\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}} |
125 |
||
126 |
||
18860
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
127 |
% styles |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
128 |
|
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
129 |
\def\isabellestyle#1{\csname isabellestyle#1\endcsname} |
9657 | 130 |
|
18860
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
131 |
\newcommand{\isabellestyledefault}{% |
42514 | 132 |
\def\isastyle{\small\tt\slshape}% |
133 |
\def\isastyleminor{\small\tt\slshape}% |
|
134 |
\def\isastylescript{\footnotesize\tt\slshape}% |
|
18860
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
135 |
\isachardefaults% |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
136 |
} |
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
137 |
\isabellestyledefault |
9657 | 138 |
|
10024 | 139 |
\newcommand{\isabellestylett}{% |
42514 | 140 |
\def\isastyle{\small\tt}% |
141 |
\def\isastyleminor{\small\tt}% |
|
142 |
\def\isastylescript{\footnotesize\tt}% |
|
18860
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
143 |
\isachardefaults% |
10024 | 144 |
} |
18860
9089cdb4c5fd
all styles now reset to defaults first, i.e. the document may switch styles back and forth;
wenzelm
parents:
17531
diff
changeset
|
145 |
|
9669 | 146 |
\newcommand{\isabellestyleit}{% |
42514 | 147 |
\def\isastyle{\small\it}% |
148 |
\def\isastyleminor{\it}% |
|
149 |
\def\isastylescript{\footnotesize\it}% |
|
150 |
\isachardefaults% |
|
151 |
\def\isacharunderscorekeyword{\mbox{-}}% |
|
152 |
\def\isacharbang{\isamath{!}}% |
|
153 |
\def\isachardoublequote{\isanil}% |
|
154 |
\def\isachardoublequoteopen{\isanil}% |
|
155 |
\def\isachardoublequoteclose{\isanil}% |
|
156 |
\def\isacharhash{\isamath{\#}}% |
|
157 |
\def\isachardollar{\isamath{\$}}% |
|
158 |
\def\isacharpercent{\isamath{\%}}% |
|
159 |
\def\isacharampersand{\isamath{\&}}% |
|
160 |
\def\isacharprime{\isamath{\mskip2mu{'}\mskip-2mu}}% |
|
161 |
\def\isacharparenleft{\isamath{(}}% |
|
162 |
\def\isacharparenright{\isamath{)}}% |
|
163 |
\def\isacharasterisk{\isamath{*}}% |
|
164 |
\def\isacharplus{\isamath{+}}% |
|
165 |
\def\isacharcomma{\isamath{\mathord,}}% |
|
166 |
\def\isacharminus{\isamath{-}}% |
|
167 |
\def\isachardot{\isamath{\mathord.}}% |
|
168 |
\def\isacharslash{\isamath{/}}% |
|
169 |
\def\isacharcolon{\isamath{\mathord:}}% |
|
170 |
\def\isacharsemicolon{\isamath{\mathord;}}% |
|
171 |
\def\isacharless{\isamath{<}}% |
|
172 |
\def\isacharequal{\isamath{=}}% |
|
173 |
\def\isachargreater{\isamath{>}}% |
|
174 |
\def\isacharat{\isamath{@}}% |
|
175 |
\def\isacharbrackleft{\isamath{[}}% |
|
176 |
\def\isacharbackslash{\isamath{\backslash}}% |
|
177 |
\def\isacharbrackright{\isamath{]}}% |
|
178 |
\def\isacharunderscore{\mbox{-}}% |
|
179 |
\def\isacharbraceleft{\isamath{\{}}% |
|
180 |
\def\isacharbar{\isamath{\mid}}% |
|
181 |
\def\isacharbraceright{\isamath{\}}}% |
|
182 |
\def\isachartilde{\isamath{{}\sp{\sim}}}% |
|
183 |
\def\isacharbackquoteopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}% |
|
184 |
\def\isacharbackquoteclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}% |
|
185 |
\def\isacharverbatimopen{\isamath{\langle\!\langle}}% |
|
186 |
\def\isacharverbatimclose{\isamath{\rangle\!\rangle}}% |
|
9657 | 187 |
} |
188 |
||
42663
c31df4184ead
provide \isabellestyle{itunderscore} (requires underscore.sty);
wenzelm
parents:
42514
diff
changeset
|
189 |
\newcommand{\isabellestyleitunderscore}{% |
c31df4184ead
provide \isabellestyle{itunderscore} (requires underscore.sty);
wenzelm
parents:
42514
diff
changeset
|
190 |
\isabellestyleit% |
c31df4184ead
provide \isabellestyle{itunderscore} (requires underscore.sty);
wenzelm
parents:
42514
diff
changeset
|
191 |
\def\isacharunderscore{\_}% |
c31df4184ead
provide \isabellestyle{itunderscore} (requires underscore.sty);
wenzelm
parents:
42514
diff
changeset
|
192 |
\def\isacharunderscorekeyword{\_}% |
c31df4184ead
provide \isabellestyle{itunderscore} (requires underscore.sty);
wenzelm
parents:
42514
diff
changeset
|
193 |
} |
c31df4184ead
provide \isabellestyle{itunderscore} (requires underscore.sty);
wenzelm
parents:
42514
diff
changeset
|
194 |
|
9975 | 195 |
\newcommand{\isabellestylesl}{% |
196 |
\isabellestyleit% |
|
42514 | 197 |
\def\isastyle{\small\sl}% |
198 |
\def\isastyleminor{\sl}% |
|
199 |
\def\isastylescript{\footnotesize\sl}% |
|
9975 | 200 |
} |
17052 | 201 |
|
202 |
||
203 |
% tagged regions |
|
204 |
||
205 |
%plain TeX version of comment package -- much faster! |
|
206 |
\let\isafmtname\fmtname\def\fmtname{plain} |
|
207 |
\usepackage{comment} |
|
208 |
\let\fmtname\isafmtname |
|
209 |
||
210 |
\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}} |
|
211 |
||
212 |
\newcommand{\isakeeptag}[1]% |
|
213 |
{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}} |
|
214 |
\newcommand{\isadroptag}[1]% |
|
215 |
{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}} |
|
216 |
\newcommand{\isafoldtag}[1]% |
|
217 |
{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}} |
|
218 |
||
219 |
\isakeeptag{theory} |
|
220 |
\isakeeptag{proof} |
|
221 |
\isakeeptag{ML} |
|
222 |
\isakeeptag{visible} |
|
223 |
\isadroptag{invisible} |
|
224 |
||
225 |
\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{} |