1.1 --- a/doc-src/AxClass/Group/document/isabelle.sty Thu May 15 20:02:44 2008 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,215 +0,0 @@
1.4 -%%
1.5 -%%
1.6 -%%
1.7 -%% macros for Isabelle generated LaTeX output
1.8 -%%
1.9 -
1.10 -%%% Simple document preparation (based on theory token language and symbols)
1.11 -
1.12 -% isabelle environments
1.13 -
1.14 -\newcommand{\isabellecontext}{UNKNOWN}
1.15 -
1.16 -\newcommand{\isastyle}{\UNDEF}
1.17 -\newcommand{\isastyleminor}{\UNDEF}
1.18 -\newcommand{\isastylescript}{\UNDEF}
1.19 -\newcommand{\isastyletext}{\normalsize\rm}
1.20 -\newcommand{\isastyletxt}{\rm}
1.21 -\newcommand{\isastylecmt}{\rm}
1.22 -
1.23 -%symbol markup -- \emph achieves decent spacing via italic corrections
1.24 -\newcommand{\isamath}[1]{\emph{$#1$}}
1.25 -\newcommand{\isatext}[1]{\emph{#1}}
1.26 -\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
1.27 -\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
1.28 -\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
1.29 -\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
1.30 -\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
1.31 -\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isastylescript}
1.32 -\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
1.33 -\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isastylescript}
1.34 -\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
1.35 -\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
1.36 -\newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
1.37 -\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
1.38 -
1.39 -
1.40 -\newdimen\isa@parindent\newdimen\isa@parskip
1.41 -
1.42 -\newenvironment{isabellebody}{%
1.43 -\isamarkuptrue\par%
1.44 -\isa@parindent\parindent\parindent0pt%
1.45 -\isa@parskip\parskip\parskip0pt%
1.46 -\isastyle}{\par}
1.47 -
1.48 -\newenvironment{isabelle}
1.49 -{\begin{trivlist}\begin{isabellebody}\item\relax}
1.50 -{\end{isabellebody}\end{trivlist}}
1.51 -
1.52 -\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
1.53 -
1.54 -\newcommand{\isaindent}[1]{\hphantom{#1}}
1.55 -\newcommand{\isanewline}{\mbox{}\par\mbox{}}
1.56 -\newcommand{\isasep}{}
1.57 -\newcommand{\isadigit}[1]{#1}
1.58 -
1.59 -\newcommand{\isachardefaults}{%
1.60 -\chardef\isacharbang=`\!%
1.61 -\chardef\isachardoublequote=`\"%
1.62 -\chardef\isachardoublequoteopen=`\"%
1.63 -\chardef\isachardoublequoteclose=`\"%
1.64 -\chardef\isacharhash=`\#%
1.65 -\chardef\isachardollar=`\$%
1.66 -\chardef\isacharpercent=`\%%
1.67 -\chardef\isacharampersand=`\&%
1.68 -\chardef\isacharprime=`\'%
1.69 -\chardef\isacharparenleft=`\(%
1.70 -\chardef\isacharparenright=`\)%
1.71 -\chardef\isacharasterisk=`\*%
1.72 -\chardef\isacharplus=`\+%
1.73 -\chardef\isacharcomma=`\,%
1.74 -\chardef\isacharminus=`\-%
1.75 -\chardef\isachardot=`\.%
1.76 -\chardef\isacharslash=`\/%
1.77 -\chardef\isacharcolon=`\:%
1.78 -\chardef\isacharsemicolon=`\;%
1.79 -\chardef\isacharless=`\<%
1.80 -\chardef\isacharequal=`\=%
1.81 -\chardef\isachargreater=`\>%
1.82 -\chardef\isacharquery=`\?%
1.83 -\chardef\isacharat=`\@%
1.84 -\chardef\isacharbrackleft=`\[%
1.85 -\chardef\isacharbackslash=`\\%
1.86 -\chardef\isacharbrackright=`\]%
1.87 -\chardef\isacharcircum=`\^%
1.88 -\chardef\isacharunderscore=`\_%
1.89 -\def\isacharunderscorekeyword{\_}%
1.90 -\chardef\isacharbackquote=`\`%
1.91 -\chardef\isacharbackquoteopen=`\`%
1.92 -\chardef\isacharbackquoteclose=`\`%
1.93 -\chardef\isacharbraceleft=`\{%
1.94 -\chardef\isacharbar=`\|%
1.95 -\chardef\isacharbraceright=`\}%
1.96 -\chardef\isachartilde=`\~%
1.97 -\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
1.98 -\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
1.99 -}
1.100 -
1.101 -
1.102 -% keyword and section markup
1.103 -
1.104 -\newcommand{\isakeyword}[1]
1.105 -{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
1.106 -\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
1.107 -\newcommand{\isacommand}[1]{\isakeyword{#1}}
1.108 -
1.109 -\newcommand{\isamarkupheader}[1]{\section{#1}}
1.110 -\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
1.111 -\newcommand{\isamarkupsection}[1]{\section{#1}}
1.112 -\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
1.113 -\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
1.114 -\newcommand{\isamarkupsect}[1]{\section{#1}}
1.115 -\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
1.116 -\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
1.117 -
1.118 -\newif\ifisamarkup
1.119 -\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
1.120 -\newcommand{\isaendpar}{\par\medskip}
1.121 -\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
1.122 -\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
1.123 -\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
1.124 -\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
1.125 -
1.126 -
1.127 -% styles
1.128 -
1.129 -\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
1.130 -
1.131 -\newcommand{\isabellestyledefault}{%
1.132 -\renewcommand{\isastyle}{\small\tt\slshape}%
1.133 -\renewcommand{\isastyleminor}{\small\tt\slshape}%
1.134 -\renewcommand{\isastylescript}{\footnotesize\tt\slshape}%
1.135 -\isachardefaults%
1.136 -}
1.137 -\isabellestyledefault
1.138 -
1.139 -\newcommand{\isabellestylett}{%
1.140 -\renewcommand{\isastyle}{\small\tt}%
1.141 -\renewcommand{\isastyleminor}{\small\tt}%
1.142 -\renewcommand{\isastylescript}{\footnotesize\tt}%
1.143 -\isachardefaults%
1.144 -}
1.145 -
1.146 -\newcommand{\isabellestyleit}{%
1.147 -\renewcommand{\isastyle}{\small\it}%
1.148 -\renewcommand{\isastyleminor}{\it}%
1.149 -\renewcommand{\isastylescript}{\footnotesize\it}%
1.150 -\renewcommand{\isacharunderscorekeyword}{\mbox{-}}%
1.151 -\renewcommand{\isacharbang}{\isamath{!}}%
1.152 -\renewcommand{\isachardoublequote}{}%
1.153 -\renewcommand{\isachardoublequoteopen}{}%
1.154 -\renewcommand{\isachardoublequoteclose}{}%
1.155 -\renewcommand{\isacharhash}{\isamath{\#}}%
1.156 -\renewcommand{\isachardollar}{\isamath{\$}}%
1.157 -\renewcommand{\isacharpercent}{\isamath{\%}}%
1.158 -\renewcommand{\isacharampersand}{\isamath{\&}}%
1.159 -\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
1.160 -\renewcommand{\isacharparenleft}{\isamath{(}}%
1.161 -\renewcommand{\isacharparenright}{\isamath{)}}%
1.162 -\renewcommand{\isacharasterisk}{\isamath{*}}%
1.163 -\renewcommand{\isacharplus}{\isamath{+}}%
1.164 -\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
1.165 -\renewcommand{\isacharminus}{\isamath{-}}%
1.166 -\renewcommand{\isachardot}{\isamath{\mathord.}}%
1.167 -\renewcommand{\isacharslash}{\isamath{/}}%
1.168 -\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
1.169 -\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
1.170 -\renewcommand{\isacharless}{\isamath{<}}%
1.171 -\renewcommand{\isacharequal}{\isamath{=}}%
1.172 -\renewcommand{\isachargreater}{\isamath{>}}%
1.173 -\renewcommand{\isacharat}{\isamath{@}}%
1.174 -\renewcommand{\isacharbrackleft}{\isamath{[}}%
1.175 -\renewcommand{\isacharbackslash}{\isamath{\backslash}}%
1.176 -\renewcommand{\isacharbrackright}{\isamath{]}}%
1.177 -\renewcommand{\isacharunderscore}{\mbox{-}}%
1.178 -\renewcommand{\isacharbraceleft}{\isamath{\{}}%
1.179 -\renewcommand{\isacharbar}{\isamath{\mid}}%
1.180 -\renewcommand{\isacharbraceright}{\isamath{\}}}%
1.181 -\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
1.182 -\renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
1.183 -\renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
1.184 -\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}%
1.185 -\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}%
1.186 -}
1.187 -
1.188 -\newcommand{\isabellestylesl}{%
1.189 -\isabellestyleit%
1.190 -\renewcommand{\isastyle}{\small\sl}%
1.191 -\renewcommand{\isastyleminor}{\sl}%
1.192 -\renewcommand{\isastylescript}{\footnotesize\sl}%
1.193 -}
1.194 -
1.195 -
1.196 -% tagged regions
1.197 -
1.198 -%plain TeX version of comment package -- much faster!
1.199 -\let\isafmtname\fmtname\def\fmtname{plain}
1.200 -\usepackage{comment}
1.201 -\let\fmtname\isafmtname
1.202 -
1.203 -\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
1.204 -
1.205 -\newcommand{\isakeeptag}[1]%
1.206 -{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
1.207 -\newcommand{\isadroptag}[1]%
1.208 -{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
1.209 -\newcommand{\isafoldtag}[1]%
1.210 -{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
1.211 -
1.212 -\isakeeptag{theory}
1.213 -\isakeeptag{proof}
1.214 -\isakeeptag{ML}
1.215 -\isakeeptag{visible}
1.216 -\isadroptag{invisible}
1.217 -
1.218 -\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}
2.1 --- a/doc-src/AxClass/Group/document/isabellesym.sty Thu May 15 20:02:44 2008 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,360 +0,0 @@
2.4 -%%
2.5 -%%
2.6 -%%
2.7 -%% definitions of standard Isabelle symbols
2.8 -%%
2.9 -
2.10 -\newcommand{\isasymzero}{\isamath{\mathbf{0}}} %requires amssymb
2.11 -\newcommand{\isasymone}{\isamath{\mathbf{1}}} %requires amssymb
2.12 -\newcommand{\isasymtwo}{\isamath{\mathbf{2}}} %requires amssymb
2.13 -\newcommand{\isasymthree}{\isamath{\mathbf{3}}} %requires amssymb
2.14 -\newcommand{\isasymfour}{\isamath{\mathbf{4}}} %requires amssymb
2.15 -\newcommand{\isasymfive}{\isamath{\mathbf{5}}} %requires amssymb
2.16 -\newcommand{\isasymsix}{\isamath{\mathbf{6}}} %requires amssymb
2.17 -\newcommand{\isasymseven}{\isamath{\mathbf{7}}} %requires amssymb
2.18 -\newcommand{\isasymeight}{\isamath{\mathbf{8}}} %requires amssymb
2.19 -\newcommand{\isasymnine}{\isamath{\mathbf{9}}} %requires amssymb
2.20 -\newcommand{\isasymA}{\isamath{\mathcal{A}}}
2.21 -\newcommand{\isasymB}{\isamath{\mathcal{B}}}
2.22 -\newcommand{\isasymC}{\isamath{\mathcal{C}}}
2.23 -\newcommand{\isasymD}{\isamath{\mathcal{D}}}
2.24 -\newcommand{\isasymE}{\isamath{\mathcal{E}}}
2.25 -\newcommand{\isasymF}{\isamath{\mathcal{F}}}
2.26 -\newcommand{\isasymG}{\isamath{\mathcal{G}}}
2.27 -\newcommand{\isasymH}{\isamath{\mathcal{H}}}
2.28 -\newcommand{\isasymI}{\isamath{\mathcal{I}}}
2.29 -\newcommand{\isasymJ}{\isamath{\mathcal{J}}}
2.30 -\newcommand{\isasymK}{\isamath{\mathcal{K}}}
2.31 -\newcommand{\isasymL}{\isamath{\mathcal{L}}}
2.32 -\newcommand{\isasymM}{\isamath{\mathcal{M}}}
2.33 -\newcommand{\isasymN}{\isamath{\mathcal{N}}}
2.34 -\newcommand{\isasymO}{\isamath{\mathcal{O}}}
2.35 -\newcommand{\isasymP}{\isamath{\mathcal{P}}}
2.36 -\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}
2.37 -\newcommand{\isasymR}{\isamath{\mathcal{R}}}
2.38 -\newcommand{\isasymS}{\isamath{\mathcal{S}}}
2.39 -\newcommand{\isasymT}{\isamath{\mathcal{T}}}
2.40 -\newcommand{\isasymU}{\isamath{\mathcal{U}}}
2.41 -\newcommand{\isasymV}{\isamath{\mathcal{V}}}
2.42 -\newcommand{\isasymW}{\isamath{\mathcal{W}}}
2.43 -\newcommand{\isasymX}{\isamath{\mathcal{X}}}
2.44 -\newcommand{\isasymY}{\isamath{\mathcal{Y}}}
2.45 -\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
2.46 -\newcommand{\isasyma}{\isamath{\mathrm{a}}}
2.47 -\newcommand{\isasymb}{\isamath{\mathrm{b}}}
2.48 -\newcommand{\isasymc}{\isamath{\mathrm{c}}}
2.49 -\newcommand{\isasymd}{\isamath{\mathrm{d}}}
2.50 -\newcommand{\isasyme}{\isamath{\mathrm{e}}}
2.51 -\newcommand{\isasymf}{\isamath{\mathrm{f}}}
2.52 -\newcommand{\isasymg}{\isamath{\mathrm{g}}}
2.53 -\newcommand{\isasymh}{\isamath{\mathrm{h}}}
2.54 -\newcommand{\isasymi}{\isamath{\mathrm{i}}}
2.55 -\newcommand{\isasymj}{\isamath{\mathrm{j}}}
2.56 -\newcommand{\isasymk}{\isamath{\mathrm{k}}}
2.57 -\newcommand{\isasyml}{\isamath{\mathrm{l}}}
2.58 -\newcommand{\isasymm}{\isamath{\mathrm{m}}}
2.59 -\newcommand{\isasymn}{\isamath{\mathrm{n}}}
2.60 -\newcommand{\isasymo}{\isamath{\mathrm{o}}}
2.61 -\newcommand{\isasymp}{\isamath{\mathrm{p}}}
2.62 -\newcommand{\isasymq}{\isamath{\mathrm{q}}}
2.63 -\newcommand{\isasymr}{\isamath{\mathrm{r}}}
2.64 -\newcommand{\isasyms}{\isamath{\mathrm{s}}}
2.65 -\newcommand{\isasymt}{\isamath{\mathrm{t}}}
2.66 -\newcommand{\isasymu}{\isamath{\mathrm{u}}}
2.67 -\newcommand{\isasymv}{\isamath{\mathrm{v}}}
2.68 -\newcommand{\isasymw}{\isamath{\mathrm{w}}}
2.69 -\newcommand{\isasymx}{\isamath{\mathrm{x}}}
2.70 -\newcommand{\isasymy}{\isamath{\mathrm{y}}}
2.71 -\newcommand{\isasymz}{\isamath{\mathrm{z}}}
2.72 -\newcommand{\isasymAA}{\isamath{\mathfrak{A}}} %requires eufrak
2.73 -\newcommand{\isasymBB}{\isamath{\mathfrak{B}}} %requires eufrak
2.74 -\newcommand{\isasymCC}{\isamath{\mathfrak{C}}} %requires eufrak
2.75 -\newcommand{\isasymDD}{\isamath{\mathfrak{D}}} %requires eufrak
2.76 -\newcommand{\isasymEE}{\isamath{\mathfrak{E}}} %requires eufrak
2.77 -\newcommand{\isasymFF}{\isamath{\mathfrak{F}}} %requires eufrak
2.78 -\newcommand{\isasymGG}{\isamath{\mathfrak{G}}} %requires eufrak
2.79 -\newcommand{\isasymHH}{\isamath{\mathfrak{H}}} %requires eufrak
2.80 -\newcommand{\isasymII}{\isamath{\mathfrak{I}}} %requires eufrak
2.81 -\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}} %requires eufrak
2.82 -\newcommand{\isasymKK}{\isamath{\mathfrak{K}}} %requires eufrak
2.83 -\newcommand{\isasymLL}{\isamath{\mathfrak{L}}} %requires eufrak
2.84 -\newcommand{\isasymMM}{\isamath{\mathfrak{M}}} %requires eufrak
2.85 -\newcommand{\isasymNN}{\isamath{\mathfrak{N}}} %requires eufrak
2.86 -\newcommand{\isasymOO}{\isamath{\mathfrak{O}}} %requires eufrak
2.87 -\newcommand{\isasymPP}{\isamath{\mathfrak{P}}} %requires eufrak
2.88 -\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}} %requires eufrak
2.89 -\newcommand{\isasymRR}{\isamath{\mathfrak{R}}} %requires eufrak
2.90 -\newcommand{\isasymSS}{\isamath{\mathfrak{S}}} %requires eufrak
2.91 -\newcommand{\isasymTT}{\isamath{\mathfrak{T}}} %requires eufrak
2.92 -\newcommand{\isasymUU}{\isamath{\mathfrak{U}}} %requires eufrak
2.93 -\newcommand{\isasymVV}{\isamath{\mathfrak{V}}} %requires eufrak
2.94 -\newcommand{\isasymWW}{\isamath{\mathfrak{W}}} %requires eufrak
2.95 -\newcommand{\isasymXX}{\isamath{\mathfrak{X}}} %requires eufrak
2.96 -\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}} %requires eufrak
2.97 -\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}} %requires eufrak
2.98 -\newcommand{\isasymaa}{\isamath{\mathfrak{a}}} %requires eufrak
2.99 -\newcommand{\isasymbb}{\isamath{\mathfrak{b}}} %requires eufrak
2.100 -\newcommand{\isasymcc}{\isamath{\mathfrak{c}}} %requires eufrak
2.101 -\newcommand{\isasymdd}{\isamath{\mathfrak{d}}} %requires eufrak
2.102 -\newcommand{\isasymee}{\isamath{\mathfrak{e}}} %requires eufrak
2.103 -\newcommand{\isasymff}{\isamath{\mathfrak{f}}} %requires eufrak
2.104 -\newcommand{\isasymgg}{\isamath{\mathfrak{g}}} %requires eufrak
2.105 -\newcommand{\isasymhh}{\isamath{\mathfrak{h}}} %requires eufrak
2.106 -\newcommand{\isasymii}{\isamath{\mathfrak{i}}} %requires eufrak
2.107 -\newcommand{\isasymjj}{\isamath{\mathfrak{j}}} %requires eufrak
2.108 -\newcommand{\isasymkk}{\isamath{\mathfrak{k}}} %requires eufrak
2.109 -\newcommand{\isasymll}{\isamath{\mathfrak{l}}} %requires eufrak
2.110 -\newcommand{\isasymmm}{\isamath{\mathfrak{m}}} %requires eufrak
2.111 -\newcommand{\isasymnn}{\isamath{\mathfrak{n}}} %requires eufrak
2.112 -\newcommand{\isasymoo}{\isamath{\mathfrak{o}}} %requires eufrak
2.113 -\newcommand{\isasympp}{\isamath{\mathfrak{p}}} %requires eufrak
2.114 -\newcommand{\isasymqq}{\isamath{\mathfrak{q}}} %requires eufrak
2.115 -\newcommand{\isasymrr}{\isamath{\mathfrak{r}}} %requires eufrak
2.116 -\newcommand{\isasymss}{\isamath{\mathfrak{s}}} %requires eufrak
2.117 -\newcommand{\isasymtt}{\isamath{\mathfrak{t}}} %requires eufrak
2.118 -\newcommand{\isasymuu}{\isamath{\mathfrak{u}}} %requires eufrak
2.119 -\newcommand{\isasymvv}{\isamath{\mathfrak{v}}} %requires eufrak
2.120 -\newcommand{\isasymww}{\isamath{\mathfrak{w}}} %requires eufrak
2.121 -\newcommand{\isasymxx}{\isamath{\mathfrak{x}}} %requires eufrak
2.122 -\newcommand{\isasymyy}{\isamath{\mathfrak{y}}} %requires eufrak
2.123 -\newcommand{\isasymzz}{\isamath{\mathfrak{z}}} %requires eufrak
2.124 -\newcommand{\isasymalpha}{\isamath{\alpha}}
2.125 -\newcommand{\isasymbeta}{\isamath{\beta}}
2.126 -\newcommand{\isasymgamma}{\isamath{\gamma}}
2.127 -\newcommand{\isasymdelta}{\isamath{\delta}}
2.128 -\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
2.129 -\newcommand{\isasymzeta}{\isamath{\zeta}}
2.130 -\newcommand{\isasymeta}{\isamath{\eta}}
2.131 -\newcommand{\isasymtheta}{\isamath{\vartheta}}
2.132 -\newcommand{\isasymiota}{\isamath{\iota}}
2.133 -\newcommand{\isasymkappa}{\isamath{\kappa}}
2.134 -\newcommand{\isasymlambda}{\isamath{\lambda}}
2.135 -\newcommand{\isasymmu}{\isamath{\mu}}
2.136 -\newcommand{\isasymnu}{\isamath{\nu}}
2.137 -\newcommand{\isasymxi}{\isamath{\xi}}
2.138 -\newcommand{\isasympi}{\isamath{\pi}}
2.139 -\newcommand{\isasymrho}{\isamath{\varrho}}
2.140 -\newcommand{\isasymsigma}{\isamath{\sigma}}
2.141 -\newcommand{\isasymtau}{\isamath{\tau}}
2.142 -\newcommand{\isasymupsilon}{\isamath{\upsilon}}
2.143 -\newcommand{\isasymphi}{\isamath{\varphi}}
2.144 -\newcommand{\isasymchi}{\isamath{\chi}}
2.145 -\newcommand{\isasympsi}{\isamath{\psi}}
2.146 -\newcommand{\isasymomega}{\isamath{\omega}}
2.147 -\newcommand{\isasymGamma}{\isamath{\Gamma}}
2.148 -\newcommand{\isasymDelta}{\isamath{\Delta}}
2.149 -\newcommand{\isasymTheta}{\isamath{\Theta}}
2.150 -\newcommand{\isasymLambda}{\isamath{\Lambda}}
2.151 -\newcommand{\isasymXi}{\isamath{\Xi}}
2.152 -\newcommand{\isasymPi}{\isamath{\Pi}}
2.153 -\newcommand{\isasymSigma}{\isamath{\Sigma}}
2.154 -\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
2.155 -\newcommand{\isasymPhi}{\isamath{\Phi}}
2.156 -\newcommand{\isasymPsi}{\isamath{\Psi}}
2.157 -\newcommand{\isasymOmega}{\isamath{\Omega}}
2.158 -\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
2.159 -\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
2.160 -\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
2.161 -\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
2.162 -\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
2.163 -\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
2.164 -\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
2.165 -\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
2.166 -\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
2.167 -\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
2.168 -\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
2.169 -\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
2.170 -\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
2.171 -\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
2.172 -\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
2.173 -\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
2.174 -\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
2.175 -\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
2.176 -\newcommand{\isasymmapsto}{\isamath{\mapsto}}
2.177 -\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
2.178 -\newcommand{\isasymmidarrow}{\isamath{\relbar}}
2.179 -\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
2.180 -\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
2.181 -\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
2.182 -\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
2.183 -\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
2.184 -\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
2.185 -\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
2.186 -\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
2.187 -\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
2.188 -\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}} %requires amssymb
2.189 -\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}} %requires amssymb
2.190 -\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}} %requires amssymb
2.191 -\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}} %requires amssymb
2.192 -\newcommand{\isasymrestriction}{\isamath{\restriction}} %requires amssymb
2.193 -\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
2.194 -\newcommand{\isasymup}{\isamath{\uparrow}}
2.195 -\newcommand{\isasymUp}{\isamath{\Uparrow}}
2.196 -\newcommand{\isasymdown}{\isamath{\downarrow}}
2.197 -\newcommand{\isasymDown}{\isamath{\Downarrow}}
2.198 -\newcommand{\isasymupdown}{\isamath{\updownarrow}}
2.199 -\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
2.200 -\newcommand{\isasymlangle}{\isamath{\langle}}
2.201 -\newcommand{\isasymrangle}{\isamath{\rangle}}
2.202 -\newcommand{\isasymlceil}{\isamath{\lceil}}
2.203 -\newcommand{\isasymrceil}{\isamath{\rceil}}
2.204 -\newcommand{\isasymlfloor}{\isamath{\lfloor}}
2.205 -\newcommand{\isasymrfloor}{\isamath{\rfloor}}
2.206 -\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
2.207 -\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}
2.208 -\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
2.209 -\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
2.210 -\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
2.211 -\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
2.212 -\newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel
2.213 -\newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel
2.214 -\newcommand{\isasymbottom}{\isamath{\bot}}
2.215 -\newcommand{\isasymtop}{\isamath{\top}}
2.216 -\newcommand{\isasymand}{\isamath{\wedge}}
2.217 -\newcommand{\isasymAnd}{\isamath{\bigwedge}}
2.218 -\newcommand{\isasymor}{\isamath{\vee}}
2.219 -\newcommand{\isasymOr}{\isamath{\bigvee}}
2.220 -\newcommand{\isasymforall}{\isamath{\forall\,}}
2.221 -\newcommand{\isasymexists}{\isamath{\exists\,}}
2.222 -\newcommand{\isasymnexists}{\isamath{\nexists\,}} %requires amssymb
2.223 -\newcommand{\isasymnot}{\isamath{\neg}}
2.224 -\newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb
2.225 -\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb
2.226 -\newcommand{\isasymturnstile}{\isamath{\vdash}}
2.227 -\newcommand{\isasymTurnstile}{\isamath{\models}}
2.228 -\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
2.229 -\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
2.230 -\newcommand{\isasymstileturn}{\isamath{\dashv}}
2.231 -\newcommand{\isasymsurd}{\isamath{\surd}}
2.232 -\newcommand{\isasymle}{\isamath{\le}}
2.233 -\newcommand{\isasymge}{\isamath{\ge}}
2.234 -\newcommand{\isasymlless}{\isamath{\ll}}
2.235 -\newcommand{\isasymggreater}{\isamath{\gg}}
2.236 -\newcommand{\isasymlesssim}{\isamath{\lesssim}} %requires amssymb
2.237 -\newcommand{\isasymgreatersim}{\isamath{\gtrsim}} %requires amssymb
2.238 -\newcommand{\isasymlessapprox}{\isamath{\lessapprox}} %requires amssymb
2.239 -\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}} %requires amssymb
2.240 -\newcommand{\isasymin}{\isamath{\in}}
2.241 -\newcommand{\isasymnotin}{\isamath{\notin}}
2.242 -\newcommand{\isasymsubset}{\isamath{\subset}}
2.243 -\newcommand{\isasymsupset}{\isamath{\supset}}
2.244 -\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
2.245 -\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
2.246 -\newcommand{\isasymsqsubset}{\isamath{\sqsubset}} %requires amssymb
2.247 -\newcommand{\isasymsqsupset}{\isamath{\sqsupset}} %requires amssymb
2.248 -\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
2.249 -\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
2.250 -\newcommand{\isasyminter}{\isamath{\cap}}
2.251 -\newcommand{\isasymInter}{\isamath{\bigcap\,}}
2.252 -\newcommand{\isasymunion}{\isamath{\cup}}
2.253 -\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
2.254 -\newcommand{\isasymsqunion}{\isamath{\sqcup}}
2.255 -\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
2.256 -\newcommand{\isasymsqinter}{\isamath{\sqcap}}
2.257 -\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires amsmath
2.258 -\newcommand{\isasymsetminus}{\isamath{\setminus}}
2.259 -\newcommand{\isasympropto}{\isamath{\propto}}
2.260 -\newcommand{\isasymuplus}{\isamath{\uplus}}
2.261 -\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
2.262 -\newcommand{\isasymnoteq}{\isamath{\not=}}
2.263 -\newcommand{\isasymsim}{\isamath{\sim}}
2.264 -\newcommand{\isasymdoteq}{\isamath{\doteq}}
2.265 -\newcommand{\isasymsimeq}{\isamath{\simeq}}
2.266 -\newcommand{\isasymapprox}{\isamath{\approx}}
2.267 -\newcommand{\isasymasymp}{\isamath{\asymp}}
2.268 -\newcommand{\isasymcong}{\isamath{\cong}}
2.269 -\newcommand{\isasymsmile}{\isamath{\smile}}
2.270 -\newcommand{\isasymequiv}{\isamath{\equiv}}
2.271 -\newcommand{\isasymfrown}{\isamath{\frown}}
2.272 -\newcommand{\isasymJoin}{\isamath{\Join}} %requires amssymb
2.273 -\newcommand{\isasymbowtie}{\isamath{\bowtie}}
2.274 -\newcommand{\isasymprec}{\isamath{\prec}}
2.275 -\newcommand{\isasymsucc}{\isamath{\succ}}
2.276 -\newcommand{\isasympreceq}{\isamath{\preceq}}
2.277 -\newcommand{\isasymsucceq}{\isamath{\succeq}}
2.278 -\newcommand{\isasymparallel}{\isamath{\parallel}}
2.279 -\newcommand{\isasymbar}{\isamath{\mid}}
2.280 -\newcommand{\isasymplusminus}{\isamath{\pm}}
2.281 -\newcommand{\isasymminusplus}{\isamath{\mp}}
2.282 -\newcommand{\isasymtimes}{\isamath{\times}}
2.283 -\newcommand{\isasymdiv}{\isamath{\div}}
2.284 -\newcommand{\isasymcdot}{\isamath{\cdot}}
2.285 -\newcommand{\isasymstar}{\isamath{\star}}
2.286 -\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
2.287 -\newcommand{\isasymcirc}{\isamath{\circ}}
2.288 -\newcommand{\isasymdagger}{\isamath{\dagger}}
2.289 -\newcommand{\isasymddagger}{\isamath{\ddagger}}
2.290 -\newcommand{\isasymlhd}{\isamath{\lhd}} %requires amssymb
2.291 -\newcommand{\isasymrhd}{\isamath{\rhd}} %requires amssymb
2.292 -\newcommand{\isasymunlhd}{\isamath{\unlhd}} %requires amssymb
2.293 -\newcommand{\isasymunrhd}{\isamath{\unrhd}} %requires amssymb
2.294 -\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
2.295 -\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
2.296 -\newcommand{\isasymtriangle}{\isamath{\triangle}}
2.297 -\newcommand{\isasymtriangleq}{\isamath{\triangleq}} %requires amssymb
2.298 -\newcommand{\isasymoplus}{\isamath{\oplus}}
2.299 -\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}
2.300 -\newcommand{\isasymotimes}{\isamath{\otimes}}
2.301 -\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}
2.302 -\newcommand{\isasymodot}{\isamath{\odot}}
2.303 -\newcommand{\isasymOdot}{\isamath{\bigodot\,}}
2.304 -\newcommand{\isasymominus}{\isamath{\ominus}}
2.305 -\newcommand{\isasymoslash}{\isamath{\oslash}}
2.306 -\newcommand{\isasymdots}{\isamath{\dots}}
2.307 -\newcommand{\isasymcdots}{\isamath{\cdots}}
2.308 -\newcommand{\isasymSum}{\isamath{\sum\,}}
2.309 -\newcommand{\isasymProd}{\isamath{\prod\,}}
2.310 -\newcommand{\isasymCoprod}{\isamath{\coprod\,}}
2.311 -\newcommand{\isasyminfinity}{\isamath{\infty}}
2.312 -\newcommand{\isasymintegral}{\isamath{\int\,}}
2.313 -\newcommand{\isasymointegral}{\isamath{\oint\,}}
2.314 -\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
2.315 -\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
2.316 -\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
2.317 -\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
2.318 -\newcommand{\isasymaleph}{\isamath{\aleph}}
2.319 -\newcommand{\isasymemptyset}{\isamath{\emptyset}}
2.320 -\newcommand{\isasymnabla}{\isamath{\nabla}}
2.321 -\newcommand{\isasympartial}{\isamath{\partial}}
2.322 -\newcommand{\isasymRe}{\isamath{\Re}}
2.323 -\newcommand{\isasymIm}{\isamath{\Im}}
2.324 -\newcommand{\isasymflat}{\isamath{\flat}}
2.325 -\newcommand{\isasymnatural}{\isamath{\natural}}
2.326 -\newcommand{\isasymsharp}{\isamath{\sharp}}
2.327 -\newcommand{\isasymangle}{\isamath{\angle}}
2.328 -\newcommand{\isasymcopyright}{\isatext{\rm\copyright}}
2.329 -\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
2.330 -\newcommand{\isasymhyphen}{\isatext{\rm-}}
2.331 -\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
2.332 -\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}} %requires latin1
2.333 -\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}} %requires latin1
2.334 -\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}} %requires latin1
2.335 -\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}} %requires latin1
2.336 -\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}} %requires latin1
2.337 -\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}} %requires latin1
2.338 -\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
2.339 -\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
2.340 -\newcommand{\isasymsection}{\isatext{\rm\S}}
2.341 -\newcommand{\isasymparagraph}{\isatext{\rm\P}}
2.342 -\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
2.343 -\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
2.344 -\newcommand{\isasymeuro}{\isatext{\textgreek{\euro}}} %requires greek babel
2.345 -\newcommand{\isasympounds}{\isamath{\pounds}}
2.346 -\newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb
2.347 -\newcommand{\isasymcent}{\isatext{\textcent}} %requires textcomp
2.348 -\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
2.349 -\newcommand{\isasymdegree}{\isatext{\rm\textdegree}} %requires latin1
2.350 -\newcommand{\isasymamalg}{\isamath{\amalg}}
2.351 -\newcommand{\isasymmho}{\isamath{\mho}} %requires amssymb
2.352 -\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssymb
2.353 -\newcommand{\isasymwp}{\isamath{\wp}}
2.354 -\newcommand{\isasymwrong}{\isamath{\wr}}
2.355 -\newcommand{\isasymstruct}{\isamath{\diamond}}
2.356 -\newcommand{\isasymacute}{\isatext{\'\relax}}
2.357 -\newcommand{\isasymindex}{\isatext{\i}}
2.358 -\newcommand{\isasymdieresis}{\isatext{\"\relax}}
2.359 -\newcommand{\isasymcedilla}{\isatext{\c\relax}}
2.360 -\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
2.361 -\newcommand{\isasymspacespace}{\isamath{~~}}
2.362 -\newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}
2.363 -\newcommand{\isasymsome}{\isamath{\epsilon\,}}
3.1 --- a/doc-src/AxClass/Makefile Thu May 15 20:02:44 2008 +0200
3.2 +++ b/doc-src/AxClass/Makefile Thu May 15 20:14:10 2008 +0200
3.3 @@ -13,8 +13,9 @@
3.4
3.5 NAME = axclass
3.6
3.7 -FILES = axclass.tex body.tex ../iman.sty ../extra.sty ../isar.sty \
3.8 - ../pdfsetup.sty Group/document/Group.tex Nat/document/NatClass.tex \
3.9 +FILES = axclass.tex body.tex ../iman.sty ../extra.sty ../isar.sty \
3.10 + ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty \
3.11 + Group/document/Group.tex Nat/document/NatClass.tex \
3.12 Group/document/Product.tex Group/document/Semigroups.tex
3.13
3.14 dvi: $(NAME).dvi
4.1 --- a/doc-src/AxClass/axclass.tex Thu May 15 20:02:44 2008 +0200
4.2 +++ b/doc-src/AxClass/axclass.tex Thu May 15 20:14:10 2008 +0200
4.3 @@ -1,7 +1,7 @@
4.4
4.5 \documentclass[12pt,a4paper,fleqn]{report}
4.6 \usepackage{graphicx,../iman,../extra,../isar}
4.7 -\usepackage{Group/document/isabelle,Group/document/isabellesym}
4.8 +\usepackage{../isabelle,../isabellesym}
4.9 \usepackage{../pdfsetup} % last one!
4.10
4.11 \isabellestyle{it}
5.1 --- a/doc-src/IsarOverview/Isar/document/Makefile Thu May 15 20:02:44 2008 +0200
5.2 +++ b/doc-src/IsarOverview/Isar/document/Makefile Thu May 15 20:14:10 2008 +0200
5.3 @@ -12,7 +12,7 @@
5.4
5.5 dvi: ../../isar-overview.dvi
5.6
5.7 -../../isar-overview.dvi: *.tex *.sty *.bib
5.8 +../../isar-overview.dvi: *.tex *.bib
5.9 $(LATEX) root
5.10 $(BIBTEX) root
5.11 $(LATEX) root
5.12 @@ -21,7 +21,7 @@
5.13
5.14 pdf: ../../isar-overview.pdf
5.15
5.16 -../../isar-overview.pdf: *.tex *.sty *.bib
5.17 +../../isar-overview.pdf: *.tex *.bib
5.18 $(PDFLATEX) root
5.19 $(BIBTEX) root
5.20 $(PDFLATEX) root
6.1 --- a/doc-src/IsarOverview/Isar/document/isabelle.sty Thu May 15 20:02:44 2008 +0200
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,215 +0,0 @@
6.4 -%%
6.5 -%%
6.6 -%%
6.7 -%% macros for Isabelle generated LaTeX output
6.8 -%%
6.9 -
6.10 -%%% Simple document preparation (based on theory token language and symbols)
6.11 -
6.12 -% isabelle environments
6.13 -
6.14 -\newcommand{\isabellecontext}{UNKNOWN}
6.15 -
6.16 -\newcommand{\isastyle}{\UNDEF}
6.17 -\newcommand{\isastyleminor}{\UNDEF}
6.18 -\newcommand{\isastylescript}{\UNDEF}
6.19 -\newcommand{\isastyletext}{\normalsize\rm}
6.20 -\newcommand{\isastyletxt}{\rm}
6.21 -\newcommand{\isastylecmt}{\rm}
6.22 -
6.23 -%symbol markup -- \emph achieves decent spacing via italic corrections
6.24 -\newcommand{\isamath}[1]{\emph{$#1$}}
6.25 -\newcommand{\isatext}[1]{\emph{#1}}
6.26 -\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
6.27 -\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
6.28 -\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
6.29 -\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
6.30 -\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
6.31 -\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isastylescript}
6.32 -\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
6.33 -\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isastylescript}
6.34 -\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
6.35 -\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
6.36 -\newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
6.37 -\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
6.38 -
6.39 -
6.40 -\newdimen\isa@parindent\newdimen\isa@parskip
6.41 -
6.42 -\newenvironment{isabellebody}{%
6.43 -\isamarkuptrue\par%
6.44 -\isa@parindent\parindent\parindent0pt%
6.45 -\isa@parskip\parskip\parskip0pt%
6.46 -\isastyle}{\par}
6.47 -
6.48 -\newenvironment{isabelle}
6.49 -{\begin{trivlist}\begin{isabellebody}\item\relax}
6.50 -{\end{isabellebody}\end{trivlist}}
6.51 -
6.52 -\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
6.53 -
6.54 -\newcommand{\isaindent}[1]{\hphantom{#1}}
6.55 -\newcommand{\isanewline}{\mbox{}\par\mbox{}}
6.56 -\newcommand{\isasep}{}
6.57 -\newcommand{\isadigit}[1]{#1}
6.58 -
6.59 -\newcommand{\isachardefaults}{%
6.60 -\chardef\isacharbang=`\!%
6.61 -\chardef\isachardoublequote=`\"%
6.62 -\chardef\isachardoublequoteopen=`\"%
6.63 -\chardef\isachardoublequoteclose=`\"%
6.64 -\chardef\isacharhash=`\#%
6.65 -\chardef\isachardollar=`\$%
6.66 -\chardef\isacharpercent=`\%%
6.67 -\chardef\isacharampersand=`\&%
6.68 -\chardef\isacharprime=`\'%
6.69 -\chardef\isacharparenleft=`\(%
6.70 -\chardef\isacharparenright=`\)%
6.71 -\chardef\isacharasterisk=`\*%
6.72 -\chardef\isacharplus=`\+%
6.73 -\chardef\isacharcomma=`\,%
6.74 -\chardef\isacharminus=`\-%
6.75 -\chardef\isachardot=`\.%
6.76 -\chardef\isacharslash=`\/%
6.77 -\chardef\isacharcolon=`\:%
6.78 -\chardef\isacharsemicolon=`\;%
6.79 -\chardef\isacharless=`\<%
6.80 -\chardef\isacharequal=`\=%
6.81 -\chardef\isachargreater=`\>%
6.82 -\chardef\isacharquery=`\?%
6.83 -\chardef\isacharat=`\@%
6.84 -\chardef\isacharbrackleft=`\[%
6.85 -\chardef\isacharbackslash=`\\%
6.86 -\chardef\isacharbrackright=`\]%
6.87 -\chardef\isacharcircum=`\^%
6.88 -\chardef\isacharunderscore=`\_%
6.89 -\def\isacharunderscorekeyword{\_}%
6.90 -\chardef\isacharbackquote=`\`%
6.91 -\chardef\isacharbackquoteopen=`\`%
6.92 -\chardef\isacharbackquoteclose=`\`%
6.93 -\chardef\isacharbraceleft=`\{%
6.94 -\chardef\isacharbar=`\|%
6.95 -\chardef\isacharbraceright=`\}%
6.96 -\chardef\isachartilde=`\~%
6.97 -\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
6.98 -\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
6.99 -}
6.100 -
6.101 -
6.102 -% keyword and section markup
6.103 -
6.104 -\newcommand{\isakeyword}[1]
6.105 -{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
6.106 -\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
6.107 -\newcommand{\isacommand}[1]{\isakeyword{#1}}
6.108 -
6.109 -\newcommand{\isamarkupheader}[1]{\section{#1}}
6.110 -\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
6.111 -\newcommand{\isamarkupsection}[1]{\section{#1}}
6.112 -\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
6.113 -\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
6.114 -\newcommand{\isamarkupsect}[1]{\section{#1}}
6.115 -\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
6.116 -\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
6.117 -
6.118 -\newif\ifisamarkup
6.119 -\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
6.120 -\newcommand{\isaendpar}{\par\medskip}
6.121 -\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
6.122 -\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
6.123 -\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
6.124 -\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
6.125 -
6.126 -
6.127 -% styles
6.128 -
6.129 -\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
6.130 -
6.131 -\newcommand{\isabellestyledefault}{%
6.132 -\renewcommand{\isastyle}{\small\tt\slshape}%
6.133 -\renewcommand{\isastyleminor}{\small\tt\slshape}%
6.134 -\renewcommand{\isastylescript}{\footnotesize\tt\slshape}%
6.135 -\isachardefaults%
6.136 -}
6.137 -\isabellestyledefault
6.138 -
6.139 -\newcommand{\isabellestylett}{%
6.140 -\renewcommand{\isastyle}{\small\tt}%
6.141 -\renewcommand{\isastyleminor}{\small\tt}%
6.142 -\renewcommand{\isastylescript}{\footnotesize\tt}%
6.143 -\isachardefaults%
6.144 -}
6.145 -
6.146 -\newcommand{\isabellestyleit}{%
6.147 -\renewcommand{\isastyle}{\small\it}%
6.148 -\renewcommand{\isastyleminor}{\it}%
6.149 -\renewcommand{\isastylescript}{\footnotesize\it}%
6.150 -\renewcommand{\isacharunderscorekeyword}{\mbox{-}}%
6.151 -\renewcommand{\isacharbang}{\isamath{!}}%
6.152 -\renewcommand{\isachardoublequote}{}%
6.153 -\renewcommand{\isachardoublequoteopen}{}%
6.154 -\renewcommand{\isachardoublequoteclose}{}%
6.155 -\renewcommand{\isacharhash}{\isamath{\#}}%
6.156 -\renewcommand{\isachardollar}{\isamath{\$}}%
6.157 -\renewcommand{\isacharpercent}{\isamath{\%}}%
6.158 -\renewcommand{\isacharampersand}{\isamath{\&}}%
6.159 -\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
6.160 -\renewcommand{\isacharparenleft}{\isamath{(}}%
6.161 -\renewcommand{\isacharparenright}{\isamath{)}}%
6.162 -\renewcommand{\isacharasterisk}{\isamath{*}}%
6.163 -\renewcommand{\isacharplus}{\isamath{+}}%
6.164 -\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
6.165 -\renewcommand{\isacharminus}{\isamath{-}}%
6.166 -\renewcommand{\isachardot}{\isamath{\mathord.}}%
6.167 -\renewcommand{\isacharslash}{\isamath{/}}%
6.168 -\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
6.169 -\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
6.170 -\renewcommand{\isacharless}{\isamath{<}}%
6.171 -\renewcommand{\isacharequal}{\isamath{=}}%
6.172 -\renewcommand{\isachargreater}{\isamath{>}}%
6.173 -\renewcommand{\isacharat}{\isamath{@}}%
6.174 -\renewcommand{\isacharbrackleft}{\isamath{[}}%
6.175 -\renewcommand{\isacharbackslash}{\isamath{\backslash}}%
6.176 -\renewcommand{\isacharbrackright}{\isamath{]}}%
6.177 -\renewcommand{\isacharunderscore}{\mbox{-}}%
6.178 -\renewcommand{\isacharbraceleft}{\isamath{\{}}%
6.179 -\renewcommand{\isacharbar}{\isamath{\mid}}%
6.180 -\renewcommand{\isacharbraceright}{\isamath{\}}}%
6.181 -\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
6.182 -\renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
6.183 -\renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
6.184 -\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}%
6.185 -\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}%
6.186 -}
6.187 -
6.188 -\newcommand{\isabellestylesl}{%
6.189 -\isabellestyleit%
6.190 -\renewcommand{\isastyle}{\small\sl}%
6.191 -\renewcommand{\isastyleminor}{\sl}%
6.192 -\renewcommand{\isastylescript}{\footnotesize\sl}%
6.193 -}
6.194 -
6.195 -
6.196 -% tagged regions
6.197 -
6.198 -%plain TeX version of comment package -- much faster!
6.199 -\let\isafmtname\fmtname\def\fmtname{plain}
6.200 -\usepackage{comment}
6.201 -\let\fmtname\isafmtname
6.202 -
6.203 -\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
6.204 -
6.205 -\newcommand{\isakeeptag}[1]%
6.206 -{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
6.207 -\newcommand{\isadroptag}[1]%
6.208 -{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
6.209 -\newcommand{\isafoldtag}[1]%
6.210 -{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
6.211 -
6.212 -\isakeeptag{theory}
6.213 -\isakeeptag{proof}
6.214 -\isakeeptag{ML}
6.215 -\isakeeptag{visible}
6.216 -\isadroptag{invisible}
6.217 -
6.218 -\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}
7.1 --- a/doc-src/IsarOverview/Isar/document/isabellesym.sty Thu May 15 20:02:44 2008 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,360 +0,0 @@
7.4 -%%
7.5 -%%
7.6 -%%
7.7 -%% definitions of standard Isabelle symbols
7.8 -%%
7.9 -
7.10 -\newcommand{\isasymzero}{\isamath{\mathbf{0}}} %requires amssymb
7.11 -\newcommand{\isasymone}{\isamath{\mathbf{1}}} %requires amssymb
7.12 -\newcommand{\isasymtwo}{\isamath{\mathbf{2}}} %requires amssymb
7.13 -\newcommand{\isasymthree}{\isamath{\mathbf{3}}} %requires amssymb
7.14 -\newcommand{\isasymfour}{\isamath{\mathbf{4}}} %requires amssymb
7.15 -\newcommand{\isasymfive}{\isamath{\mathbf{5}}} %requires amssymb
7.16 -\newcommand{\isasymsix}{\isamath{\mathbf{6}}} %requires amssymb
7.17 -\newcommand{\isasymseven}{\isamath{\mathbf{7}}} %requires amssymb
7.18 -\newcommand{\isasymeight}{\isamath{\mathbf{8}}} %requires amssymb
7.19 -\newcommand{\isasymnine}{\isamath{\mathbf{9}}} %requires amssymb
7.20 -\newcommand{\isasymA}{\isamath{\mathcal{A}}}
7.21 -\newcommand{\isasymB}{\isamath{\mathcal{B}}}
7.22 -\newcommand{\isasymC}{\isamath{\mathcal{C}}}
7.23 -\newcommand{\isasymD}{\isamath{\mathcal{D}}}
7.24 -\newcommand{\isasymE}{\isamath{\mathcal{E}}}
7.25 -\newcommand{\isasymF}{\isamath{\mathcal{F}}}
7.26 -\newcommand{\isasymG}{\isamath{\mathcal{G}}}
7.27 -\newcommand{\isasymH}{\isamath{\mathcal{H}}}
7.28 -\newcommand{\isasymI}{\isamath{\mathcal{I}}}
7.29 -\newcommand{\isasymJ}{\isamath{\mathcal{J}}}
7.30 -\newcommand{\isasymK}{\isamath{\mathcal{K}}}
7.31 -\newcommand{\isasymL}{\isamath{\mathcal{L}}}
7.32 -\newcommand{\isasymM}{\isamath{\mathcal{M}}}
7.33 -\newcommand{\isasymN}{\isamath{\mathcal{N}}}
7.34 -\newcommand{\isasymO}{\isamath{\mathcal{O}}}
7.35 -\newcommand{\isasymP}{\isamath{\mathcal{P}}}
7.36 -\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}
7.37 -\newcommand{\isasymR}{\isamath{\mathcal{R}}}
7.38 -\newcommand{\isasymS}{\isamath{\mathcal{S}}}
7.39 -\newcommand{\isasymT}{\isamath{\mathcal{T}}}
7.40 -\newcommand{\isasymU}{\isamath{\mathcal{U}}}
7.41 -\newcommand{\isasymV}{\isamath{\mathcal{V}}}
7.42 -\newcommand{\isasymW}{\isamath{\mathcal{W}}}
7.43 -\newcommand{\isasymX}{\isamath{\mathcal{X}}}
7.44 -\newcommand{\isasymY}{\isamath{\mathcal{Y}}}
7.45 -\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
7.46 -\newcommand{\isasyma}{\isamath{\mathrm{a}}}
7.47 -\newcommand{\isasymb}{\isamath{\mathrm{b}}}
7.48 -\newcommand{\isasymc}{\isamath{\mathrm{c}}}
7.49 -\newcommand{\isasymd}{\isamath{\mathrm{d}}}
7.50 -\newcommand{\isasyme}{\isamath{\mathrm{e}}}
7.51 -\newcommand{\isasymf}{\isamath{\mathrm{f}}}
7.52 -\newcommand{\isasymg}{\isamath{\mathrm{g}}}
7.53 -\newcommand{\isasymh}{\isamath{\mathrm{h}}}
7.54 -\newcommand{\isasymi}{\isamath{\mathrm{i}}}
7.55 -\newcommand{\isasymj}{\isamath{\mathrm{j}}}
7.56 -\newcommand{\isasymk}{\isamath{\mathrm{k}}}
7.57 -\newcommand{\isasyml}{\isamath{\mathrm{l}}}
7.58 -\newcommand{\isasymm}{\isamath{\mathrm{m}}}
7.59 -\newcommand{\isasymn}{\isamath{\mathrm{n}}}
7.60 -\newcommand{\isasymo}{\isamath{\mathrm{o}}}
7.61 -\newcommand{\isasymp}{\isamath{\mathrm{p}}}
7.62 -\newcommand{\isasymq}{\isamath{\mathrm{q}}}
7.63 -\newcommand{\isasymr}{\isamath{\mathrm{r}}}
7.64 -\newcommand{\isasyms}{\isamath{\mathrm{s}}}
7.65 -\newcommand{\isasymt}{\isamath{\mathrm{t}}}
7.66 -\newcommand{\isasymu}{\isamath{\mathrm{u}}}
7.67 -\newcommand{\isasymv}{\isamath{\mathrm{v}}}
7.68 -\newcommand{\isasymw}{\isamath{\mathrm{w}}}
7.69 -\newcommand{\isasymx}{\isamath{\mathrm{x}}}
7.70 -\newcommand{\isasymy}{\isamath{\mathrm{y}}}
7.71 -\newcommand{\isasymz}{\isamath{\mathrm{z}}}
7.72 -\newcommand{\isasymAA}{\isamath{\mathfrak{A}}} %requires eufrak
7.73 -\newcommand{\isasymBB}{\isamath{\mathfrak{B}}} %requires eufrak
7.74 -\newcommand{\isasymCC}{\isamath{\mathfrak{C}}} %requires eufrak
7.75 -\newcommand{\isasymDD}{\isamath{\mathfrak{D}}} %requires eufrak
7.76 -\newcommand{\isasymEE}{\isamath{\mathfrak{E}}} %requires eufrak
7.77 -\newcommand{\isasymFF}{\isamath{\mathfrak{F}}} %requires eufrak
7.78 -\newcommand{\isasymGG}{\isamath{\mathfrak{G}}} %requires eufrak
7.79 -\newcommand{\isasymHH}{\isamath{\mathfrak{H}}} %requires eufrak
7.80 -\newcommand{\isasymII}{\isamath{\mathfrak{I}}} %requires eufrak
7.81 -\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}} %requires eufrak
7.82 -\newcommand{\isasymKK}{\isamath{\mathfrak{K}}} %requires eufrak
7.83 -\newcommand{\isasymLL}{\isamath{\mathfrak{L}}} %requires eufrak
7.84 -\newcommand{\isasymMM}{\isamath{\mathfrak{M}}} %requires eufrak
7.85 -\newcommand{\isasymNN}{\isamath{\mathfrak{N}}} %requires eufrak
7.86 -\newcommand{\isasymOO}{\isamath{\mathfrak{O}}} %requires eufrak
7.87 -\newcommand{\isasymPP}{\isamath{\mathfrak{P}}} %requires eufrak
7.88 -\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}} %requires eufrak
7.89 -\newcommand{\isasymRR}{\isamath{\mathfrak{R}}} %requires eufrak
7.90 -\newcommand{\isasymSS}{\isamath{\mathfrak{S}}} %requires eufrak
7.91 -\newcommand{\isasymTT}{\isamath{\mathfrak{T}}} %requires eufrak
7.92 -\newcommand{\isasymUU}{\isamath{\mathfrak{U}}} %requires eufrak
7.93 -\newcommand{\isasymVV}{\isamath{\mathfrak{V}}} %requires eufrak
7.94 -\newcommand{\isasymWW}{\isamath{\mathfrak{W}}} %requires eufrak
7.95 -\newcommand{\isasymXX}{\isamath{\mathfrak{X}}} %requires eufrak
7.96 -\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}} %requires eufrak
7.97 -\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}} %requires eufrak
7.98 -\newcommand{\isasymaa}{\isamath{\mathfrak{a}}} %requires eufrak
7.99 -\newcommand{\isasymbb}{\isamath{\mathfrak{b}}} %requires eufrak
7.100 -\newcommand{\isasymcc}{\isamath{\mathfrak{c}}} %requires eufrak
7.101 -\newcommand{\isasymdd}{\isamath{\mathfrak{d}}} %requires eufrak
7.102 -\newcommand{\isasymee}{\isamath{\mathfrak{e}}} %requires eufrak
7.103 -\newcommand{\isasymff}{\isamath{\mathfrak{f}}} %requires eufrak
7.104 -\newcommand{\isasymgg}{\isamath{\mathfrak{g}}} %requires eufrak
7.105 -\newcommand{\isasymhh}{\isamath{\mathfrak{h}}} %requires eufrak
7.106 -\newcommand{\isasymii}{\isamath{\mathfrak{i}}} %requires eufrak
7.107 -\newcommand{\isasymjj}{\isamath{\mathfrak{j}}} %requires eufrak
7.108 -\newcommand{\isasymkk}{\isamath{\mathfrak{k}}} %requires eufrak
7.109 -\newcommand{\isasymll}{\isamath{\mathfrak{l}}} %requires eufrak
7.110 -\newcommand{\isasymmm}{\isamath{\mathfrak{m}}} %requires eufrak
7.111 -\newcommand{\isasymnn}{\isamath{\mathfrak{n}}} %requires eufrak
7.112 -\newcommand{\isasymoo}{\isamath{\mathfrak{o}}} %requires eufrak
7.113 -\newcommand{\isasympp}{\isamath{\mathfrak{p}}} %requires eufrak
7.114 -\newcommand{\isasymqq}{\isamath{\mathfrak{q}}} %requires eufrak
7.115 -\newcommand{\isasymrr}{\isamath{\mathfrak{r}}} %requires eufrak
7.116 -\newcommand{\isasymss}{\isamath{\mathfrak{s}}} %requires eufrak
7.117 -\newcommand{\isasymtt}{\isamath{\mathfrak{t}}} %requires eufrak
7.118 -\newcommand{\isasymuu}{\isamath{\mathfrak{u}}} %requires eufrak
7.119 -\newcommand{\isasymvv}{\isamath{\mathfrak{v}}} %requires eufrak
7.120 -\newcommand{\isasymww}{\isamath{\mathfrak{w}}} %requires eufrak
7.121 -\newcommand{\isasymxx}{\isamath{\mathfrak{x}}} %requires eufrak
7.122 -\newcommand{\isasymyy}{\isamath{\mathfrak{y}}} %requires eufrak
7.123 -\newcommand{\isasymzz}{\isamath{\mathfrak{z}}} %requires eufrak
7.124 -\newcommand{\isasymalpha}{\isamath{\alpha}}
7.125 -\newcommand{\isasymbeta}{\isamath{\beta}}
7.126 -\newcommand{\isasymgamma}{\isamath{\gamma}}
7.127 -\newcommand{\isasymdelta}{\isamath{\delta}}
7.128 -\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
7.129 -\newcommand{\isasymzeta}{\isamath{\zeta}}
7.130 -\newcommand{\isasymeta}{\isamath{\eta}}
7.131 -\newcommand{\isasymtheta}{\isamath{\vartheta}}
7.132 -\newcommand{\isasymiota}{\isamath{\iota}}
7.133 -\newcommand{\isasymkappa}{\isamath{\kappa}}
7.134 -\newcommand{\isasymlambda}{\isamath{\lambda}}
7.135 -\newcommand{\isasymmu}{\isamath{\mu}}
7.136 -\newcommand{\isasymnu}{\isamath{\nu}}
7.137 -\newcommand{\isasymxi}{\isamath{\xi}}
7.138 -\newcommand{\isasympi}{\isamath{\pi}}
7.139 -\newcommand{\isasymrho}{\isamath{\varrho}}
7.140 -\newcommand{\isasymsigma}{\isamath{\sigma}}
7.141 -\newcommand{\isasymtau}{\isamath{\tau}}
7.142 -\newcommand{\isasymupsilon}{\isamath{\upsilon}}
7.143 -\newcommand{\isasymphi}{\isamath{\varphi}}
7.144 -\newcommand{\isasymchi}{\isamath{\chi}}
7.145 -\newcommand{\isasympsi}{\isamath{\psi}}
7.146 -\newcommand{\isasymomega}{\isamath{\omega}}
7.147 -\newcommand{\isasymGamma}{\isamath{\Gamma}}
7.148 -\newcommand{\isasymDelta}{\isamath{\Delta}}
7.149 -\newcommand{\isasymTheta}{\isamath{\Theta}}
7.150 -\newcommand{\isasymLambda}{\isamath{\Lambda}}
7.151 -\newcommand{\isasymXi}{\isamath{\Xi}}
7.152 -\newcommand{\isasymPi}{\isamath{\Pi}}
7.153 -\newcommand{\isasymSigma}{\isamath{\Sigma}}
7.154 -\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
7.155 -\newcommand{\isasymPhi}{\isamath{\Phi}}
7.156 -\newcommand{\isasymPsi}{\isamath{\Psi}}
7.157 -\newcommand{\isasymOmega}{\isamath{\Omega}}
7.158 -\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
7.159 -\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
7.160 -\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
7.161 -\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
7.162 -\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
7.163 -\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
7.164 -\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
7.165 -\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
7.166 -\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
7.167 -\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
7.168 -\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
7.169 -\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
7.170 -\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
7.171 -\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
7.172 -\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
7.173 -\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
7.174 -\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
7.175 -\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
7.176 -\newcommand{\isasymmapsto}{\isamath{\mapsto}}
7.177 -\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
7.178 -\newcommand{\isasymmidarrow}{\isamath{\relbar}}
7.179 -\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
7.180 -\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
7.181 -\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
7.182 -\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
7.183 -\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
7.184 -\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
7.185 -\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
7.186 -\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
7.187 -\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
7.188 -\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}} %requires amssymb
7.189 -\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}} %requires amssymb
7.190 -\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}} %requires amssymb
7.191 -\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}} %requires amssymb
7.192 -\newcommand{\isasymrestriction}{\isamath{\restriction}} %requires amssymb
7.193 -\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
7.194 -\newcommand{\isasymup}{\isamath{\uparrow}}
7.195 -\newcommand{\isasymUp}{\isamath{\Uparrow}}
7.196 -\newcommand{\isasymdown}{\isamath{\downarrow}}
7.197 -\newcommand{\isasymDown}{\isamath{\Downarrow}}
7.198 -\newcommand{\isasymupdown}{\isamath{\updownarrow}}
7.199 -\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
7.200 -\newcommand{\isasymlangle}{\isamath{\langle}}
7.201 -\newcommand{\isasymrangle}{\isamath{\rangle}}
7.202 -\newcommand{\isasymlceil}{\isamath{\lceil}}
7.203 -\newcommand{\isasymrceil}{\isamath{\rceil}}
7.204 -\newcommand{\isasymlfloor}{\isamath{\lfloor}}
7.205 -\newcommand{\isasymrfloor}{\isamath{\rfloor}}
7.206 -\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
7.207 -\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}
7.208 -\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
7.209 -\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
7.210 -\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
7.211 -\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
7.212 -\newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel
7.213 -\newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel
7.214 -\newcommand{\isasymbottom}{\isamath{\bot}}
7.215 -\newcommand{\isasymtop}{\isamath{\top}}
7.216 -\newcommand{\isasymand}{\isamath{\wedge}}
7.217 -\newcommand{\isasymAnd}{\isamath{\bigwedge}}
7.218 -\newcommand{\isasymor}{\isamath{\vee}}
7.219 -\newcommand{\isasymOr}{\isamath{\bigvee}}
7.220 -\newcommand{\isasymforall}{\isamath{\forall\,}}
7.221 -\newcommand{\isasymexists}{\isamath{\exists\,}}
7.222 -\newcommand{\isasymnexists}{\isamath{\nexists\,}} %requires amssymb
7.223 -\newcommand{\isasymnot}{\isamath{\neg}}
7.224 -\newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb
7.225 -\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb
7.226 -\newcommand{\isasymturnstile}{\isamath{\vdash}}
7.227 -\newcommand{\isasymTurnstile}{\isamath{\models}}
7.228 -\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
7.229 -\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
7.230 -\newcommand{\isasymstileturn}{\isamath{\dashv}}
7.231 -\newcommand{\isasymsurd}{\isamath{\surd}}
7.232 -\newcommand{\isasymle}{\isamath{\le}}
7.233 -\newcommand{\isasymge}{\isamath{\ge}}
7.234 -\newcommand{\isasymlless}{\isamath{\ll}}
7.235 -\newcommand{\isasymggreater}{\isamath{\gg}}
7.236 -\newcommand{\isasymlesssim}{\isamath{\lesssim}} %requires amssymb
7.237 -\newcommand{\isasymgreatersim}{\isamath{\gtrsim}} %requires amssymb
7.238 -\newcommand{\isasymlessapprox}{\isamath{\lessapprox}} %requires amssymb
7.239 -\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}} %requires amssymb
7.240 -\newcommand{\isasymin}{\isamath{\in}}
7.241 -\newcommand{\isasymnotin}{\isamath{\notin}}
7.242 -\newcommand{\isasymsubset}{\isamath{\subset}}
7.243 -\newcommand{\isasymsupset}{\isamath{\supset}}
7.244 -\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
7.245 -\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
7.246 -\newcommand{\isasymsqsubset}{\isamath{\sqsubset}} %requires amssymb
7.247 -\newcommand{\isasymsqsupset}{\isamath{\sqsupset}} %requires amssymb
7.248 -\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
7.249 -\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
7.250 -\newcommand{\isasyminter}{\isamath{\cap}}
7.251 -\newcommand{\isasymInter}{\isamath{\bigcap\,}}
7.252 -\newcommand{\isasymunion}{\isamath{\cup}}
7.253 -\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
7.254 -\newcommand{\isasymsqunion}{\isamath{\sqcup}}
7.255 -\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
7.256 -\newcommand{\isasymsqinter}{\isamath{\sqcap}}
7.257 -\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires amsmath
7.258 -\newcommand{\isasymsetminus}{\isamath{\setminus}}
7.259 -\newcommand{\isasympropto}{\isamath{\propto}}
7.260 -\newcommand{\isasymuplus}{\isamath{\uplus}}
7.261 -\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
7.262 -\newcommand{\isasymnoteq}{\isamath{\not=}}
7.263 -\newcommand{\isasymsim}{\isamath{\sim}}
7.264 -\newcommand{\isasymdoteq}{\isamath{\doteq}}
7.265 -\newcommand{\isasymsimeq}{\isamath{\simeq}}
7.266 -\newcommand{\isasymapprox}{\isamath{\approx}}
7.267 -\newcommand{\isasymasymp}{\isamath{\asymp}}
7.268 -\newcommand{\isasymcong}{\isamath{\cong}}
7.269 -\newcommand{\isasymsmile}{\isamath{\smile}}
7.270 -\newcommand{\isasymequiv}{\isamath{\equiv}}
7.271 -\newcommand{\isasymfrown}{\isamath{\frown}}
7.272 -\newcommand{\isasymJoin}{\isamath{\Join}} %requires amssymb
7.273 -\newcommand{\isasymbowtie}{\isamath{\bowtie}}
7.274 -\newcommand{\isasymprec}{\isamath{\prec}}
7.275 -\newcommand{\isasymsucc}{\isamath{\succ}}
7.276 -\newcommand{\isasympreceq}{\isamath{\preceq}}
7.277 -\newcommand{\isasymsucceq}{\isamath{\succeq}}
7.278 -\newcommand{\isasymparallel}{\isamath{\parallel}}
7.279 -\newcommand{\isasymbar}{\isamath{\mid}}
7.280 -\newcommand{\isasymplusminus}{\isamath{\pm}}
7.281 -\newcommand{\isasymminusplus}{\isamath{\mp}}
7.282 -\newcommand{\isasymtimes}{\isamath{\times}}
7.283 -\newcommand{\isasymdiv}{\isamath{\div}}
7.284 -\newcommand{\isasymcdot}{\isamath{\cdot}}
7.285 -\newcommand{\isasymstar}{\isamath{\star}}
7.286 -\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
7.287 -\newcommand{\isasymcirc}{\isamath{\circ}}
7.288 -\newcommand{\isasymdagger}{\isamath{\dagger}}
7.289 -\newcommand{\isasymddagger}{\isamath{\ddagger}}
7.290 -\newcommand{\isasymlhd}{\isamath{\lhd}} %requires amssymb
7.291 -\newcommand{\isasymrhd}{\isamath{\rhd}} %requires amssymb
7.292 -\newcommand{\isasymunlhd}{\isamath{\unlhd}} %requires amssymb
7.293 -\newcommand{\isasymunrhd}{\isamath{\unrhd}} %requires amssymb
7.294 -\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
7.295 -\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
7.296 -\newcommand{\isasymtriangle}{\isamath{\triangle}}
7.297 -\newcommand{\isasymtriangleq}{\isamath{\triangleq}} %requires amssymb
7.298 -\newcommand{\isasymoplus}{\isamath{\oplus}}
7.299 -\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}
7.300 -\newcommand{\isasymotimes}{\isamath{\otimes}}
7.301 -\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}
7.302 -\newcommand{\isasymodot}{\isamath{\odot}}
7.303 -\newcommand{\isasymOdot}{\isamath{\bigodot\,}}
7.304 -\newcommand{\isasymominus}{\isamath{\ominus}}
7.305 -\newcommand{\isasymoslash}{\isamath{\oslash}}
7.306 -\newcommand{\isasymdots}{\isamath{\dots}}
7.307 -\newcommand{\isasymcdots}{\isamath{\cdots}}
7.308 -\newcommand{\isasymSum}{\isamath{\sum\,}}
7.309 -\newcommand{\isasymProd}{\isamath{\prod\,}}
7.310 -\newcommand{\isasymCoprod}{\isamath{\coprod\,}}
7.311 -\newcommand{\isasyminfinity}{\isamath{\infty}}
7.312 -\newcommand{\isasymintegral}{\isamath{\int\,}}
7.313 -\newcommand{\isasymointegral}{\isamath{\oint\,}}
7.314 -\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
7.315 -\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
7.316 -\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
7.317 -\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
7.318 -\newcommand{\isasymaleph}{\isamath{\aleph}}
7.319 -\newcommand{\isasymemptyset}{\isamath{\emptyset}}
7.320 -\newcommand{\isasymnabla}{\isamath{\nabla}}
7.321 -\newcommand{\isasympartial}{\isamath{\partial}}
7.322 -\newcommand{\isasymRe}{\isamath{\Re}}
7.323 -\newcommand{\isasymIm}{\isamath{\Im}}
7.324 -\newcommand{\isasymflat}{\isamath{\flat}}
7.325 -\newcommand{\isasymnatural}{\isamath{\natural}}
7.326 -\newcommand{\isasymsharp}{\isamath{\sharp}}
7.327 -\newcommand{\isasymangle}{\isamath{\angle}}
7.328 -\newcommand{\isasymcopyright}{\isatext{\rm\copyright}}
7.329 -\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
7.330 -\newcommand{\isasymhyphen}{\isatext{\rm-}}
7.331 -\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
7.332 -\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}} %requires latin1
7.333 -\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}} %requires latin1
7.334 -\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}} %requires latin1
7.335 -\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}} %requires latin1
7.336 -\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}} %requires latin1
7.337 -\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}} %requires latin1
7.338 -\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
7.339 -\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
7.340 -\newcommand{\isasymsection}{\isatext{\rm\S}}
7.341 -\newcommand{\isasymparagraph}{\isatext{\rm\P}}
7.342 -\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
7.343 -\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
7.344 -\newcommand{\isasymeuro}{\isatext{\textgreek{\euro}}} %requires greek babel
7.345 -\newcommand{\isasympounds}{\isamath{\pounds}}
7.346 -\newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb
7.347 -\newcommand{\isasymcent}{\isatext{\textcent}} %requires textcomp
7.348 -\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
7.349 -\newcommand{\isasymdegree}{\isatext{\rm\textdegree}} %requires latin1
7.350 -\newcommand{\isasymamalg}{\isamath{\amalg}}
7.351 -\newcommand{\isasymmho}{\isamath{\mho}} %requires amssymb
7.352 -\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssymb
7.353 -\newcommand{\isasymwp}{\isamath{\wp}}
7.354 -\newcommand{\isasymwrong}{\isamath{\wr}}
7.355 -\newcommand{\isasymstruct}{\isamath{\diamond}}
7.356 -\newcommand{\isasymacute}{\isatext{\'\relax}}
7.357 -\newcommand{\isasymindex}{\isatext{\i}}
7.358 -\newcommand{\isasymdieresis}{\isatext{\"\relax}}
7.359 -\newcommand{\isasymcedilla}{\isatext{\c\relax}}
7.360 -\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
7.361 -\newcommand{\isasymspacespace}{\isamath{~~}}
7.362 -\newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}
7.363 -\newcommand{\isasymsome}{\isamath{\epsilon\,}}
8.1 --- a/doc-src/LaTeXsugar/Sugar/document/isabelle.sty Thu May 15 20:02:44 2008 +0200
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,215 +0,0 @@
8.4 -%%
8.5 -%%
8.6 -%%
8.7 -%% macros for Isabelle generated LaTeX output
8.8 -%%
8.9 -
8.10 -%%% Simple document preparation (based on theory token language and symbols)
8.11 -
8.12 -% isabelle environments
8.13 -
8.14 -\newcommand{\isabellecontext}{UNKNOWN}
8.15 -
8.16 -\newcommand{\isastyle}{\UNDEF}
8.17 -\newcommand{\isastyleminor}{\UNDEF}
8.18 -\newcommand{\isastylescript}{\UNDEF}
8.19 -\newcommand{\isastyletext}{\normalsize\rm}
8.20 -\newcommand{\isastyletxt}{\rm}
8.21 -\newcommand{\isastylecmt}{\rm}
8.22 -
8.23 -%symbol markup -- \emph achieves decent spacing via italic corrections
8.24 -\newcommand{\isamath}[1]{\emph{$#1$}}
8.25 -\newcommand{\isatext}[1]{\emph{#1}}
8.26 -\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
8.27 -\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
8.28 -\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
8.29 -\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
8.30 -\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
8.31 -\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isastylescript}
8.32 -\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
8.33 -\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isastylescript}
8.34 -\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
8.35 -\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
8.36 -\newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
8.37 -\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
8.38 -
8.39 -
8.40 -\newdimen\isa@parindent\newdimen\isa@parskip
8.41 -
8.42 -\newenvironment{isabellebody}{%
8.43 -\isamarkuptrue\par%
8.44 -\isa@parindent\parindent\parindent0pt%
8.45 -\isa@parskip\parskip\parskip0pt%
8.46 -\isastyle}{\par}
8.47 -
8.48 -\newenvironment{isabelle}
8.49 -{\begin{trivlist}\begin{isabellebody}\item\relax}
8.50 -{\end{isabellebody}\end{trivlist}}
8.51 -
8.52 -\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
8.53 -
8.54 -\newcommand{\isaindent}[1]{\hphantom{#1}}
8.55 -\newcommand{\isanewline}{\mbox{}\par\mbox{}}
8.56 -\newcommand{\isasep}{}
8.57 -\newcommand{\isadigit}[1]{#1}
8.58 -
8.59 -\newcommand{\isachardefaults}{%
8.60 -\chardef\isacharbang=`\!%
8.61 -\chardef\isachardoublequote=`\"%
8.62 -\chardef\isachardoublequoteopen=`\"%
8.63 -\chardef\isachardoublequoteclose=`\"%
8.64 -\chardef\isacharhash=`\#%
8.65 -\chardef\isachardollar=`\$%
8.66 -\chardef\isacharpercent=`\%%
8.67 -\chardef\isacharampersand=`\&%
8.68 -\chardef\isacharprime=`\'%
8.69 -\chardef\isacharparenleft=`\(%
8.70 -\chardef\isacharparenright=`\)%
8.71 -\chardef\isacharasterisk=`\*%
8.72 -\chardef\isacharplus=`\+%
8.73 -\chardef\isacharcomma=`\,%
8.74 -\chardef\isacharminus=`\-%
8.75 -\chardef\isachardot=`\.%
8.76 -\chardef\isacharslash=`\/%
8.77 -\chardef\isacharcolon=`\:%
8.78 -\chardef\isacharsemicolon=`\;%
8.79 -\chardef\isacharless=`\<%
8.80 -\chardef\isacharequal=`\=%
8.81 -\chardef\isachargreater=`\>%
8.82 -\chardef\isacharquery=`\?%
8.83 -\chardef\isacharat=`\@%
8.84 -\chardef\isacharbrackleft=`\[%
8.85 -\chardef\isacharbackslash=`\\%
8.86 -\chardef\isacharbrackright=`\]%
8.87 -\chardef\isacharcircum=`\^%
8.88 -\chardef\isacharunderscore=`\_%
8.89 -\def\isacharunderscorekeyword{\_}%
8.90 -\chardef\isacharbackquote=`\`%
8.91 -\chardef\isacharbackquoteopen=`\`%
8.92 -\chardef\isacharbackquoteclose=`\`%
8.93 -\chardef\isacharbraceleft=`\{%
8.94 -\chardef\isacharbar=`\|%
8.95 -\chardef\isacharbraceright=`\}%
8.96 -\chardef\isachartilde=`\~%
8.97 -\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
8.98 -\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
8.99 -}
8.100 -
8.101 -
8.102 -% keyword and section markup
8.103 -
8.104 -\newcommand{\isakeyword}[1]
8.105 -{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
8.106 -\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
8.107 -\newcommand{\isacommand}[1]{\isakeyword{#1}}
8.108 -
8.109 -\newcommand{\isamarkupheader}[1]{\section{#1}}
8.110 -\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
8.111 -\newcommand{\isamarkupsection}[1]{\section{#1}}
8.112 -\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
8.113 -\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
8.114 -\newcommand{\isamarkupsect}[1]{\section{#1}}
8.115 -\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
8.116 -\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
8.117 -
8.118 -\newif\ifisamarkup
8.119 -\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
8.120 -\newcommand{\isaendpar}{\par\medskip}
8.121 -\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
8.122 -\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
8.123 -\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
8.124 -\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
8.125 -
8.126 -
8.127 -% styles
8.128 -
8.129 -\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
8.130 -
8.131 -\newcommand{\isabellestyledefault}{%
8.132 -\renewcommand{\isastyle}{\small\tt\slshape}%
8.133 -\renewcommand{\isastyleminor}{\small\tt\slshape}%
8.134 -\renewcommand{\isastylescript}{\footnotesize\tt\slshape}%
8.135 -\isachardefaults%
8.136 -}
8.137 -\isabellestyledefault
8.138 -
8.139 -\newcommand{\isabellestylett}{%
8.140 -\renewcommand{\isastyle}{\small\tt}%
8.141 -\renewcommand{\isastyleminor}{\small\tt}%
8.142 -\renewcommand{\isastylescript}{\footnotesize\tt}%
8.143 -\isachardefaults%
8.144 -}
8.145 -
8.146 -\newcommand{\isabellestyleit}{%
8.147 -\renewcommand{\isastyle}{\small\it}%
8.148 -\renewcommand{\isastyleminor}{\it}%
8.149 -\renewcommand{\isastylescript}{\footnotesize\it}%
8.150 -\renewcommand{\isacharunderscorekeyword}{\mbox{-}}%
8.151 -\renewcommand{\isacharbang}{\isamath{!}}%
8.152 -\renewcommand{\isachardoublequote}{}%
8.153 -\renewcommand{\isachardoublequoteopen}{}%
8.154 -\renewcommand{\isachardoublequoteclose}{}%
8.155 -\renewcommand{\isacharhash}{\isamath{\#}}%
8.156 -\renewcommand{\isachardollar}{\isamath{\$}}%
8.157 -\renewcommand{\isacharpercent}{\isamath{\%}}%
8.158 -\renewcommand{\isacharampersand}{\isamath{\&}}%
8.159 -\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
8.160 -\renewcommand{\isacharparenleft}{\isamath{(}}%
8.161 -\renewcommand{\isacharparenright}{\isamath{)}}%
8.162 -\renewcommand{\isacharasterisk}{\isamath{*}}%
8.163 -\renewcommand{\isacharplus}{\isamath{+}}%
8.164 -\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
8.165 -\renewcommand{\isacharminus}{\isamath{-}}%
8.166 -\renewcommand{\isachardot}{\isamath{\mathord.}}%
8.167 -\renewcommand{\isacharslash}{\isamath{/}}%
8.168 -\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
8.169 -\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
8.170 -\renewcommand{\isacharless}{\isamath{<}}%
8.171 -\renewcommand{\isacharequal}{\isamath{=}}%
8.172 -\renewcommand{\isachargreater}{\isamath{>}}%
8.173 -\renewcommand{\isacharat}{\isamath{@}}%
8.174 -\renewcommand{\isacharbrackleft}{\isamath{[}}%
8.175 -\renewcommand{\isacharbackslash}{\isamath{\backslash}}%
8.176 -\renewcommand{\isacharbrackright}{\isamath{]}}%
8.177 -\renewcommand{\isacharunderscore}{\mbox{-}}%
8.178 -\renewcommand{\isacharbraceleft}{\isamath{\{}}%
8.179 -\renewcommand{\isacharbar}{\isamath{\mid}}%
8.180 -\renewcommand{\isacharbraceright}{\isamath{\}}}%
8.181 -\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
8.182 -\renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
8.183 -\renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
8.184 -\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}%
8.185 -\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}%
8.186 -}
8.187 -
8.188 -\newcommand{\isabellestylesl}{%
8.189 -\isabellestyleit%
8.190 -\renewcommand{\isastyle}{\small\sl}%
8.191 -\renewcommand{\isastyleminor}{\sl}%
8.192 -\renewcommand{\isastylescript}{\footnotesize\sl}%
8.193 -}
8.194 -
8.195 -
8.196 -% tagged regions
8.197 -
8.198 -%plain TeX version of comment package -- much faster!
8.199 -\let\isafmtname\fmtname\def\fmtname{plain}
8.200 -\usepackage{comment}
8.201 -\let\fmtname\isafmtname
8.202 -
8.203 -\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
8.204 -
8.205 -\newcommand{\isakeeptag}[1]%
8.206 -{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
8.207 -\newcommand{\isadroptag}[1]%
8.208 -{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
8.209 -\newcommand{\isafoldtag}[1]%
8.210 -{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
8.211 -
8.212 -\isakeeptag{theory}
8.213 -\isakeeptag{proof}
8.214 -\isakeeptag{ML}
8.215 -\isakeeptag{visible}
8.216 -\isadroptag{invisible}
8.217 -
8.218 -\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}
9.1 --- a/doc-src/LaTeXsugar/Sugar/document/isabellesym.sty Thu May 15 20:02:44 2008 +0200
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,360 +0,0 @@
9.4 -%%
9.5 -%%
9.6 -%%
9.7 -%% definitions of standard Isabelle symbols
9.8 -%%
9.9 -
9.10 -\newcommand{\isasymzero}{\isamath{\mathbf{0}}} %requires amssymb
9.11 -\newcommand{\isasymone}{\isamath{\mathbf{1}}} %requires amssymb
9.12 -\newcommand{\isasymtwo}{\isamath{\mathbf{2}}} %requires amssymb
9.13 -\newcommand{\isasymthree}{\isamath{\mathbf{3}}} %requires amssymb
9.14 -\newcommand{\isasymfour}{\isamath{\mathbf{4}}} %requires amssymb
9.15 -\newcommand{\isasymfive}{\isamath{\mathbf{5}}} %requires amssymb
9.16 -\newcommand{\isasymsix}{\isamath{\mathbf{6}}} %requires amssymb
9.17 -\newcommand{\isasymseven}{\isamath{\mathbf{7}}} %requires amssymb
9.18 -\newcommand{\isasymeight}{\isamath{\mathbf{8}}} %requires amssymb
9.19 -\newcommand{\isasymnine}{\isamath{\mathbf{9}}} %requires amssymb
9.20 -\newcommand{\isasymA}{\isamath{\mathcal{A}}}
9.21 -\newcommand{\isasymB}{\isamath{\mathcal{B}}}
9.22 -\newcommand{\isasymC}{\isamath{\mathcal{C}}}
9.23 -\newcommand{\isasymD}{\isamath{\mathcal{D}}}
9.24 -\newcommand{\isasymE}{\isamath{\mathcal{E}}}
9.25 -\newcommand{\isasymF}{\isamath{\mathcal{F}}}
9.26 -\newcommand{\isasymG}{\isamath{\mathcal{G}}}
9.27 -\newcommand{\isasymH}{\isamath{\mathcal{H}}}
9.28 -\newcommand{\isasymI}{\isamath{\mathcal{I}}}
9.29 -\newcommand{\isasymJ}{\isamath{\mathcal{J}}}
9.30 -\newcommand{\isasymK}{\isamath{\mathcal{K}}}
9.31 -\newcommand{\isasymL}{\isamath{\mathcal{L}}}
9.32 -\newcommand{\isasymM}{\isamath{\mathcal{M}}}
9.33 -\newcommand{\isasymN}{\isamath{\mathcal{N}}}
9.34 -\newcommand{\isasymO}{\isamath{\mathcal{O}}}
9.35 -\newcommand{\isasymP}{\isamath{\mathcal{P}}}
9.36 -\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}
9.37 -\newcommand{\isasymR}{\isamath{\mathcal{R}}}
9.38 -\newcommand{\isasymS}{\isamath{\mathcal{S}}}
9.39 -\newcommand{\isasymT}{\isamath{\mathcal{T}}}
9.40 -\newcommand{\isasymU}{\isamath{\mathcal{U}}}
9.41 -\newcommand{\isasymV}{\isamath{\mathcal{V}}}
9.42 -\newcommand{\isasymW}{\isamath{\mathcal{W}}}
9.43 -\newcommand{\isasymX}{\isamath{\mathcal{X}}}
9.44 -\newcommand{\isasymY}{\isamath{\mathcal{Y}}}
9.45 -\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
9.46 -\newcommand{\isasyma}{\isamath{\mathrm{a}}}
9.47 -\newcommand{\isasymb}{\isamath{\mathrm{b}}}
9.48 -\newcommand{\isasymc}{\isamath{\mathrm{c}}}
9.49 -\newcommand{\isasymd}{\isamath{\mathrm{d}}}
9.50 -\newcommand{\isasyme}{\isamath{\mathrm{e}}}
9.51 -\newcommand{\isasymf}{\isamath{\mathrm{f}}}
9.52 -\newcommand{\isasymg}{\isamath{\mathrm{g}}}
9.53 -\newcommand{\isasymh}{\isamath{\mathrm{h}}}
9.54 -\newcommand{\isasymi}{\isamath{\mathrm{i}}}
9.55 -\newcommand{\isasymj}{\isamath{\mathrm{j}}}
9.56 -\newcommand{\isasymk}{\isamath{\mathrm{k}}}
9.57 -\newcommand{\isasyml}{\isamath{\mathrm{l}}}
9.58 -\newcommand{\isasymm}{\isamath{\mathrm{m}}}
9.59 -\newcommand{\isasymn}{\isamath{\mathrm{n}}}
9.60 -\newcommand{\isasymo}{\isamath{\mathrm{o}}}
9.61 -\newcommand{\isasymp}{\isamath{\mathrm{p}}}
9.62 -\newcommand{\isasymq}{\isamath{\mathrm{q}}}
9.63 -\newcommand{\isasymr}{\isamath{\mathrm{r}}}
9.64 -\newcommand{\isasyms}{\isamath{\mathrm{s}}}
9.65 -\newcommand{\isasymt}{\isamath{\mathrm{t}}}
9.66 -\newcommand{\isasymu}{\isamath{\mathrm{u}}}
9.67 -\newcommand{\isasymv}{\isamath{\mathrm{v}}}
9.68 -\newcommand{\isasymw}{\isamath{\mathrm{w}}}
9.69 -\newcommand{\isasymx}{\isamath{\mathrm{x}}}
9.70 -\newcommand{\isasymy}{\isamath{\mathrm{y}}}
9.71 -\newcommand{\isasymz}{\isamath{\mathrm{z}}}
9.72 -\newcommand{\isasymAA}{\isamath{\mathfrak{A}}} %requires eufrak
9.73 -\newcommand{\isasymBB}{\isamath{\mathfrak{B}}} %requires eufrak
9.74 -\newcommand{\isasymCC}{\isamath{\mathfrak{C}}} %requires eufrak
9.75 -\newcommand{\isasymDD}{\isamath{\mathfrak{D}}} %requires eufrak
9.76 -\newcommand{\isasymEE}{\isamath{\mathfrak{E}}} %requires eufrak
9.77 -\newcommand{\isasymFF}{\isamath{\mathfrak{F}}} %requires eufrak
9.78 -\newcommand{\isasymGG}{\isamath{\mathfrak{G}}} %requires eufrak
9.79 -\newcommand{\isasymHH}{\isamath{\mathfrak{H}}} %requires eufrak
9.80 -\newcommand{\isasymII}{\isamath{\mathfrak{I}}} %requires eufrak
9.81 -\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}} %requires eufrak
9.82 -\newcommand{\isasymKK}{\isamath{\mathfrak{K}}} %requires eufrak
9.83 -\newcommand{\isasymLL}{\isamath{\mathfrak{L}}} %requires eufrak
9.84 -\newcommand{\isasymMM}{\isamath{\mathfrak{M}}} %requires eufrak
9.85 -\newcommand{\isasymNN}{\isamath{\mathfrak{N}}} %requires eufrak
9.86 -\newcommand{\isasymOO}{\isamath{\mathfrak{O}}} %requires eufrak
9.87 -\newcommand{\isasymPP}{\isamath{\mathfrak{P}}} %requires eufrak
9.88 -\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}} %requires eufrak
9.89 -\newcommand{\isasymRR}{\isamath{\mathfrak{R}}} %requires eufrak
9.90 -\newcommand{\isasymSS}{\isamath{\mathfrak{S}}} %requires eufrak
9.91 -\newcommand{\isasymTT}{\isamath{\mathfrak{T}}} %requires eufrak
9.92 -\newcommand{\isasymUU}{\isamath{\mathfrak{U}}} %requires eufrak
9.93 -\newcommand{\isasymVV}{\isamath{\mathfrak{V}}} %requires eufrak
9.94 -\newcommand{\isasymWW}{\isamath{\mathfrak{W}}} %requires eufrak
9.95 -\newcommand{\isasymXX}{\isamath{\mathfrak{X}}} %requires eufrak
9.96 -\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}} %requires eufrak
9.97 -\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}} %requires eufrak
9.98 -\newcommand{\isasymaa}{\isamath{\mathfrak{a}}} %requires eufrak
9.99 -\newcommand{\isasymbb}{\isamath{\mathfrak{b}}} %requires eufrak
9.100 -\newcommand{\isasymcc}{\isamath{\mathfrak{c}}} %requires eufrak
9.101 -\newcommand{\isasymdd}{\isamath{\mathfrak{d}}} %requires eufrak
9.102 -\newcommand{\isasymee}{\isamath{\mathfrak{e}}} %requires eufrak
9.103 -\newcommand{\isasymff}{\isamath{\mathfrak{f}}} %requires eufrak
9.104 -\newcommand{\isasymgg}{\isamath{\mathfrak{g}}} %requires eufrak
9.105 -\newcommand{\isasymhh}{\isamath{\mathfrak{h}}} %requires eufrak
9.106 -\newcommand{\isasymii}{\isamath{\mathfrak{i}}} %requires eufrak
9.107 -\newcommand{\isasymjj}{\isamath{\mathfrak{j}}} %requires eufrak
9.108 -\newcommand{\isasymkk}{\isamath{\mathfrak{k}}} %requires eufrak
9.109 -\newcommand{\isasymll}{\isamath{\mathfrak{l}}} %requires eufrak
9.110 -\newcommand{\isasymmm}{\isamath{\mathfrak{m}}} %requires eufrak
9.111 -\newcommand{\isasymnn}{\isamath{\mathfrak{n}}} %requires eufrak
9.112 -\newcommand{\isasymoo}{\isamath{\mathfrak{o}}} %requires eufrak
9.113 -\newcommand{\isasympp}{\isamath{\mathfrak{p}}} %requires eufrak
9.114 -\newcommand{\isasymqq}{\isamath{\mathfrak{q}}} %requires eufrak
9.115 -\newcommand{\isasymrr}{\isamath{\mathfrak{r}}} %requires eufrak
9.116 -\newcommand{\isasymss}{\isamath{\mathfrak{s}}} %requires eufrak
9.117 -\newcommand{\isasymtt}{\isamath{\mathfrak{t}}} %requires eufrak
9.118 -\newcommand{\isasymuu}{\isamath{\mathfrak{u}}} %requires eufrak
9.119 -\newcommand{\isasymvv}{\isamath{\mathfrak{v}}} %requires eufrak
9.120 -\newcommand{\isasymww}{\isamath{\mathfrak{w}}} %requires eufrak
9.121 -\newcommand{\isasymxx}{\isamath{\mathfrak{x}}} %requires eufrak
9.122 -\newcommand{\isasymyy}{\isamath{\mathfrak{y}}} %requires eufrak
9.123 -\newcommand{\isasymzz}{\isamath{\mathfrak{z}}} %requires eufrak
9.124 -\newcommand{\isasymalpha}{\isamath{\alpha}}
9.125 -\newcommand{\isasymbeta}{\isamath{\beta}}
9.126 -\newcommand{\isasymgamma}{\isamath{\gamma}}
9.127 -\newcommand{\isasymdelta}{\isamath{\delta}}
9.128 -\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
9.129 -\newcommand{\isasymzeta}{\isamath{\zeta}}
9.130 -\newcommand{\isasymeta}{\isamath{\eta}}
9.131 -\newcommand{\isasymtheta}{\isamath{\vartheta}}
9.132 -\newcommand{\isasymiota}{\isamath{\iota}}
9.133 -\newcommand{\isasymkappa}{\isamath{\kappa}}
9.134 -\newcommand{\isasymlambda}{\isamath{\lambda}}
9.135 -\newcommand{\isasymmu}{\isamath{\mu}}
9.136 -\newcommand{\isasymnu}{\isamath{\nu}}
9.137 -\newcommand{\isasymxi}{\isamath{\xi}}
9.138 -\newcommand{\isasympi}{\isamath{\pi}}
9.139 -\newcommand{\isasymrho}{\isamath{\varrho}}
9.140 -\newcommand{\isasymsigma}{\isamath{\sigma}}
9.141 -\newcommand{\isasymtau}{\isamath{\tau}}
9.142 -\newcommand{\isasymupsilon}{\isamath{\upsilon}}
9.143 -\newcommand{\isasymphi}{\isamath{\varphi}}
9.144 -\newcommand{\isasymchi}{\isamath{\chi}}
9.145 -\newcommand{\isasympsi}{\isamath{\psi}}
9.146 -\newcommand{\isasymomega}{\isamath{\omega}}
9.147 -\newcommand{\isasymGamma}{\isamath{\Gamma}}
9.148 -\newcommand{\isasymDelta}{\isamath{\Delta}}
9.149 -\newcommand{\isasymTheta}{\isamath{\Theta}}
9.150 -\newcommand{\isasymLambda}{\isamath{\Lambda}}
9.151 -\newcommand{\isasymXi}{\isamath{\Xi}}
9.152 -\newcommand{\isasymPi}{\isamath{\Pi}}
9.153 -\newcommand{\isasymSigma}{\isamath{\Sigma}}
9.154 -\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
9.155 -\newcommand{\isasymPhi}{\isamath{\Phi}}
9.156 -\newcommand{\isasymPsi}{\isamath{\Psi}}
9.157 -\newcommand{\isasymOmega}{\isamath{\Omega}}
9.158 -\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
9.159 -\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
9.160 -\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
9.161 -\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
9.162 -\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
9.163 -\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
9.164 -\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
9.165 -\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
9.166 -\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
9.167 -\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
9.168 -\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
9.169 -\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
9.170 -\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
9.171 -\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
9.172 -\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
9.173 -\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
9.174 -\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
9.175 -\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
9.176 -\newcommand{\isasymmapsto}{\isamath{\mapsto}}
9.177 -\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
9.178 -\newcommand{\isasymmidarrow}{\isamath{\relbar}}
9.179 -\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
9.180 -\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
9.181 -\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
9.182 -\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
9.183 -\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
9.184 -\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
9.185 -\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
9.186 -\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
9.187 -\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
9.188 -\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}} %requires amssymb
9.189 -\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}} %requires amssymb
9.190 -\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}} %requires amssymb
9.191 -\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}} %requires amssymb
9.192 -\newcommand{\isasymrestriction}{\isamath{\restriction}} %requires amssymb
9.193 -\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
9.194 -\newcommand{\isasymup}{\isamath{\uparrow}}
9.195 -\newcommand{\isasymUp}{\isamath{\Uparrow}}
9.196 -\newcommand{\isasymdown}{\isamath{\downarrow}}
9.197 -\newcommand{\isasymDown}{\isamath{\Downarrow}}
9.198 -\newcommand{\isasymupdown}{\isamath{\updownarrow}}
9.199 -\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
9.200 -\newcommand{\isasymlangle}{\isamath{\langle}}
9.201 -\newcommand{\isasymrangle}{\isamath{\rangle}}
9.202 -\newcommand{\isasymlceil}{\isamath{\lceil}}
9.203 -\newcommand{\isasymrceil}{\isamath{\rceil}}
9.204 -\newcommand{\isasymlfloor}{\isamath{\lfloor}}
9.205 -\newcommand{\isasymrfloor}{\isamath{\rfloor}}
9.206 -\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
9.207 -\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}
9.208 -\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
9.209 -\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
9.210 -\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
9.211 -\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
9.212 -\newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel
9.213 -\newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel
9.214 -\newcommand{\isasymbottom}{\isamath{\bot}}
9.215 -\newcommand{\isasymtop}{\isamath{\top}}
9.216 -\newcommand{\isasymand}{\isamath{\wedge}}
9.217 -\newcommand{\isasymAnd}{\isamath{\bigwedge}}
9.218 -\newcommand{\isasymor}{\isamath{\vee}}
9.219 -\newcommand{\isasymOr}{\isamath{\bigvee}}
9.220 -\newcommand{\isasymforall}{\isamath{\forall\,}}
9.221 -\newcommand{\isasymexists}{\isamath{\exists\,}}
9.222 -\newcommand{\isasymnexists}{\isamath{\nexists\,}} %requires amssymb
9.223 -\newcommand{\isasymnot}{\isamath{\neg}}
9.224 -\newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb
9.225 -\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb
9.226 -\newcommand{\isasymturnstile}{\isamath{\vdash}}
9.227 -\newcommand{\isasymTurnstile}{\isamath{\models}}
9.228 -\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
9.229 -\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
9.230 -\newcommand{\isasymstileturn}{\isamath{\dashv}}
9.231 -\newcommand{\isasymsurd}{\isamath{\surd}}
9.232 -\newcommand{\isasymle}{\isamath{\le}}
9.233 -\newcommand{\isasymge}{\isamath{\ge}}
9.234 -\newcommand{\isasymlless}{\isamath{\ll}}
9.235 -\newcommand{\isasymggreater}{\isamath{\gg}}
9.236 -\newcommand{\isasymlesssim}{\isamath{\lesssim}} %requires amssymb
9.237 -\newcommand{\isasymgreatersim}{\isamath{\gtrsim}} %requires amssymb
9.238 -\newcommand{\isasymlessapprox}{\isamath{\lessapprox}} %requires amssymb
9.239 -\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}} %requires amssymb
9.240 -\newcommand{\isasymin}{\isamath{\in}}
9.241 -\newcommand{\isasymnotin}{\isamath{\notin}}
9.242 -\newcommand{\isasymsubset}{\isamath{\subset}}
9.243 -\newcommand{\isasymsupset}{\isamath{\supset}}
9.244 -\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
9.245 -\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
9.246 -\newcommand{\isasymsqsubset}{\isamath{\sqsubset}} %requires amssymb
9.247 -\newcommand{\isasymsqsupset}{\isamath{\sqsupset}} %requires amssymb
9.248 -\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
9.249 -\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
9.250 -\newcommand{\isasyminter}{\isamath{\cap}}
9.251 -\newcommand{\isasymInter}{\isamath{\bigcap\,}}
9.252 -\newcommand{\isasymunion}{\isamath{\cup}}
9.253 -\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
9.254 -\newcommand{\isasymsqunion}{\isamath{\sqcup}}
9.255 -\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
9.256 -\newcommand{\isasymsqinter}{\isamath{\sqcap}}
9.257 -\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires amsmath
9.258 -\newcommand{\isasymsetminus}{\isamath{\setminus}}
9.259 -\newcommand{\isasympropto}{\isamath{\propto}}
9.260 -\newcommand{\isasymuplus}{\isamath{\uplus}}
9.261 -\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
9.262 -\newcommand{\isasymnoteq}{\isamath{\not=}}
9.263 -\newcommand{\isasymsim}{\isamath{\sim}}
9.264 -\newcommand{\isasymdoteq}{\isamath{\doteq}}
9.265 -\newcommand{\isasymsimeq}{\isamath{\simeq}}
9.266 -\newcommand{\isasymapprox}{\isamath{\approx}}
9.267 -\newcommand{\isasymasymp}{\isamath{\asymp}}
9.268 -\newcommand{\isasymcong}{\isamath{\cong}}
9.269 -\newcommand{\isasymsmile}{\isamath{\smile}}
9.270 -\newcommand{\isasymequiv}{\isamath{\equiv}}
9.271 -\newcommand{\isasymfrown}{\isamath{\frown}}
9.272 -\newcommand{\isasymJoin}{\isamath{\Join}} %requires amssymb
9.273 -\newcommand{\isasymbowtie}{\isamath{\bowtie}}
9.274 -\newcommand{\isasymprec}{\isamath{\prec}}
9.275 -\newcommand{\isasymsucc}{\isamath{\succ}}
9.276 -\newcommand{\isasympreceq}{\isamath{\preceq}}
9.277 -\newcommand{\isasymsucceq}{\isamath{\succeq}}
9.278 -\newcommand{\isasymparallel}{\isamath{\parallel}}
9.279 -\newcommand{\isasymbar}{\isamath{\mid}}
9.280 -\newcommand{\isasymplusminus}{\isamath{\pm}}
9.281 -\newcommand{\isasymminusplus}{\isamath{\mp}}
9.282 -\newcommand{\isasymtimes}{\isamath{\times}}
9.283 -\newcommand{\isasymdiv}{\isamath{\div}}
9.284 -\newcommand{\isasymcdot}{\isamath{\cdot}}
9.285 -\newcommand{\isasymstar}{\isamath{\star}}
9.286 -\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
9.287 -\newcommand{\isasymcirc}{\isamath{\circ}}
9.288 -\newcommand{\isasymdagger}{\isamath{\dagger}}
9.289 -\newcommand{\isasymddagger}{\isamath{\ddagger}}
9.290 -\newcommand{\isasymlhd}{\isamath{\lhd}} %requires amssymb
9.291 -\newcommand{\isasymrhd}{\isamath{\rhd}} %requires amssymb
9.292 -\newcommand{\isasymunlhd}{\isamath{\unlhd}} %requires amssymb
9.293 -\newcommand{\isasymunrhd}{\isamath{\unrhd}} %requires amssymb
9.294 -\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
9.295 -\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
9.296 -\newcommand{\isasymtriangle}{\isamath{\triangle}}
9.297 -\newcommand{\isasymtriangleq}{\isamath{\triangleq}} %requires amssymb
9.298 -\newcommand{\isasymoplus}{\isamath{\oplus}}
9.299 -\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}
9.300 -\newcommand{\isasymotimes}{\isamath{\otimes}}
9.301 -\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}
9.302 -\newcommand{\isasymodot}{\isamath{\odot}}
9.303 -\newcommand{\isasymOdot}{\isamath{\bigodot\,}}
9.304 -\newcommand{\isasymominus}{\isamath{\ominus}}
9.305 -\newcommand{\isasymoslash}{\isamath{\oslash}}
9.306 -\newcommand{\isasymdots}{\isamath{\dots}}
9.307 -\newcommand{\isasymcdots}{\isamath{\cdots}}
9.308 -\newcommand{\isasymSum}{\isamath{\sum\,}}
9.309 -\newcommand{\isasymProd}{\isamath{\prod\,}}
9.310 -\newcommand{\isasymCoprod}{\isamath{\coprod\,}}
9.311 -\newcommand{\isasyminfinity}{\isamath{\infty}}
9.312 -\newcommand{\isasymintegral}{\isamath{\int\,}}
9.313 -\newcommand{\isasymointegral}{\isamath{\oint\,}}
9.314 -\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
9.315 -\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
9.316 -\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
9.317 -\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
9.318 -\newcommand{\isasymaleph}{\isamath{\aleph}}
9.319 -\newcommand{\isasymemptyset}{\isamath{\emptyset}}
9.320 -\newcommand{\isasymnabla}{\isamath{\nabla}}
9.321 -\newcommand{\isasympartial}{\isamath{\partial}}
9.322 -\newcommand{\isasymRe}{\isamath{\Re}}
9.323 -\newcommand{\isasymIm}{\isamath{\Im}}
9.324 -\newcommand{\isasymflat}{\isamath{\flat}}
9.325 -\newcommand{\isasymnatural}{\isamath{\natural}}
9.326 -\newcommand{\isasymsharp}{\isamath{\sharp}}
9.327 -\newcommand{\isasymangle}{\isamath{\angle}}
9.328 -\newcommand{\isasymcopyright}{\isatext{\rm\copyright}}
9.329 -\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
9.330 -\newcommand{\isasymhyphen}{\isatext{\rm-}}
9.331 -\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
9.332 -\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}} %requires latin1
9.333 -\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}} %requires latin1
9.334 -\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}} %requires latin1
9.335 -\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}} %requires latin1
9.336 -\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}} %requires latin1
9.337 -\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}} %requires latin1
9.338 -\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
9.339 -\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
9.340 -\newcommand{\isasymsection}{\isatext{\rm\S}}
9.341 -\newcommand{\isasymparagraph}{\isatext{\rm\P}}
9.342 -\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
9.343 -\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
9.344 -\newcommand{\isasymeuro}{\isatext{\textgreek{\euro}}} %requires greek babel
9.345 -\newcommand{\isasympounds}{\isamath{\pounds}}
9.346 -\newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb
9.347 -\newcommand{\isasymcent}{\isatext{\textcent}} %requires textcomp
9.348 -\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
9.349 -\newcommand{\isasymdegree}{\isatext{\rm\textdegree}} %requires latin1
9.350 -\newcommand{\isasymamalg}{\isamath{\amalg}}
9.351 -\newcommand{\isasymmho}{\isamath{\mho}} %requires amssymb
9.352 -\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssymb
9.353 -\newcommand{\isasymwp}{\isamath{\wp}}
9.354 -\newcommand{\isasymwrong}{\isamath{\wr}}
9.355 -\newcommand{\isasymstruct}{\isamath{\diamond}}
9.356 -\newcommand{\isasymacute}{\isatext{\'\relax}}
9.357 -\newcommand{\isasymindex}{\isatext{\i}}
9.358 -\newcommand{\isasymdieresis}{\isatext{\"\relax}}
9.359 -\newcommand{\isasymcedilla}{\isatext{\c\relax}}
9.360 -\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
9.361 -\newcommand{\isasymspacespace}{\isamath{~~}}
9.362 -\newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}
9.363 -\newcommand{\isasymsome}{\isamath{\epsilon\,}}
10.1 --- a/doc-src/TutorialI/Makefile Thu May 15 20:02:44 2008 +0200
10.2 +++ b/doc-src/TutorialI/Makefile Thu May 15 20:14:10 2008 +0200
10.3 @@ -14,20 +14,17 @@
10.4 SEDINDEX = ./isa-index
10.5
10.6 NAME = tutorial
10.7 -FILES = tutorial.tex basics.tex fp.tex appendix.tex \
10.8 - Advanced/advanced.tex \
10.9 - CTL/ctl.tex \
10.10 - Inductive/inductive.tex Inductive/document/AB.tex \
10.11 - Inductive/document/Advanced.tex Inductive/document/Even.tex \
10.12 - Inductive/document/Mutual.tex Inductive/document/Star.tex \
10.13 - Protocol/protocol.tex Protocol/document/Event.tex \
10.14 - Protocol/document/Message.tex Protocol/document/Public.tex \
10.15 - Protocol/document/NS_Public.tex \
10.16 - Rules/rules.tex Sets/sets.tex \
10.17 - Types/numerics.tex Types/types.tex \
10.18 - Documents/documents.tex \
10.19 - ../iman.sty ../ttbox.sty ../extra.sty \
10.20 - isabelle.sty isabellesym.sty ../pdfsetup.sty
10.21 +FILES = tutorial.tex basics.tex fp.tex appendix.tex \
10.22 + Advanced/advanced.tex CTL/ctl.tex Inductive/inductive.tex \
10.23 + Inductive/document/AB.tex Inductive/document/Advanced.tex \
10.24 + Inductive/document/Even.tex Inductive/document/Mutual.tex \
10.25 + Inductive/document/Star.tex Protocol/protocol.tex \
10.26 + Protocol/document/Event.tex Protocol/document/Message.tex \
10.27 + Protocol/document/Public.tex Protocol/document/NS_Public.tex \
10.28 + Rules/rules.tex Sets/sets.tex Types/numerics.tex \
10.29 + Types/types.tex Documents/documents.tex ../iman.sty \
10.30 + ../ttbox.sty ../extra.sty ../isabelle.sty ../isabellesym.sty \
10.31 + ../pdfsetup.sty
10.32
10.33 dvi: $(NAME).dvi
10.34
11.1 --- a/doc-src/TutorialI/isabelle.sty Thu May 15 20:02:44 2008 +0200
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,215 +0,0 @@
11.4 -%%
11.5 -%%
11.6 -%%
11.7 -%% macros for Isabelle generated LaTeX output
11.8 -%%
11.9 -
11.10 -%%% Simple document preparation (based on theory token language and symbols)
11.11 -
11.12 -% isabelle environments
11.13 -
11.14 -\newcommand{\isabellecontext}{UNKNOWN}
11.15 -
11.16 -\newcommand{\isastyle}{\UNDEF}
11.17 -\newcommand{\isastyleminor}{\UNDEF}
11.18 -\newcommand{\isastylescript}{\UNDEF}
11.19 -\newcommand{\isastyletext}{\normalsize\rm}
11.20 -\newcommand{\isastyletxt}{\rm}
11.21 -\newcommand{\isastylecmt}{\rm}
11.22 -
11.23 -%symbol markup -- \emph achieves decent spacing via italic corrections
11.24 -\newcommand{\isamath}[1]{\emph{$#1$}}
11.25 -\newcommand{\isatext}[1]{\emph{#1}}
11.26 -\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
11.27 -\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
11.28 -\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
11.29 -\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
11.30 -\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
11.31 -\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isastylescript}
11.32 -\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
11.33 -\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isastylescript}
11.34 -\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
11.35 -\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
11.36 -\newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
11.37 -\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
11.38 -
11.39 -
11.40 -\newdimen\isa@parindent\newdimen\isa@parskip
11.41 -
11.42 -\newenvironment{isabellebody}{%
11.43 -\isamarkuptrue\par%
11.44 -\isa@parindent\parindent\parindent0pt%
11.45 -\isa@parskip\parskip\parskip0pt%
11.46 -\isastyle}{\par}
11.47 -
11.48 -\newenvironment{isabelle}
11.49 -{\begin{trivlist}\begin{isabellebody}\item\relax}
11.50 -{\end{isabellebody}\end{trivlist}}
11.51 -
11.52 -\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
11.53 -
11.54 -\newcommand{\isaindent}[1]{\hphantom{#1}}
11.55 -\newcommand{\isanewline}{\mbox{}\par\mbox{}}
11.56 -\newcommand{\isasep}{}
11.57 -\newcommand{\isadigit}[1]{#1}
11.58 -
11.59 -\newcommand{\isachardefaults}{%
11.60 -\chardef\isacharbang=`\!%
11.61 -\chardef\isachardoublequote=`\"%
11.62 -\chardef\isachardoublequoteopen=`\"%
11.63 -\chardef\isachardoublequoteclose=`\"%
11.64 -\chardef\isacharhash=`\#%
11.65 -\chardef\isachardollar=`\$%
11.66 -\chardef\isacharpercent=`\%%
11.67 -\chardef\isacharampersand=`\&%
11.68 -\chardef\isacharprime=`\'%
11.69 -\chardef\isacharparenleft=`\(%
11.70 -\chardef\isacharparenright=`\)%
11.71 -\chardef\isacharasterisk=`\*%
11.72 -\chardef\isacharplus=`\+%
11.73 -\chardef\isacharcomma=`\,%
11.74 -\chardef\isacharminus=`\-%
11.75 -\chardef\isachardot=`\.%
11.76 -\chardef\isacharslash=`\/%
11.77 -\chardef\isacharcolon=`\:%
11.78 -\chardef\isacharsemicolon=`\;%
11.79 -\chardef\isacharless=`\<%
11.80 -\chardef\isacharequal=`\=%
11.81 -\chardef\isachargreater=`\>%
11.82 -\chardef\isacharquery=`\?%
11.83 -\chardef\isacharat=`\@%
11.84 -\chardef\isacharbrackleft=`\[%
11.85 -\chardef\isacharbackslash=`\\%
11.86 -\chardef\isacharbrackright=`\]%
11.87 -\chardef\isacharcircum=`\^%
11.88 -\chardef\isacharunderscore=`\_%
11.89 -\def\isacharunderscorekeyword{\_}%
11.90 -\chardef\isacharbackquote=`\`%
11.91 -\chardef\isacharbackquoteopen=`\`%
11.92 -\chardef\isacharbackquoteclose=`\`%
11.93 -\chardef\isacharbraceleft=`\{%
11.94 -\chardef\isacharbar=`\|%
11.95 -\chardef\isacharbraceright=`\}%
11.96 -\chardef\isachartilde=`\~%
11.97 -\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
11.98 -\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
11.99 -}
11.100 -
11.101 -
11.102 -% keyword and section markup
11.103 -
11.104 -\newcommand{\isakeyword}[1]
11.105 -{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
11.106 -\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
11.107 -\newcommand{\isacommand}[1]{\isakeyword{#1}}
11.108 -
11.109 -\newcommand{\isamarkupheader}[1]{\section{#1}}
11.110 -\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
11.111 -\newcommand{\isamarkupsection}[1]{\section{#1}}
11.112 -\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
11.113 -\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
11.114 -\newcommand{\isamarkupsect}[1]{\section{#1}}
11.115 -\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
11.116 -\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
11.117 -
11.118 -\newif\ifisamarkup
11.119 -\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
11.120 -\newcommand{\isaendpar}{\par\medskip}
11.121 -\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
11.122 -\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
11.123 -\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
11.124 -\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
11.125 -
11.126 -
11.127 -% styles
11.128 -
11.129 -\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
11.130 -
11.131 -\newcommand{\isabellestyledefault}{%
11.132 -\renewcommand{\isastyle}{\small\tt\slshape}%
11.133 -\renewcommand{\isastyleminor}{\small\tt\slshape}%
11.134 -\renewcommand{\isastylescript}{\footnotesize\tt\slshape}%
11.135 -\isachardefaults%
11.136 -}
11.137 -\isabellestyledefault
11.138 -
11.139 -\newcommand{\isabellestylett}{%
11.140 -\renewcommand{\isastyle}{\small\tt}%
11.141 -\renewcommand{\isastyleminor}{\small\tt}%
11.142 -\renewcommand{\isastylescript}{\footnotesize\tt}%
11.143 -\isachardefaults%
11.144 -}
11.145 -
11.146 -\newcommand{\isabellestyleit}{%
11.147 -\renewcommand{\isastyle}{\small\it}%
11.148 -\renewcommand{\isastyleminor}{\it}%
11.149 -\renewcommand{\isastylescript}{\footnotesize\it}%
11.150 -\renewcommand{\isacharunderscorekeyword}{\mbox{-}}%
11.151 -\renewcommand{\isacharbang}{\isamath{!}}%
11.152 -\renewcommand{\isachardoublequote}{}%
11.153 -\renewcommand{\isachardoublequoteopen}{}%
11.154 -\renewcommand{\isachardoublequoteclose}{}%
11.155 -\renewcommand{\isacharhash}{\isamath{\#}}%
11.156 -\renewcommand{\isachardollar}{\isamath{\$}}%
11.157 -\renewcommand{\isacharpercent}{\isamath{\%}}%
11.158 -\renewcommand{\isacharampersand}{\isamath{\&}}%
11.159 -\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
11.160 -\renewcommand{\isacharparenleft}{\isamath{(}}%
11.161 -\renewcommand{\isacharparenright}{\isamath{)}}%
11.162 -\renewcommand{\isacharasterisk}{\isamath{*}}%
11.163 -\renewcommand{\isacharplus}{\isamath{+}}%
11.164 -\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
11.165 -\renewcommand{\isacharminus}{\isamath{-}}%
11.166 -\renewcommand{\isachardot}{\isamath{\mathord.}}%
11.167 -\renewcommand{\isacharslash}{\isamath{/}}%
11.168 -\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
11.169 -\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
11.170 -\renewcommand{\isacharless}{\isamath{<}}%
11.171 -\renewcommand{\isacharequal}{\isamath{=}}%
11.172 -\renewcommand{\isachargreater}{\isamath{>}}%
11.173 -\renewcommand{\isacharat}{\isamath{@}}%
11.174 -\renewcommand{\isacharbrackleft}{\isamath{[}}%
11.175 -\renewcommand{\isacharbackslash}{\isamath{\backslash}}%
11.176 -\renewcommand{\isacharbrackright}{\isamath{]}}%
11.177 -\renewcommand{\isacharunderscore}{\mbox{-}}%
11.178 -\renewcommand{\isacharbraceleft}{\isamath{\{}}%
11.179 -\renewcommand{\isacharbar}{\isamath{\mid}}%
11.180 -\renewcommand{\isacharbraceright}{\isamath{\}}}%
11.181 -\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
11.182 -\renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
11.183 -\renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
11.184 -\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}%
11.185 -\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}%
11.186 -}
11.187 -
11.188 -\newcommand{\isabellestylesl}{%
11.189 -\isabellestyleit%
11.190 -\renewcommand{\isastyle}{\small\sl}%
11.191 -\renewcommand{\isastyleminor}{\sl}%
11.192 -\renewcommand{\isastylescript}{\footnotesize\sl}%
11.193 -}
11.194 -
11.195 -
11.196 -% tagged regions
11.197 -
11.198 -%plain TeX version of comment package -- much faster!
11.199 -\let\isafmtname\fmtname\def\fmtname{plain}
11.200 -\usepackage{comment}
11.201 -\let\fmtname\isafmtname
11.202 -
11.203 -\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
11.204 -
11.205 -\newcommand{\isakeeptag}[1]%
11.206 -{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
11.207 -\newcommand{\isadroptag}[1]%
11.208 -{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
11.209 -\newcommand{\isafoldtag}[1]%
11.210 -{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
11.211 -
11.212 -\isakeeptag{theory}
11.213 -\isakeeptag{proof}
11.214 -\isakeeptag{ML}
11.215 -\isakeeptag{visible}
11.216 -\isadroptag{invisible}
11.217 -
11.218 -\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}
12.1 --- a/doc-src/TutorialI/isabellesym.sty Thu May 15 20:02:44 2008 +0200
12.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
12.3 @@ -1,360 +0,0 @@
12.4 -%%
12.5 -%%
12.6 -%%
12.7 -%% definitions of standard Isabelle symbols
12.8 -%%
12.9 -
12.10 -\newcommand{\isasymzero}{\isamath{\mathbf{0}}} %requires amssymb
12.11 -\newcommand{\isasymone}{\isamath{\mathbf{1}}} %requires amssymb
12.12 -\newcommand{\isasymtwo}{\isamath{\mathbf{2}}} %requires amssymb
12.13 -\newcommand{\isasymthree}{\isamath{\mathbf{3}}} %requires amssymb
12.14 -\newcommand{\isasymfour}{\isamath{\mathbf{4}}} %requires amssymb
12.15 -\newcommand{\isasymfive}{\isamath{\mathbf{5}}} %requires amssymb
12.16 -\newcommand{\isasymsix}{\isamath{\mathbf{6}}} %requires amssymb
12.17 -\newcommand{\isasymseven}{\isamath{\mathbf{7}}} %requires amssymb
12.18 -\newcommand{\isasymeight}{\isamath{\mathbf{8}}} %requires amssymb
12.19 -\newcommand{\isasymnine}{\isamath{\mathbf{9}}} %requires amssymb
12.20 -\newcommand{\isasymA}{\isamath{\mathcal{A}}}
12.21 -\newcommand{\isasymB}{\isamath{\mathcal{B}}}
12.22 -\newcommand{\isasymC}{\isamath{\mathcal{C}}}
12.23 -\newcommand{\isasymD}{\isamath{\mathcal{D}}}
12.24 -\newcommand{\isasymE}{\isamath{\mathcal{E}}}
12.25 -\newcommand{\isasymF}{\isamath{\mathcal{F}}}
12.26 -\newcommand{\isasymG}{\isamath{\mathcal{G}}}
12.27 -\newcommand{\isasymH}{\isamath{\mathcal{H}}}
12.28 -\newcommand{\isasymI}{\isamath{\mathcal{I}}}
12.29 -\newcommand{\isasymJ}{\isamath{\mathcal{J}}}
12.30 -\newcommand{\isasymK}{\isamath{\mathcal{K}}}
12.31 -\newcommand{\isasymL}{\isamath{\mathcal{L}}}
12.32 -\newcommand{\isasymM}{\isamath{\mathcal{M}}}
12.33 -\newcommand{\isasymN}{\isamath{\mathcal{N}}}
12.34 -\newcommand{\isasymO}{\isamath{\mathcal{O}}}
12.35 -\newcommand{\isasymP}{\isamath{\mathcal{P}}}
12.36 -\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}
12.37 -\newcommand{\isasymR}{\isamath{\mathcal{R}}}
12.38 -\newcommand{\isasymS}{\isamath{\mathcal{S}}}
12.39 -\newcommand{\isasymT}{\isamath{\mathcal{T}}}
12.40 -\newcommand{\isasymU}{\isamath{\mathcal{U}}}
12.41 -\newcommand{\isasymV}{\isamath{\mathcal{V}}}
12.42 -\newcommand{\isasymW}{\isamath{\mathcal{W}}}
12.43 -\newcommand{\isasymX}{\isamath{\mathcal{X}}}
12.44 -\newcommand{\isasymY}{\isamath{\mathcal{Y}}}
12.45 -\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
12.46 -\newcommand{\isasyma}{\isamath{\mathrm{a}}}
12.47 -\newcommand{\isasymb}{\isamath{\mathrm{b}}}
12.48 -\newcommand{\isasymc}{\isamath{\mathrm{c}}}
12.49 -\newcommand{\isasymd}{\isamath{\mathrm{d}}}
12.50 -\newcommand{\isasyme}{\isamath{\mathrm{e}}}
12.51 -\newcommand{\isasymf}{\isamath{\mathrm{f}}}
12.52 -\newcommand{\isasymg}{\isamath{\mathrm{g}}}
12.53 -\newcommand{\isasymh}{\isamath{\mathrm{h}}}
12.54 -\newcommand{\isasymi}{\isamath{\mathrm{i}}}
12.55 -\newcommand{\isasymj}{\isamath{\mathrm{j}}}
12.56 -\newcommand{\isasymk}{\isamath{\mathrm{k}}}
12.57 -\newcommand{\isasyml}{\isamath{\mathrm{l}}}
12.58 -\newcommand{\isasymm}{\isamath{\mathrm{m}}}
12.59 -\newcommand{\isasymn}{\isamath{\mathrm{n}}}
12.60 -\newcommand{\isasymo}{\isamath{\mathrm{o}}}
12.61 -\newcommand{\isasymp}{\isamath{\mathrm{p}}}
12.62 -\newcommand{\isasymq}{\isamath{\mathrm{q}}}
12.63 -\newcommand{\isasymr}{\isamath{\mathrm{r}}}
12.64 -\newcommand{\isasyms}{\isamath{\mathrm{s}}}
12.65 -\newcommand{\isasymt}{\isamath{\mathrm{t}}}
12.66 -\newcommand{\isasymu}{\isamath{\mathrm{u}}}
12.67 -\newcommand{\isasymv}{\isamath{\mathrm{v}}}
12.68 -\newcommand{\isasymw}{\isamath{\mathrm{w}}}
12.69 -\newcommand{\isasymx}{\isamath{\mathrm{x}}}
12.70 -\newcommand{\isasymy}{\isamath{\mathrm{y}}}
12.71 -\newcommand{\isasymz}{\isamath{\mathrm{z}}}
12.72 -\newcommand{\isasymAA}{\isamath{\mathfrak{A}}} %requires eufrak
12.73 -\newcommand{\isasymBB}{\isamath{\mathfrak{B}}} %requires eufrak
12.74 -\newcommand{\isasymCC}{\isamath{\mathfrak{C}}} %requires eufrak
12.75 -\newcommand{\isasymDD}{\isamath{\mathfrak{D}}} %requires eufrak
12.76 -\newcommand{\isasymEE}{\isamath{\mathfrak{E}}} %requires eufrak
12.77 -\newcommand{\isasymFF}{\isamath{\mathfrak{F}}} %requires eufrak
12.78 -\newcommand{\isasymGG}{\isamath{\mathfrak{G}}} %requires eufrak
12.79 -\newcommand{\isasymHH}{\isamath{\mathfrak{H}}} %requires eufrak
12.80 -\newcommand{\isasymII}{\isamath{\mathfrak{I}}} %requires eufrak
12.81 -\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}} %requires eufrak
12.82 -\newcommand{\isasymKK}{\isamath{\mathfrak{K}}} %requires eufrak
12.83 -\newcommand{\isasymLL}{\isamath{\mathfrak{L}}} %requires eufrak
12.84 -\newcommand{\isasymMM}{\isamath{\mathfrak{M}}} %requires eufrak
12.85 -\newcommand{\isasymNN}{\isamath{\mathfrak{N}}} %requires eufrak
12.86 -\newcommand{\isasymOO}{\isamath{\mathfrak{O}}} %requires eufrak
12.87 -\newcommand{\isasymPP}{\isamath{\mathfrak{P}}} %requires eufrak
12.88 -\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}} %requires eufrak
12.89 -\newcommand{\isasymRR}{\isamath{\mathfrak{R}}} %requires eufrak
12.90 -\newcommand{\isasymSS}{\isamath{\mathfrak{S}}} %requires eufrak
12.91 -\newcommand{\isasymTT}{\isamath{\mathfrak{T}}} %requires eufrak
12.92 -\newcommand{\isasymUU}{\isamath{\mathfrak{U}}} %requires eufrak
12.93 -\newcommand{\isasymVV}{\isamath{\mathfrak{V}}} %requires eufrak
12.94 -\newcommand{\isasymWW}{\isamath{\mathfrak{W}}} %requires eufrak
12.95 -\newcommand{\isasymXX}{\isamath{\mathfrak{X}}} %requires eufrak
12.96 -\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}} %requires eufrak
12.97 -\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}} %requires eufrak
12.98 -\newcommand{\isasymaa}{\isamath{\mathfrak{a}}} %requires eufrak
12.99 -\newcommand{\isasymbb}{\isamath{\mathfrak{b}}} %requires eufrak
12.100 -\newcommand{\isasymcc}{\isamath{\mathfrak{c}}} %requires eufrak
12.101 -\newcommand{\isasymdd}{\isamath{\mathfrak{d}}} %requires eufrak
12.102 -\newcommand{\isasymee}{\isamath{\mathfrak{e}}} %requires eufrak
12.103 -\newcommand{\isasymff}{\isamath{\mathfrak{f}}} %requires eufrak
12.104 -\newcommand{\isasymgg}{\isamath{\mathfrak{g}}} %requires eufrak
12.105 -\newcommand{\isasymhh}{\isamath{\mathfrak{h}}} %requires eufrak
12.106 -\newcommand{\isasymii}{\isamath{\mathfrak{i}}} %requires eufrak
12.107 -\newcommand{\isasymjj}{\isamath{\mathfrak{j}}} %requires eufrak
12.108 -\newcommand{\isasymkk}{\isamath{\mathfrak{k}}} %requires eufrak
12.109 -\newcommand{\isasymll}{\isamath{\mathfrak{l}}} %requires eufrak
12.110 -\newcommand{\isasymmm}{\isamath{\mathfrak{m}}} %requires eufrak
12.111 -\newcommand{\isasymnn}{\isamath{\mathfrak{n}}} %requires eufrak
12.112 -\newcommand{\isasymoo}{\isamath{\mathfrak{o}}} %requires eufrak
12.113 -\newcommand{\isasympp}{\isamath{\mathfrak{p}}} %requires eufrak
12.114 -\newcommand{\isasymqq}{\isamath{\mathfrak{q}}} %requires eufrak
12.115 -\newcommand{\isasymrr}{\isamath{\mathfrak{r}}} %requires eufrak
12.116 -\newcommand{\isasymss}{\isamath{\mathfrak{s}}} %requires eufrak
12.117 -\newcommand{\isasymtt}{\isamath{\mathfrak{t}}} %requires eufrak
12.118 -\newcommand{\isasymuu}{\isamath{\mathfrak{u}}} %requires eufrak
12.119 -\newcommand{\isasymvv}{\isamath{\mathfrak{v}}} %requires eufrak
12.120 -\newcommand{\isasymww}{\isamath{\mathfrak{w}}} %requires eufrak
12.121 -\newcommand{\isasymxx}{\isamath{\mathfrak{x}}} %requires eufrak
12.122 -\newcommand{\isasymyy}{\isamath{\mathfrak{y}}} %requires eufrak
12.123 -\newcommand{\isasymzz}{\isamath{\mathfrak{z}}} %requires eufrak
12.124 -\newcommand{\isasymalpha}{\isamath{\alpha}}
12.125 -\newcommand{\isasymbeta}{\isamath{\beta}}
12.126 -\newcommand{\isasymgamma}{\isamath{\gamma}}
12.127 -\newcommand{\isasymdelta}{\isamath{\delta}}
12.128 -\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
12.129 -\newcommand{\isasymzeta}{\isamath{\zeta}}
12.130 -\newcommand{\isasymeta}{\isamath{\eta}}
12.131 -\newcommand{\isasymtheta}{\isamath{\vartheta}}
12.132 -\newcommand{\isasymiota}{\isamath{\iota}}
12.133 -\newcommand{\isasymkappa}{\isamath{\kappa}}
12.134 -\newcommand{\isasymlambda}{\isamath{\lambda}}
12.135 -\newcommand{\isasymmu}{\isamath{\mu}}
12.136 -\newcommand{\isasymnu}{\isamath{\nu}}
12.137 -\newcommand{\isasymxi}{\isamath{\xi}}
12.138 -\newcommand{\isasympi}{\isamath{\pi}}
12.139 -\newcommand{\isasymrho}{\isamath{\varrho}}
12.140 -\newcommand{\isasymsigma}{\isamath{\sigma}}
12.141 -\newcommand{\isasymtau}{\isamath{\tau}}
12.142 -\newcommand{\isasymupsilon}{\isamath{\upsilon}}
12.143 -\newcommand{\isasymphi}{\isamath{\varphi}}
12.144 -\newcommand{\isasymchi}{\isamath{\chi}}
12.145 -\newcommand{\isasympsi}{\isamath{\psi}}
12.146 -\newcommand{\isasymomega}{\isamath{\omega}}
12.147 -\newcommand{\isasymGamma}{\isamath{\Gamma}}
12.148 -\newcommand{\isasymDelta}{\isamath{\Delta}}
12.149 -\newcommand{\isasymTheta}{\isamath{\Theta}}
12.150 -\newcommand{\isasymLambda}{\isamath{\Lambda}}
12.151 -\newcommand{\isasymXi}{\isamath{\Xi}}
12.152 -\newcommand{\isasymPi}{\isamath{\Pi}}
12.153 -\newcommand{\isasymSigma}{\isamath{\Sigma}}
12.154 -\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
12.155 -\newcommand{\isasymPhi}{\isamath{\Phi}}
12.156 -\newcommand{\isasymPsi}{\isamath{\Psi}}
12.157 -\newcommand{\isasymOmega}{\isamath{\Omega}}
12.158 -\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
12.159 -\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
12.160 -\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
12.161 -\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
12.162 -\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
12.163 -\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
12.164 -\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
12.165 -\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
12.166 -\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
12.167 -\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
12.168 -\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
12.169 -\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
12.170 -\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
12.171 -\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
12.172 -\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
12.173 -\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
12.174 -\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
12.175 -\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
12.176 -\newcommand{\isasymmapsto}{\isamath{\mapsto}}
12.177 -\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
12.178 -\newcommand{\isasymmidarrow}{\isamath{\relbar}}
12.179 -\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
12.180 -\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
12.181 -\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
12.182 -\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
12.183 -\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
12.184 -\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
12.185 -\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
12.186 -\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
12.187 -\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
12.188 -\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}} %requires amssymb
12.189 -\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}} %requires amssymb
12.190 -\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}} %requires amssymb
12.191 -\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}} %requires amssymb
12.192 -\newcommand{\isasymrestriction}{\isamath{\restriction}} %requires amssymb
12.193 -\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
12.194 -\newcommand{\isasymup}{\isamath{\uparrow}}
12.195 -\newcommand{\isasymUp}{\isamath{\Uparrow}}
12.196 -\newcommand{\isasymdown}{\isamath{\downarrow}}
12.197 -\newcommand{\isasymDown}{\isamath{\Downarrow}}
12.198 -\newcommand{\isasymupdown}{\isamath{\updownarrow}}
12.199 -\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
12.200 -\newcommand{\isasymlangle}{\isamath{\langle}}
12.201 -\newcommand{\isasymrangle}{\isamath{\rangle}}
12.202 -\newcommand{\isasymlceil}{\isamath{\lceil}}
12.203 -\newcommand{\isasymrceil}{\isamath{\rceil}}
12.204 -\newcommand{\isasymlfloor}{\isamath{\lfloor}}
12.205 -\newcommand{\isasymrfloor}{\isamath{\rfloor}}
12.206 -\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
12.207 -\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}
12.208 -\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
12.209 -\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
12.210 -\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
12.211 -\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
12.212 -\newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel
12.213 -\newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel
12.214 -\newcommand{\isasymbottom}{\isamath{\bot}}
12.215 -\newcommand{\isasymtop}{\isamath{\top}}
12.216 -\newcommand{\isasymand}{\isamath{\wedge}}
12.217 -\newcommand{\isasymAnd}{\isamath{\bigwedge}}
12.218 -\newcommand{\isasymor}{\isamath{\vee}}
12.219 -\newcommand{\isasymOr}{\isamath{\bigvee}}
12.220 -\newcommand{\isasymforall}{\isamath{\forall\,}}
12.221 -\newcommand{\isasymexists}{\isamath{\exists\,}}
12.222 -\newcommand{\isasymnexists}{\isamath{\nexists\,}} %requires amssymb
12.223 -\newcommand{\isasymnot}{\isamath{\neg}}
12.224 -\newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb
12.225 -\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb
12.226 -\newcommand{\isasymturnstile}{\isamath{\vdash}}
12.227 -\newcommand{\isasymTurnstile}{\isamath{\models}}
12.228 -\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
12.229 -\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
12.230 -\newcommand{\isasymstileturn}{\isamath{\dashv}}
12.231 -\newcommand{\isasymsurd}{\isamath{\surd}}
12.232 -\newcommand{\isasymle}{\isamath{\le}}
12.233 -\newcommand{\isasymge}{\isamath{\ge}}
12.234 -\newcommand{\isasymlless}{\isamath{\ll}}
12.235 -\newcommand{\isasymggreater}{\isamath{\gg}}
12.236 -\newcommand{\isasymlesssim}{\isamath{\lesssim}} %requires amssymb
12.237 -\newcommand{\isasymgreatersim}{\isamath{\gtrsim}} %requires amssymb
12.238 -\newcommand{\isasymlessapprox}{\isamath{\lessapprox}} %requires amssymb
12.239 -\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}} %requires amssymb
12.240 -\newcommand{\isasymin}{\isamath{\in}}
12.241 -\newcommand{\isasymnotin}{\isamath{\notin}}
12.242 -\newcommand{\isasymsubset}{\isamath{\subset}}
12.243 -\newcommand{\isasymsupset}{\isamath{\supset}}
12.244 -\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
12.245 -\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
12.246 -\newcommand{\isasymsqsubset}{\isamath{\sqsubset}} %requires amssymb
12.247 -\newcommand{\isasymsqsupset}{\isamath{\sqsupset}} %requires amssymb
12.248 -\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
12.249 -\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
12.250 -\newcommand{\isasyminter}{\isamath{\cap}}
12.251 -\newcommand{\isasymInter}{\isamath{\bigcap\,}}
12.252 -\newcommand{\isasymunion}{\isamath{\cup}}
12.253 -\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
12.254 -\newcommand{\isasymsqunion}{\isamath{\sqcup}}
12.255 -\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
12.256 -\newcommand{\isasymsqinter}{\isamath{\sqcap}}
12.257 -\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires amsmath
12.258 -\newcommand{\isasymsetminus}{\isamath{\setminus}}
12.259 -\newcommand{\isasympropto}{\isamath{\propto}}
12.260 -\newcommand{\isasymuplus}{\isamath{\uplus}}
12.261 -\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
12.262 -\newcommand{\isasymnoteq}{\isamath{\not=}}
12.263 -\newcommand{\isasymsim}{\isamath{\sim}}
12.264 -\newcommand{\isasymdoteq}{\isamath{\doteq}}
12.265 -\newcommand{\isasymsimeq}{\isamath{\simeq}}
12.266 -\newcommand{\isasymapprox}{\isamath{\approx}}
12.267 -\newcommand{\isasymasymp}{\isamath{\asymp}}
12.268 -\newcommand{\isasymcong}{\isamath{\cong}}
12.269 -\newcommand{\isasymsmile}{\isamath{\smile}}
12.270 -\newcommand{\isasymequiv}{\isamath{\equiv}}
12.271 -\newcommand{\isasymfrown}{\isamath{\frown}}
12.272 -\newcommand{\isasymJoin}{\isamath{\Join}} %requires amssymb
12.273 -\newcommand{\isasymbowtie}{\isamath{\bowtie}}
12.274 -\newcommand{\isasymprec}{\isamath{\prec}}
12.275 -\newcommand{\isasymsucc}{\isamath{\succ}}
12.276 -\newcommand{\isasympreceq}{\isamath{\preceq}}
12.277 -\newcommand{\isasymsucceq}{\isamath{\succeq}}
12.278 -\newcommand{\isasymparallel}{\isamath{\parallel}}
12.279 -\newcommand{\isasymbar}{\isamath{\mid}}
12.280 -\newcommand{\isasymplusminus}{\isamath{\pm}}
12.281 -\newcommand{\isasymminusplus}{\isamath{\mp}}
12.282 -\newcommand{\isasymtimes}{\isamath{\times}}
12.283 -\newcommand{\isasymdiv}{\isamath{\div}}
12.284 -\newcommand{\isasymcdot}{\isamath{\cdot}}
12.285 -\newcommand{\isasymstar}{\isamath{\star}}
12.286 -\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
12.287 -\newcommand{\isasymcirc}{\isamath{\circ}}
12.288 -\newcommand{\isasymdagger}{\isamath{\dagger}}
12.289 -\newcommand{\isasymddagger}{\isamath{\ddagger}}
12.290 -\newcommand{\isasymlhd}{\isamath{\lhd}} %requires amssymb
12.291 -\newcommand{\isasymrhd}{\isamath{\rhd}} %requires amssymb
12.292 -\newcommand{\isasymunlhd}{\isamath{\unlhd}} %requires amssymb
12.293 -\newcommand{\isasymunrhd}{\isamath{\unrhd}} %requires amssymb
12.294 -\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
12.295 -\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
12.296 -\newcommand{\isasymtriangle}{\isamath{\triangle}}
12.297 -\newcommand{\isasymtriangleq}{\isamath{\triangleq}} %requires amssymb
12.298 -\newcommand{\isasymoplus}{\isamath{\oplus}}
12.299 -\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}
12.300 -\newcommand{\isasymotimes}{\isamath{\otimes}}
12.301 -\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}
12.302 -\newcommand{\isasymodot}{\isamath{\odot}}
12.303 -\newcommand{\isasymOdot}{\isamath{\bigodot\,}}
12.304 -\newcommand{\isasymominus}{\isamath{\ominus}}
12.305 -\newcommand{\isasymoslash}{\isamath{\oslash}}
12.306 -\newcommand{\isasymdots}{\isamath{\dots}}
12.307 -\newcommand{\isasymcdots}{\isamath{\cdots}}
12.308 -\newcommand{\isasymSum}{\isamath{\sum\,}}
12.309 -\newcommand{\isasymProd}{\isamath{\prod\,}}
12.310 -\newcommand{\isasymCoprod}{\isamath{\coprod\,}}
12.311 -\newcommand{\isasyminfinity}{\isamath{\infty}}
12.312 -\newcommand{\isasymintegral}{\isamath{\int\,}}
12.313 -\newcommand{\isasymointegral}{\isamath{\oint\,}}
12.314 -\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
12.315 -\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
12.316 -\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
12.317 -\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
12.318 -\newcommand{\isasymaleph}{\isamath{\aleph}}
12.319 -\newcommand{\isasymemptyset}{\isamath{\emptyset}}
12.320 -\newcommand{\isasymnabla}{\isamath{\nabla}}
12.321 -\newcommand{\isasympartial}{\isamath{\partial}}
12.322 -\newcommand{\isasymRe}{\isamath{\Re}}
12.323 -\newcommand{\isasymIm}{\isamath{\Im}}
12.324 -\newcommand{\isasymflat}{\isamath{\flat}}
12.325 -\newcommand{\isasymnatural}{\isamath{\natural}}
12.326 -\newcommand{\isasymsharp}{\isamath{\sharp}}
12.327 -\newcommand{\isasymangle}{\isamath{\angle}}
12.328 -\newcommand{\isasymcopyright}{\isatext{\rm\copyright}}
12.329 -\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
12.330 -\newcommand{\isasymhyphen}{\isatext{\rm-}}
12.331 -\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
12.332 -\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}} %requires latin1
12.333 -\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}} %requires latin1
12.334 -\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}} %requires latin1
12.335 -\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}} %requires latin1
12.336 -\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}} %requires latin1
12.337 -\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}} %requires latin1
12.338 -\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
12.339 -\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
12.340 -\newcommand{\isasymsection}{\isatext{\rm\S}}
12.341 -\newcommand{\isasymparagraph}{\isatext{\rm\P}}
12.342 -\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
12.343 -\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
12.344 -\newcommand{\isasymeuro}{\isatext{\textgreek{\euro}}} %requires greek babel
12.345 -\newcommand{\isasympounds}{\isamath{\pounds}}
12.346 -\newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb
12.347 -\newcommand{\isasymcent}{\isatext{\textcent}} %requires textcomp
12.348 -\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
12.349 -\newcommand{\isasymdegree}{\isatext{\rm\textdegree}} %requires latin1
12.350 -\newcommand{\isasymamalg}{\isamath{\amalg}}
12.351 -\newcommand{\isasymmho}{\isamath{\mho}} %requires amssymb
12.352 -\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssymb
12.353 -\newcommand{\isasymwp}{\isamath{\wp}}
12.354 -\newcommand{\isasymwrong}{\isamath{\wr}}
12.355 -\newcommand{\isasymstruct}{\isamath{\diamond}}
12.356 -\newcommand{\isasymacute}{\isatext{\'\relax}}
12.357 -\newcommand{\isasymindex}{\isatext{\i}}
12.358 -\newcommand{\isasymdieresis}{\isatext{\"\relax}}
12.359 -\newcommand{\isasymcedilla}{\isatext{\c\relax}}
12.360 -\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
12.361 -\newcommand{\isasymspacespace}{\isamath{~~}}
12.362 -\newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}
12.363 -\newcommand{\isasymsome}{\isamath{\epsilon\,}}
13.1 --- a/doc-src/TutorialI/tutorial.tex Thu May 15 20:02:44 2008 +0200
13.2 +++ b/doc-src/TutorialI/tutorial.tex Thu May 15 20:14:10 2008 +0200
13.3 @@ -1,6 +1,6 @@
13.4 \documentclass{article}
13.5 %%\includeonly{Types/types} %%UNCOMMENT to process only selected chapters
13.6 -\usepackage{cl2emono-modified,isabelle,isabellesym}
13.7 +\usepackage{cl2emono-modified,../isabelle,../isabellesym}
13.8 \usepackage{../proof,amsmath,amsfonts}
13.9 \usepackage{latexsym,wasysym,verbatim,graphicx,tutorial,../ttbox,comment}
13.10 \usepackage[greek,english]{babel}
14.1 --- a/doc-src/ZF/Makefile Thu May 15 20:02:44 2008 +0200
14.2 +++ b/doc-src/ZF/Makefile Thu May 15 20:14:10 2008 +0200
14.3 @@ -12,8 +12,9 @@
14.4 include ../Makefile.in
14.5
14.6 NAME = logics-ZF
14.7 -FILES = logics-ZF.tex ../Logics/syntax.tex FOL.tex ZF.tex logics.sty\
14.8 - ../rail.sty ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
14.9 +FILES = logics-ZF.tex ../Logics/syntax.tex FOL.tex ZF.tex logics.sty \
14.10 + ../rail.sty ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty \
14.11 + ../isabelle.sty ../isabellesym.sty ../pdfsetup.sty ../manual.bib
14.12
14.13 dvi: $(NAME).dvi
14.14
15.1 --- a/doc-src/ZF/isabelle.sty Thu May 15 20:02:44 2008 +0200
15.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
15.3 @@ -1,215 +0,0 @@
15.4 -%%
15.5 -%%
15.6 -%%
15.7 -%% macros for Isabelle generated LaTeX output
15.8 -%%
15.9 -
15.10 -%%% Simple document preparation (based on theory token language and symbols)
15.11 -
15.12 -% isabelle environments
15.13 -
15.14 -\newcommand{\isabellecontext}{UNKNOWN}
15.15 -
15.16 -\newcommand{\isastyle}{\UNDEF}
15.17 -\newcommand{\isastyleminor}{\UNDEF}
15.18 -\newcommand{\isastylescript}{\UNDEF}
15.19 -\newcommand{\isastyletext}{\normalsize\rm}
15.20 -\newcommand{\isastyletxt}{\rm}
15.21 -\newcommand{\isastylecmt}{\rm}
15.22 -
15.23 -%symbol markup -- \emph achieves decent spacing via italic corrections
15.24 -\newcommand{\isamath}[1]{\emph{$#1$}}
15.25 -\newcommand{\isatext}[1]{\emph{#1}}
15.26 -\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
15.27 -\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
15.28 -\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
15.29 -\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
15.30 -\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
15.31 -\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isastylescript}
15.32 -\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
15.33 -\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isastylescript}
15.34 -\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
15.35 -\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
15.36 -\newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
15.37 -\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
15.38 -
15.39 -
15.40 -\newdimen\isa@parindent\newdimen\isa@parskip
15.41 -
15.42 -\newenvironment{isabellebody}{%
15.43 -\isamarkuptrue\par%
15.44 -\isa@parindent\parindent\parindent0pt%
15.45 -\isa@parskip\parskip\parskip0pt%
15.46 -\isastyle}{\par}
15.47 -
15.48 -\newenvironment{isabelle}
15.49 -{\begin{trivlist}\begin{isabellebody}\item\relax}
15.50 -{\end{isabellebody}\end{trivlist}}
15.51 -
15.52 -\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
15.53 -
15.54 -\newcommand{\isaindent}[1]{\hphantom{#1}}
15.55 -\newcommand{\isanewline}{\mbox{}\par\mbox{}}
15.56 -\newcommand{\isasep}{}
15.57 -\newcommand{\isadigit}[1]{#1}
15.58 -
15.59 -\newcommand{\isachardefaults}{%
15.60 -\chardef\isacharbang=`\!%
15.61 -\chardef\isachardoublequote=`\"%
15.62 -\chardef\isachardoublequoteopen=`\"%
15.63 -\chardef\isachardoublequoteclose=`\"%
15.64 -\chardef\isacharhash=`\#%
15.65 -\chardef\isachardollar=`\$%
15.66 -\chardef\isacharpercent=`\%%
15.67 -\chardef\isacharampersand=`\&%
15.68 -\chardef\isacharprime=`\'%
15.69 -\chardef\isacharparenleft=`\(%
15.70 -\chardef\isacharparenright=`\)%
15.71 -\chardef\isacharasterisk=`\*%
15.72 -\chardef\isacharplus=`\+%
15.73 -\chardef\isacharcomma=`\,%
15.74 -\chardef\isacharminus=`\-%
15.75 -\chardef\isachardot=`\.%
15.76 -\chardef\isacharslash=`\/%
15.77 -\chardef\isacharcolon=`\:%
15.78 -\chardef\isacharsemicolon=`\;%
15.79 -\chardef\isacharless=`\<%
15.80 -\chardef\isacharequal=`\=%
15.81 -\chardef\isachargreater=`\>%
15.82 -\chardef\isacharquery=`\?%
15.83 -\chardef\isacharat=`\@%
15.84 -\chardef\isacharbrackleft=`\[%
15.85 -\chardef\isacharbackslash=`\\%
15.86 -\chardef\isacharbrackright=`\]%
15.87 -\chardef\isacharcircum=`\^%
15.88 -\chardef\isacharunderscore=`\_%
15.89 -\def\isacharunderscorekeyword{\_}%
15.90 -\chardef\isacharbackquote=`\`%
15.91 -\chardef\isacharbackquoteopen=`\`%
15.92 -\chardef\isacharbackquoteclose=`\`%
15.93 -\chardef\isacharbraceleft=`\{%
15.94 -\chardef\isacharbar=`\|%
15.95 -\chardef\isacharbraceright=`\}%
15.96 -\chardef\isachartilde=`\~%
15.97 -\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
15.98 -\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
15.99 -}
15.100 -
15.101 -
15.102 -% keyword and section markup
15.103 -
15.104 -\newcommand{\isakeyword}[1]
15.105 -{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
15.106 -\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
15.107 -\newcommand{\isacommand}[1]{\isakeyword{#1}}
15.108 -
15.109 -\newcommand{\isamarkupheader}[1]{\section{#1}}
15.110 -\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
15.111 -\newcommand{\isamarkupsection}[1]{\section{#1}}
15.112 -\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
15.113 -\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
15.114 -\newcommand{\isamarkupsect}[1]{\section{#1}}
15.115 -\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
15.116 -\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
15.117 -
15.118 -\newif\ifisamarkup
15.119 -\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
15.120 -\newcommand{\isaendpar}{\par\medskip}
15.121 -\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
15.122 -\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
15.123 -\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
15.124 -\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
15.125 -
15.126 -
15.127 -% styles
15.128 -
15.129 -\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
15.130 -
15.131 -\newcommand{\isabellestyledefault}{%
15.132 -\renewcommand{\isastyle}{\small\tt\slshape}%
15.133 -\renewcommand{\isastyleminor}{\small\tt\slshape}%
15.134 -\renewcommand{\isastylescript}{\footnotesize\tt\slshape}%
15.135 -\isachardefaults%
15.136 -}
15.137 -\isabellestyledefault
15.138 -
15.139 -\newcommand{\isabellestylett}{%
15.140 -\renewcommand{\isastyle}{\small\tt}%
15.141 -\renewcommand{\isastyleminor}{\small\tt}%
15.142 -\renewcommand{\isastylescript}{\footnotesize\tt}%
15.143 -\isachardefaults%
15.144 -}
15.145 -
15.146 -\newcommand{\isabellestyleit}{%
15.147 -\renewcommand{\isastyle}{\small\it}%
15.148 -\renewcommand{\isastyleminor}{\it}%
15.149 -\renewcommand{\isastylescript}{\footnotesize\it}%
15.150 -\renewcommand{\isacharunderscorekeyword}{\mbox{-}}%
15.151 -\renewcommand{\isacharbang}{\isamath{!}}%
15.152 -\renewcommand{\isachardoublequote}{}%
15.153 -\renewcommand{\isachardoublequoteopen}{}%
15.154 -\renewcommand{\isachardoublequoteclose}{}%
15.155 -\renewcommand{\isacharhash}{\isamath{\#}}%
15.156 -\renewcommand{\isachardollar}{\isamath{\$}}%
15.157 -\renewcommand{\isacharpercent}{\isamath{\%}}%
15.158 -\renewcommand{\isacharampersand}{\isamath{\&}}%
15.159 -\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
15.160 -\renewcommand{\isacharparenleft}{\isamath{(}}%
15.161 -\renewcommand{\isacharparenright}{\isamath{)}}%
15.162 -\renewcommand{\isacharasterisk}{\isamath{*}}%
15.163 -\renewcommand{\isacharplus}{\isamath{+}}%
15.164 -\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
15.165 -\renewcommand{\isacharminus}{\isamath{-}}%
15.166 -\renewcommand{\isachardot}{\isamath{\mathord.}}%
15.167 -\renewcommand{\isacharslash}{\isamath{/}}%
15.168 -\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
15.169 -\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
15.170 -\renewcommand{\isacharless}{\isamath{<}}%
15.171 -\renewcommand{\isacharequal}{\isamath{=}}%
15.172 -\renewcommand{\isachargreater}{\isamath{>}}%
15.173 -\renewcommand{\isacharat}{\isamath{@}}%
15.174 -\renewcommand{\isacharbrackleft}{\isamath{[}}%
15.175 -\renewcommand{\isacharbackslash}{\isamath{\backslash}}%
15.176 -\renewcommand{\isacharbrackright}{\isamath{]}}%
15.177 -\renewcommand{\isacharunderscore}{\mbox{-}}%
15.178 -\renewcommand{\isacharbraceleft}{\isamath{\{}}%
15.179 -\renewcommand{\isacharbar}{\isamath{\mid}}%
15.180 -\renewcommand{\isacharbraceright}{\isamath{\}}}%
15.181 -\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
15.182 -\renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
15.183 -\renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
15.184 -\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}%
15.185 -\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}%
15.186 -}
15.187 -
15.188 -\newcommand{\isabellestylesl}{%
15.189 -\isabellestyleit%
15.190 -\renewcommand{\isastyle}{\small\sl}%
15.191 -\renewcommand{\isastyleminor}{\sl}%
15.192 -\renewcommand{\isastylescript}{\footnotesize\sl}%
15.193 -}
15.194 -
15.195 -
15.196 -% tagged regions
15.197 -
15.198 -%plain TeX version of comment package -- much faster!
15.199 -\let\isafmtname\fmtname\def\fmtname{plain}
15.200 -\usepackage{comment}
15.201 -\let\fmtname\isafmtname
15.202 -
15.203 -\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
15.204 -
15.205 -\newcommand{\isakeeptag}[1]%
15.206 -{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
15.207 -\newcommand{\isadroptag}[1]%
15.208 -{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
15.209 -\newcommand{\isafoldtag}[1]%
15.210 -{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
15.211 -
15.212 -\isakeeptag{theory}
15.213 -\isakeeptag{proof}
15.214 -\isakeeptag{ML}
15.215 -\isakeeptag{visible}
15.216 -\isadroptag{invisible}
15.217 -
15.218 -\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}
16.1 --- a/doc-src/ZF/isabellesym.sty Thu May 15 20:02:44 2008 +0200
16.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
16.3 @@ -1,360 +0,0 @@
16.4 -%%
16.5 -%%
16.6 -%%
16.7 -%% definitions of standard Isabelle symbols
16.8 -%%
16.9 -
16.10 -\newcommand{\isasymzero}{\isamath{\mathbf{0}}} %requires amssymb
16.11 -\newcommand{\isasymone}{\isamath{\mathbf{1}}} %requires amssymb
16.12 -\newcommand{\isasymtwo}{\isamath{\mathbf{2}}} %requires amssymb
16.13 -\newcommand{\isasymthree}{\isamath{\mathbf{3}}} %requires amssymb
16.14 -\newcommand{\isasymfour}{\isamath{\mathbf{4}}} %requires amssymb
16.15 -\newcommand{\isasymfive}{\isamath{\mathbf{5}}} %requires amssymb
16.16 -\newcommand{\isasymsix}{\isamath{\mathbf{6}}} %requires amssymb
16.17 -\newcommand{\isasymseven}{\isamath{\mathbf{7}}} %requires amssymb
16.18 -\newcommand{\isasymeight}{\isamath{\mathbf{8}}} %requires amssymb
16.19 -\newcommand{\isasymnine}{\isamath{\mathbf{9}}} %requires amssymb
16.20 -\newcommand{\isasymA}{\isamath{\mathcal{A}}}
16.21 -\newcommand{\isasymB}{\isamath{\mathcal{B}}}
16.22 -\newcommand{\isasymC}{\isamath{\mathcal{C}}}
16.23 -\newcommand{\isasymD}{\isamath{\mathcal{D}}}
16.24 -\newcommand{\isasymE}{\isamath{\mathcal{E}}}
16.25 -\newcommand{\isasymF}{\isamath{\mathcal{F}}}
16.26 -\newcommand{\isasymG}{\isamath{\mathcal{G}}}
16.27 -\newcommand{\isasymH}{\isamath{\mathcal{H}}}
16.28 -\newcommand{\isasymI}{\isamath{\mathcal{I}}}
16.29 -\newcommand{\isasymJ}{\isamath{\mathcal{J}}}
16.30 -\newcommand{\isasymK}{\isamath{\mathcal{K}}}
16.31 -\newcommand{\isasymL}{\isamath{\mathcal{L}}}
16.32 -\newcommand{\isasymM}{\isamath{\mathcal{M}}}
16.33 -\newcommand{\isasymN}{\isamath{\mathcal{N}}}
16.34 -\newcommand{\isasymO}{\isamath{\mathcal{O}}}
16.35 -\newcommand{\isasymP}{\isamath{\mathcal{P}}}
16.36 -\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}
16.37 -\newcommand{\isasymR}{\isamath{\mathcal{R}}}
16.38 -\newcommand{\isasymS}{\isamath{\mathcal{S}}}
16.39 -\newcommand{\isasymT}{\isamath{\mathcal{T}}}
16.40 -\newcommand{\isasymU}{\isamath{\mathcal{U}}}
16.41 -\newcommand{\isasymV}{\isamath{\mathcal{V}}}
16.42 -\newcommand{\isasymW}{\isamath{\mathcal{W}}}
16.43 -\newcommand{\isasymX}{\isamath{\mathcal{X}}}
16.44 -\newcommand{\isasymY}{\isamath{\mathcal{Y}}}
16.45 -\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
16.46 -\newcommand{\isasyma}{\isamath{\mathrm{a}}}
16.47 -\newcommand{\isasymb}{\isamath{\mathrm{b}}}
16.48 -\newcommand{\isasymc}{\isamath{\mathrm{c}}}
16.49 -\newcommand{\isasymd}{\isamath{\mathrm{d}}}
16.50 -\newcommand{\isasyme}{\isamath{\mathrm{e}}}
16.51 -\newcommand{\isasymf}{\isamath{\mathrm{f}}}
16.52 -\newcommand{\isasymg}{\isamath{\mathrm{g}}}
16.53 -\newcommand{\isasymh}{\isamath{\mathrm{h}}}
16.54 -\newcommand{\isasymi}{\isamath{\mathrm{i}}}
16.55 -\newcommand{\isasymj}{\isamath{\mathrm{j}}}
16.56 -\newcommand{\isasymk}{\isamath{\mathrm{k}}}
16.57 -\newcommand{\isasyml}{\isamath{\mathrm{l}}}
16.58 -\newcommand{\isasymm}{\isamath{\mathrm{m}}}
16.59 -\newcommand{\isasymn}{\isamath{\mathrm{n}}}
16.60 -\newcommand{\isasymo}{\isamath{\mathrm{o}}}
16.61 -\newcommand{\isasymp}{\isamath{\mathrm{p}}}
16.62 -\newcommand{\isasymq}{\isamath{\mathrm{q}}}
16.63 -\newcommand{\isasymr}{\isamath{\mathrm{r}}}
16.64 -\newcommand{\isasyms}{\isamath{\mathrm{s}}}
16.65 -\newcommand{\isasymt}{\isamath{\mathrm{t}}}
16.66 -\newcommand{\isasymu}{\isamath{\mathrm{u}}}
16.67 -\newcommand{\isasymv}{\isamath{\mathrm{v}}}
16.68 -\newcommand{\isasymw}{\isamath{\mathrm{w}}}
16.69 -\newcommand{\isasymx}{\isamath{\mathrm{x}}}
16.70 -\newcommand{\isasymy}{\isamath{\mathrm{y}}}
16.71 -\newcommand{\isasymz}{\isamath{\mathrm{z}}}
16.72 -\newcommand{\isasymAA}{\isamath{\mathfrak{A}}} %requires eufrak
16.73 -\newcommand{\isasymBB}{\isamath{\mathfrak{B}}} %requires eufrak
16.74 -\newcommand{\isasymCC}{\isamath{\mathfrak{C}}} %requires eufrak
16.75 -\newcommand{\isasymDD}{\isamath{\mathfrak{D}}} %requires eufrak
16.76 -\newcommand{\isasymEE}{\isamath{\mathfrak{E}}} %requires eufrak
16.77 -\newcommand{\isasymFF}{\isamath{\mathfrak{F}}} %requires eufrak
16.78 -\newcommand{\isasymGG}{\isamath{\mathfrak{G}}} %requires eufrak
16.79 -\newcommand{\isasymHH}{\isamath{\mathfrak{H}}} %requires eufrak
16.80 -\newcommand{\isasymII}{\isamath{\mathfrak{I}}} %requires eufrak
16.81 -\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}} %requires eufrak
16.82 -\newcommand{\isasymKK}{\isamath{\mathfrak{K}}} %requires eufrak
16.83 -\newcommand{\isasymLL}{\isamath{\mathfrak{L}}} %requires eufrak
16.84 -\newcommand{\isasymMM}{\isamath{\mathfrak{M}}} %requires eufrak
16.85 -\newcommand{\isasymNN}{\isamath{\mathfrak{N}}} %requires eufrak
16.86 -\newcommand{\isasymOO}{\isamath{\mathfrak{O}}} %requires eufrak
16.87 -\newcommand{\isasymPP}{\isamath{\mathfrak{P}}} %requires eufrak
16.88 -\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}} %requires eufrak
16.89 -\newcommand{\isasymRR}{\isamath{\mathfrak{R}}} %requires eufrak
16.90 -\newcommand{\isasymSS}{\isamath{\mathfrak{S}}} %requires eufrak
16.91 -\newcommand{\isasymTT}{\isamath{\mathfrak{T}}} %requires eufrak
16.92 -\newcommand{\isasymUU}{\isamath{\mathfrak{U}}} %requires eufrak
16.93 -\newcommand{\isasymVV}{\isamath{\mathfrak{V}}} %requires eufrak
16.94 -\newcommand{\isasymWW}{\isamath{\mathfrak{W}}} %requires eufrak
16.95 -\newcommand{\isasymXX}{\isamath{\mathfrak{X}}} %requires eufrak
16.96 -\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}} %requires eufrak
16.97 -\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}} %requires eufrak
16.98 -\newcommand{\isasymaa}{\isamath{\mathfrak{a}}} %requires eufrak
16.99 -\newcommand{\isasymbb}{\isamath{\mathfrak{b}}} %requires eufrak
16.100 -\newcommand{\isasymcc}{\isamath{\mathfrak{c}}} %requires eufrak
16.101 -\newcommand{\isasymdd}{\isamath{\mathfrak{d}}} %requires eufrak
16.102 -\newcommand{\isasymee}{\isamath{\mathfrak{e}}} %requires eufrak
16.103 -\newcommand{\isasymff}{\isamath{\mathfrak{f}}} %requires eufrak
16.104 -\newcommand{\isasymgg}{\isamath{\mathfrak{g}}} %requires eufrak
16.105 -\newcommand{\isasymhh}{\isamath{\mathfrak{h}}} %requires eufrak
16.106 -\newcommand{\isasymii}{\isamath{\mathfrak{i}}} %requires eufrak
16.107 -\newcommand{\isasymjj}{\isamath{\mathfrak{j}}} %requires eufrak
16.108 -\newcommand{\isasymkk}{\isamath{\mathfrak{k}}} %requires eufrak
16.109 -\newcommand{\isasymll}{\isamath{\mathfrak{l}}} %requires eufrak
16.110 -\newcommand{\isasymmm}{\isamath{\mathfrak{m}}} %requires eufrak
16.111 -\newcommand{\isasymnn}{\isamath{\mathfrak{n}}} %requires eufrak
16.112 -\newcommand{\isasymoo}{\isamath{\mathfrak{o}}} %requires eufrak
16.113 -\newcommand{\isasympp}{\isamath{\mathfrak{p}}} %requires eufrak
16.114 -\newcommand{\isasymqq}{\isamath{\mathfrak{q}}} %requires eufrak
16.115 -\newcommand{\isasymrr}{\isamath{\mathfrak{r}}} %requires eufrak
16.116 -\newcommand{\isasymss}{\isamath{\mathfrak{s}}} %requires eufrak
16.117 -\newcommand{\isasymtt}{\isamath{\mathfrak{t}}} %requires eufrak
16.118 -\newcommand{\isasymuu}{\isamath{\mathfrak{u}}} %requires eufrak
16.119 -\newcommand{\isasymvv}{\isamath{\mathfrak{v}}} %requires eufrak
16.120 -\newcommand{\isasymww}{\isamath{\mathfrak{w}}} %requires eufrak
16.121 -\newcommand{\isasymxx}{\isamath{\mathfrak{x}}} %requires eufrak
16.122 -\newcommand{\isasymyy}{\isamath{\mathfrak{y}}} %requires eufrak
16.123 -\newcommand{\isasymzz}{\isamath{\mathfrak{z}}} %requires eufrak
16.124 -\newcommand{\isasymalpha}{\isamath{\alpha}}
16.125 -\newcommand{\isasymbeta}{\isamath{\beta}}
16.126 -\newcommand{\isasymgamma}{\isamath{\gamma}}
16.127 -\newcommand{\isasymdelta}{\isamath{\delta}}
16.128 -\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
16.129 -\newcommand{\isasymzeta}{\isamath{\zeta}}
16.130 -\newcommand{\isasymeta}{\isamath{\eta}}
16.131 -\newcommand{\isasymtheta}{\isamath{\vartheta}}
16.132 -\newcommand{\isasymiota}{\isamath{\iota}}
16.133 -\newcommand{\isasymkappa}{\isamath{\kappa}}
16.134 -\newcommand{\isasymlambda}{\isamath{\lambda}}
16.135 -\newcommand{\isasymmu}{\isamath{\mu}}
16.136 -\newcommand{\isasymnu}{\isamath{\nu}}
16.137 -\newcommand{\isasymxi}{\isamath{\xi}}
16.138 -\newcommand{\isasympi}{\isamath{\pi}}
16.139 -\newcommand{\isasymrho}{\isamath{\varrho}}
16.140 -\newcommand{\isasymsigma}{\isamath{\sigma}}
16.141 -\newcommand{\isasymtau}{\isamath{\tau}}
16.142 -\newcommand{\isasymupsilon}{\isamath{\upsilon}}
16.143 -\newcommand{\isasymphi}{\isamath{\varphi}}
16.144 -\newcommand{\isasymchi}{\isamath{\chi}}
16.145 -\newcommand{\isasympsi}{\isamath{\psi}}
16.146 -\newcommand{\isasymomega}{\isamath{\omega}}
16.147 -\newcommand{\isasymGamma}{\isamath{\Gamma}}
16.148 -\newcommand{\isasymDelta}{\isamath{\Delta}}
16.149 -\newcommand{\isasymTheta}{\isamath{\Theta}}
16.150 -\newcommand{\isasymLambda}{\isamath{\Lambda}}
16.151 -\newcommand{\isasymXi}{\isamath{\Xi}}
16.152 -\newcommand{\isasymPi}{\isamath{\Pi}}
16.153 -\newcommand{\isasymSigma}{\isamath{\Sigma}}
16.154 -\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
16.155 -\newcommand{\isasymPhi}{\isamath{\Phi}}
16.156 -\newcommand{\isasymPsi}{\isamath{\Psi}}
16.157 -\newcommand{\isasymOmega}{\isamath{\Omega}}
16.158 -\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
16.159 -\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
16.160 -\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
16.161 -\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
16.162 -\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
16.163 -\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
16.164 -\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
16.165 -\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
16.166 -\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
16.167 -\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
16.168 -\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
16.169 -\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
16.170 -\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
16.171 -\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
16.172 -\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
16.173 -\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
16.174 -\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
16.175 -\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
16.176 -\newcommand{\isasymmapsto}{\isamath{\mapsto}}
16.177 -\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
16.178 -\newcommand{\isasymmidarrow}{\isamath{\relbar}}
16.179 -\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
16.180 -\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
16.181 -\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
16.182 -\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
16.183 -\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
16.184 -\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
16.185 -\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
16.186 -\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
16.187 -\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
16.188 -\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}} %requires amssymb
16.189 -\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}} %requires amssymb
16.190 -\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}} %requires amssymb
16.191 -\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}} %requires amssymb
16.192 -\newcommand{\isasymrestriction}{\isamath{\restriction}} %requires amssymb
16.193 -\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
16.194 -\newcommand{\isasymup}{\isamath{\uparrow}}
16.195 -\newcommand{\isasymUp}{\isamath{\Uparrow}}
16.196 -\newcommand{\isasymdown}{\isamath{\downarrow}}
16.197 -\newcommand{\isasymDown}{\isamath{\Downarrow}}
16.198 -\newcommand{\isasymupdown}{\isamath{\updownarrow}}
16.199 -\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
16.200 -\newcommand{\isasymlangle}{\isamath{\langle}}
16.201 -\newcommand{\isasymrangle}{\isamath{\rangle}}
16.202 -\newcommand{\isasymlceil}{\isamath{\lceil}}
16.203 -\newcommand{\isasymrceil}{\isamath{\rceil}}
16.204 -\newcommand{\isasymlfloor}{\isamath{\lfloor}}
16.205 -\newcommand{\isasymrfloor}{\isamath{\rfloor}}
16.206 -\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
16.207 -\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}
16.208 -\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
16.209 -\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
16.210 -\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
16.211 -\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
16.212 -\newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel
16.213 -\newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel
16.214 -\newcommand{\isasymbottom}{\isamath{\bot}}
16.215 -\newcommand{\isasymtop}{\isamath{\top}}
16.216 -\newcommand{\isasymand}{\isamath{\wedge}}
16.217 -\newcommand{\isasymAnd}{\isamath{\bigwedge}}
16.218 -\newcommand{\isasymor}{\isamath{\vee}}
16.219 -\newcommand{\isasymOr}{\isamath{\bigvee}}
16.220 -\newcommand{\isasymforall}{\isamath{\forall\,}}
16.221 -\newcommand{\isasymexists}{\isamath{\exists\,}}
16.222 -\newcommand{\isasymnexists}{\isamath{\nexists\,}} %requires amssymb
16.223 -\newcommand{\isasymnot}{\isamath{\neg}}
16.224 -\newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb
16.225 -\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb
16.226 -\newcommand{\isasymturnstile}{\isamath{\vdash}}
16.227 -\newcommand{\isasymTurnstile}{\isamath{\models}}
16.228 -\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
16.229 -\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
16.230 -\newcommand{\isasymstileturn}{\isamath{\dashv}}
16.231 -\newcommand{\isasymsurd}{\isamath{\surd}}
16.232 -\newcommand{\isasymle}{\isamath{\le}}
16.233 -\newcommand{\isasymge}{\isamath{\ge}}
16.234 -\newcommand{\isasymlless}{\isamath{\ll}}
16.235 -\newcommand{\isasymggreater}{\isamath{\gg}}
16.236 -\newcommand{\isasymlesssim}{\isamath{\lesssim}} %requires amssymb
16.237 -\newcommand{\isasymgreatersim}{\isamath{\gtrsim}} %requires amssymb
16.238 -\newcommand{\isasymlessapprox}{\isamath{\lessapprox}} %requires amssymb
16.239 -\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}} %requires amssymb
16.240 -\newcommand{\isasymin}{\isamath{\in}}
16.241 -\newcommand{\isasymnotin}{\isamath{\notin}}
16.242 -\newcommand{\isasymsubset}{\isamath{\subset}}
16.243 -\newcommand{\isasymsupset}{\isamath{\supset}}
16.244 -\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
16.245 -\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
16.246 -\newcommand{\isasymsqsubset}{\isamath{\sqsubset}} %requires amssymb
16.247 -\newcommand{\isasymsqsupset}{\isamath{\sqsupset}} %requires amssymb
16.248 -\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
16.249 -\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
16.250 -\newcommand{\isasyminter}{\isamath{\cap}}
16.251 -\newcommand{\isasymInter}{\isamath{\bigcap\,}}
16.252 -\newcommand{\isasymunion}{\isamath{\cup}}
16.253 -\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
16.254 -\newcommand{\isasymsqunion}{\isamath{\sqcup}}
16.255 -\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
16.256 -\newcommand{\isasymsqinter}{\isamath{\sqcap}}
16.257 -\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires amsmath
16.258 -\newcommand{\isasymsetminus}{\isamath{\setminus}}
16.259 -\newcommand{\isasympropto}{\isamath{\propto}}
16.260 -\newcommand{\isasymuplus}{\isamath{\uplus}}
16.261 -\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
16.262 -\newcommand{\isasymnoteq}{\isamath{\not=}}
16.263 -\newcommand{\isasymsim}{\isamath{\sim}}
16.264 -\newcommand{\isasymdoteq}{\isamath{\doteq}}
16.265 -\newcommand{\isasymsimeq}{\isamath{\simeq}}
16.266 -\newcommand{\isasymapprox}{\isamath{\approx}}
16.267 -\newcommand{\isasymasymp}{\isamath{\asymp}}
16.268 -\newcommand{\isasymcong}{\isamath{\cong}}
16.269 -\newcommand{\isasymsmile}{\isamath{\smile}}
16.270 -\newcommand{\isasymequiv}{\isamath{\equiv}}
16.271 -\newcommand{\isasymfrown}{\isamath{\frown}}
16.272 -\newcommand{\isasymJoin}{\isamath{\Join}} %requires amssymb
16.273 -\newcommand{\isasymbowtie}{\isamath{\bowtie}}
16.274 -\newcommand{\isasymprec}{\isamath{\prec}}
16.275 -\newcommand{\isasymsucc}{\isamath{\succ}}
16.276 -\newcommand{\isasympreceq}{\isamath{\preceq}}
16.277 -\newcommand{\isasymsucceq}{\isamath{\succeq}}
16.278 -\newcommand{\isasymparallel}{\isamath{\parallel}}
16.279 -\newcommand{\isasymbar}{\isamath{\mid}}
16.280 -\newcommand{\isasymplusminus}{\isamath{\pm}}
16.281 -\newcommand{\isasymminusplus}{\isamath{\mp}}
16.282 -\newcommand{\isasymtimes}{\isamath{\times}}
16.283 -\newcommand{\isasymdiv}{\isamath{\div}}
16.284 -\newcommand{\isasymcdot}{\isamath{\cdot}}
16.285 -\newcommand{\isasymstar}{\isamath{\star}}
16.286 -\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
16.287 -\newcommand{\isasymcirc}{\isamath{\circ}}
16.288 -\newcommand{\isasymdagger}{\isamath{\dagger}}
16.289 -\newcommand{\isasymddagger}{\isamath{\ddagger}}
16.290 -\newcommand{\isasymlhd}{\isamath{\lhd}} %requires amssymb
16.291 -\newcommand{\isasymrhd}{\isamath{\rhd}} %requires amssymb
16.292 -\newcommand{\isasymunlhd}{\isamath{\unlhd}} %requires amssymb
16.293 -\newcommand{\isasymunrhd}{\isamath{\unrhd}} %requires amssymb
16.294 -\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
16.295 -\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
16.296 -\newcommand{\isasymtriangle}{\isamath{\triangle}}
16.297 -\newcommand{\isasymtriangleq}{\isamath{\triangleq}} %requires amssymb
16.298 -\newcommand{\isasymoplus}{\isamath{\oplus}}
16.299 -\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}
16.300 -\newcommand{\isasymotimes}{\isamath{\otimes}}
16.301 -\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}
16.302 -\newcommand{\isasymodot}{\isamath{\odot}}
16.303 -\newcommand{\isasymOdot}{\isamath{\bigodot\,}}
16.304 -\newcommand{\isasymominus}{\isamath{\ominus}}
16.305 -\newcommand{\isasymoslash}{\isamath{\oslash}}
16.306 -\newcommand{\isasymdots}{\isamath{\dots}}
16.307 -\newcommand{\isasymcdots}{\isamath{\cdots}}
16.308 -\newcommand{\isasymSum}{\isamath{\sum\,}}
16.309 -\newcommand{\isasymProd}{\isamath{\prod\,}}
16.310 -\newcommand{\isasymCoprod}{\isamath{\coprod\,}}
16.311 -\newcommand{\isasyminfinity}{\isamath{\infty}}
16.312 -\newcommand{\isasymintegral}{\isamath{\int\,}}
16.313 -\newcommand{\isasymointegral}{\isamath{\oint\,}}
16.314 -\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
16.315 -\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
16.316 -\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
16.317 -\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
16.318 -\newcommand{\isasymaleph}{\isamath{\aleph}}
16.319 -\newcommand{\isasymemptyset}{\isamath{\emptyset}}
16.320 -\newcommand{\isasymnabla}{\isamath{\nabla}}
16.321 -\newcommand{\isasympartial}{\isamath{\partial}}
16.322 -\newcommand{\isasymRe}{\isamath{\Re}}
16.323 -\newcommand{\isasymIm}{\isamath{\Im}}
16.324 -\newcommand{\isasymflat}{\isamath{\flat}}
16.325 -\newcommand{\isasymnatural}{\isamath{\natural}}
16.326 -\newcommand{\isasymsharp}{\isamath{\sharp}}
16.327 -\newcommand{\isasymangle}{\isamath{\angle}}
16.328 -\newcommand{\isasymcopyright}{\isatext{\rm\copyright}}
16.329 -\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
16.330 -\newcommand{\isasymhyphen}{\isatext{\rm-}}
16.331 -\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
16.332 -\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}} %requires latin1
16.333 -\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}} %requires latin1
16.334 -\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}} %requires latin1
16.335 -\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}} %requires latin1
16.336 -\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}} %requires latin1
16.337 -\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}} %requires latin1
16.338 -\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
16.339 -\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
16.340 -\newcommand{\isasymsection}{\isatext{\rm\S}}
16.341 -\newcommand{\isasymparagraph}{\isatext{\rm\P}}
16.342 -\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
16.343 -\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
16.344 -\newcommand{\isasymeuro}{\isatext{\textgreek{\euro}}} %requires greek babel
16.345 -\newcommand{\isasympounds}{\isamath{\pounds}}
16.346 -\newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb
16.347 -\newcommand{\isasymcent}{\isatext{\textcent}} %requires textcomp
16.348 -\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
16.349 -\newcommand{\isasymdegree}{\isatext{\rm\textdegree}} %requires latin1
16.350 -\newcommand{\isasymamalg}{\isamath{\amalg}}
16.351 -\newcommand{\isasymmho}{\isamath{\mho}} %requires amssymb
16.352 -\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssymb
16.353 -\newcommand{\isasymwp}{\isamath{\wp}}
16.354 -\newcommand{\isasymwrong}{\isamath{\wr}}
16.355 -\newcommand{\isasymstruct}{\isamath{\diamond}}
16.356 -\newcommand{\isasymacute}{\isatext{\'\relax}}
16.357 -\newcommand{\isasymindex}{\isatext{\i}}
16.358 -\newcommand{\isasymdieresis}{\isatext{\"\relax}}
16.359 -\newcommand{\isasymcedilla}{\isatext{\c\relax}}
16.360 -\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
16.361 -\newcommand{\isasymspacespace}{\isamath{~~}}
16.362 -\newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}
16.363 -\newcommand{\isasymsome}{\isamath{\epsilon\,}}
17.1 --- a/doc-src/ZF/logics-ZF.tex Thu May 15 20:02:44 2008 +0200
17.2 +++ b/doc-src/ZF/logics-ZF.tex Thu May 15 20:14:10 2008 +0200
17.3 @@ -1,6 +1,6 @@
17.4 %% $Id$
17.5 \documentclass[11pt,a4paper]{report}
17.6 -\usepackage{isabelle,isabellesym}
17.7 +\usepackage{../isabelle,../isabellesym}
17.8 \usepackage{graphicx,logics,../ttbox,../proof,../rail,latexsym}
17.9
17.10 \usepackage{../pdfsetup}
18.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
18.2 +++ b/doc-src/isabelle.sty Thu May 15 20:14:10 2008 +0200
18.3 @@ -0,0 +1,215 @@
18.4 +%%
18.5 +%%
18.6 +%%
18.7 +%% macros for Isabelle generated LaTeX output
18.8 +%%
18.9 +
18.10 +%%% Simple document preparation (based on theory token language and symbols)
18.11 +
18.12 +% isabelle environments
18.13 +
18.14 +\newcommand{\isabellecontext}{UNKNOWN}
18.15 +
18.16 +\newcommand{\isastyle}{\UNDEF}
18.17 +\newcommand{\isastyleminor}{\UNDEF}
18.18 +\newcommand{\isastylescript}{\UNDEF}
18.19 +\newcommand{\isastyletext}{\normalsize\rm}
18.20 +\newcommand{\isastyletxt}{\rm}
18.21 +\newcommand{\isastylecmt}{\rm}
18.22 +
18.23 +%symbol markup -- \emph achieves decent spacing via italic corrections
18.24 +\newcommand{\isamath}[1]{\emph{$#1$}}
18.25 +\newcommand{\isatext}[1]{\emph{#1}}
18.26 +\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
18.27 +\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
18.28 +\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
18.29 +\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
18.30 +\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
18.31 +\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isastylescript}
18.32 +\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
18.33 +\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isastylescript}
18.34 +\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
18.35 +\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
18.36 +\newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
18.37 +\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
18.38 +
18.39 +
18.40 +\newdimen\isa@parindent\newdimen\isa@parskip
18.41 +
18.42 +\newenvironment{isabellebody}{%
18.43 +\isamarkuptrue\par%
18.44 +\isa@parindent\parindent\parindent0pt%
18.45 +\isa@parskip\parskip\parskip0pt%
18.46 +\isastyle}{\par}
18.47 +
18.48 +\newenvironment{isabelle}
18.49 +{\begin{trivlist}\begin{isabellebody}\item\relax}
18.50 +{\end{isabellebody}\end{trivlist}}
18.51 +
18.52 +\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
18.53 +
18.54 +\newcommand{\isaindent}[1]{\hphantom{#1}}
18.55 +\newcommand{\isanewline}{\mbox{}\par\mbox{}}
18.56 +\newcommand{\isasep}{}
18.57 +\newcommand{\isadigit}[1]{#1}
18.58 +
18.59 +\newcommand{\isachardefaults}{%
18.60 +\chardef\isacharbang=`\!%
18.61 +\chardef\isachardoublequote=`\"%
18.62 +\chardef\isachardoublequoteopen=`\"%
18.63 +\chardef\isachardoublequoteclose=`\"%
18.64 +\chardef\isacharhash=`\#%
18.65 +\chardef\isachardollar=`\$%
18.66 +\chardef\isacharpercent=`\%%
18.67 +\chardef\isacharampersand=`\&%
18.68 +\chardef\isacharprime=`\'%
18.69 +\chardef\isacharparenleft=`\(%
18.70 +\chardef\isacharparenright=`\)%
18.71 +\chardef\isacharasterisk=`\*%
18.72 +\chardef\isacharplus=`\+%
18.73 +\chardef\isacharcomma=`\,%
18.74 +\chardef\isacharminus=`\-%
18.75 +\chardef\isachardot=`\.%
18.76 +\chardef\isacharslash=`\/%
18.77 +\chardef\isacharcolon=`\:%
18.78 +\chardef\isacharsemicolon=`\;%
18.79 +\chardef\isacharless=`\<%
18.80 +\chardef\isacharequal=`\=%
18.81 +\chardef\isachargreater=`\>%
18.82 +\chardef\isacharquery=`\?%
18.83 +\chardef\isacharat=`\@%
18.84 +\chardef\isacharbrackleft=`\[%
18.85 +\chardef\isacharbackslash=`\\%
18.86 +\chardef\isacharbrackright=`\]%
18.87 +\chardef\isacharcircum=`\^%
18.88 +\chardef\isacharunderscore=`\_%
18.89 +\def\isacharunderscorekeyword{\_}%
18.90 +\chardef\isacharbackquote=`\`%
18.91 +\chardef\isacharbackquoteopen=`\`%
18.92 +\chardef\isacharbackquoteclose=`\`%
18.93 +\chardef\isacharbraceleft=`\{%
18.94 +\chardef\isacharbar=`\|%
18.95 +\chardef\isacharbraceright=`\}%
18.96 +\chardef\isachartilde=`\~%
18.97 +\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
18.98 +\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
18.99 +}
18.100 +
18.101 +
18.102 +% keyword and section markup
18.103 +
18.104 +\newcommand{\isakeyword}[1]
18.105 +{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
18.106 +\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
18.107 +\newcommand{\isacommand}[1]{\isakeyword{#1}}
18.108 +
18.109 +\newcommand{\isamarkupheader}[1]{\section{#1}}
18.110 +\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
18.111 +\newcommand{\isamarkupsection}[1]{\section{#1}}
18.112 +\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
18.113 +\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
18.114 +\newcommand{\isamarkupsect}[1]{\section{#1}}
18.115 +\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
18.116 +\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
18.117 +
18.118 +\newif\ifisamarkup
18.119 +\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
18.120 +\newcommand{\isaendpar}{\par\medskip}
18.121 +\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
18.122 +\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
18.123 +\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
18.124 +\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
18.125 +
18.126 +
18.127 +% styles
18.128 +
18.129 +\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
18.130 +
18.131 +\newcommand{\isabellestyledefault}{%
18.132 +\renewcommand{\isastyle}{\small\tt\slshape}%
18.133 +\renewcommand{\isastyleminor}{\small\tt\slshape}%
18.134 +\renewcommand{\isastylescript}{\footnotesize\tt\slshape}%
18.135 +\isachardefaults%
18.136 +}
18.137 +\isabellestyledefault
18.138 +
18.139 +\newcommand{\isabellestylett}{%
18.140 +\renewcommand{\isastyle}{\small\tt}%
18.141 +\renewcommand{\isastyleminor}{\small\tt}%
18.142 +\renewcommand{\isastylescript}{\footnotesize\tt}%
18.143 +\isachardefaults%
18.144 +}
18.145 +
18.146 +\newcommand{\isabellestyleit}{%
18.147 +\renewcommand{\isastyle}{\small\it}%
18.148 +\renewcommand{\isastyleminor}{\it}%
18.149 +\renewcommand{\isastylescript}{\footnotesize\it}%
18.150 +\renewcommand{\isacharunderscorekeyword}{\mbox{-}}%
18.151 +\renewcommand{\isacharbang}{\isamath{!}}%
18.152 +\renewcommand{\isachardoublequote}{}%
18.153 +\renewcommand{\isachardoublequoteopen}{}%
18.154 +\renewcommand{\isachardoublequoteclose}{}%
18.155 +\renewcommand{\isacharhash}{\isamath{\#}}%
18.156 +\renewcommand{\isachardollar}{\isamath{\$}}%
18.157 +\renewcommand{\isacharpercent}{\isamath{\%}}%
18.158 +\renewcommand{\isacharampersand}{\isamath{\&}}%
18.159 +\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
18.160 +\renewcommand{\isacharparenleft}{\isamath{(}}%
18.161 +\renewcommand{\isacharparenright}{\isamath{)}}%
18.162 +\renewcommand{\isacharasterisk}{\isamath{*}}%
18.163 +\renewcommand{\isacharplus}{\isamath{+}}%
18.164 +\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
18.165 +\renewcommand{\isacharminus}{\isamath{-}}%
18.166 +\renewcommand{\isachardot}{\isamath{\mathord.}}%
18.167 +\renewcommand{\isacharslash}{\isamath{/}}%
18.168 +\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
18.169 +\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
18.170 +\renewcommand{\isacharless}{\isamath{<}}%
18.171 +\renewcommand{\isacharequal}{\isamath{=}}%
18.172 +\renewcommand{\isachargreater}{\isamath{>}}%
18.173 +\renewcommand{\isacharat}{\isamath{@}}%
18.174 +\renewcommand{\isacharbrackleft}{\isamath{[}}%
18.175 +\renewcommand{\isacharbackslash}{\isamath{\backslash}}%
18.176 +\renewcommand{\isacharbrackright}{\isamath{]}}%
18.177 +\renewcommand{\isacharunderscore}{\mbox{-}}%
18.178 +\renewcommand{\isacharbraceleft}{\isamath{\{}}%
18.179 +\renewcommand{\isacharbar}{\isamath{\mid}}%
18.180 +\renewcommand{\isacharbraceright}{\isamath{\}}}%
18.181 +\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
18.182 +\renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
18.183 +\renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
18.184 +\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}%
18.185 +\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}%
18.186 +}
18.187 +
18.188 +\newcommand{\isabellestylesl}{%
18.189 +\isabellestyleit%
18.190 +\renewcommand{\isastyle}{\small\sl}%
18.191 +\renewcommand{\isastyleminor}{\sl}%
18.192 +\renewcommand{\isastylescript}{\footnotesize\sl}%
18.193 +}
18.194 +
18.195 +
18.196 +% tagged regions
18.197 +
18.198 +%plain TeX version of comment package -- much faster!
18.199 +\let\isafmtname\fmtname\def\fmtname{plain}
18.200 +\usepackage{comment}
18.201 +\let\fmtname\isafmtname
18.202 +
18.203 +\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
18.204 +
18.205 +\newcommand{\isakeeptag}[1]%
18.206 +{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
18.207 +\newcommand{\isadroptag}[1]%
18.208 +{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
18.209 +\newcommand{\isafoldtag}[1]%
18.210 +{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
18.211 +
18.212 +\isakeeptag{theory}
18.213 +\isakeeptag{proof}
18.214 +\isakeeptag{ML}
18.215 +\isakeeptag{visible}
18.216 +\isadroptag{invisible}
18.217 +
18.218 +\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}
19.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
19.2 +++ b/doc-src/isabellesym.sty Thu May 15 20:14:10 2008 +0200
19.3 @@ -0,0 +1,360 @@
19.4 +%%
19.5 +%%
19.6 +%%
19.7 +%% definitions of standard Isabelle symbols
19.8 +%%
19.9 +
19.10 +\newcommand{\isasymzero}{\isamath{\mathbf{0}}} %requires amssymb
19.11 +\newcommand{\isasymone}{\isamath{\mathbf{1}}} %requires amssymb
19.12 +\newcommand{\isasymtwo}{\isamath{\mathbf{2}}} %requires amssymb
19.13 +\newcommand{\isasymthree}{\isamath{\mathbf{3}}} %requires amssymb
19.14 +\newcommand{\isasymfour}{\isamath{\mathbf{4}}} %requires amssymb
19.15 +\newcommand{\isasymfive}{\isamath{\mathbf{5}}} %requires amssymb
19.16 +\newcommand{\isasymsix}{\isamath{\mathbf{6}}} %requires amssymb
19.17 +\newcommand{\isasymseven}{\isamath{\mathbf{7}}} %requires amssymb
19.18 +\newcommand{\isasymeight}{\isamath{\mathbf{8}}} %requires amssymb
19.19 +\newcommand{\isasymnine}{\isamath{\mathbf{9}}} %requires amssymb
19.20 +\newcommand{\isasymA}{\isamath{\mathcal{A}}}
19.21 +\newcommand{\isasymB}{\isamath{\mathcal{B}}}
19.22 +\newcommand{\isasymC}{\isamath{\mathcal{C}}}
19.23 +\newcommand{\isasymD}{\isamath{\mathcal{D}}}
19.24 +\newcommand{\isasymE}{\isamath{\mathcal{E}}}
19.25 +\newcommand{\isasymF}{\isamath{\mathcal{F}}}
19.26 +\newcommand{\isasymG}{\isamath{\mathcal{G}}}
19.27 +\newcommand{\isasymH}{\isamath{\mathcal{H}}}
19.28 +\newcommand{\isasymI}{\isamath{\mathcal{I}}}
19.29 +\newcommand{\isasymJ}{\isamath{\mathcal{J}}}
19.30 +\newcommand{\isasymK}{\isamath{\mathcal{K}}}
19.31 +\newcommand{\isasymL}{\isamath{\mathcal{L}}}
19.32 +\newcommand{\isasymM}{\isamath{\mathcal{M}}}
19.33 +\newcommand{\isasymN}{\isamath{\mathcal{N}}}
19.34 +\newcommand{\isasymO}{\isamath{\mathcal{O}}}
19.35 +\newcommand{\isasymP}{\isamath{\mathcal{P}}}
19.36 +\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}
19.37 +\newcommand{\isasymR}{\isamath{\mathcal{R}}}
19.38 +\newcommand{\isasymS}{\isamath{\mathcal{S}}}
19.39 +\newcommand{\isasymT}{\isamath{\mathcal{T}}}
19.40 +\newcommand{\isasymU}{\isamath{\mathcal{U}}}
19.41 +\newcommand{\isasymV}{\isamath{\mathcal{V}}}
19.42 +\newcommand{\isasymW}{\isamath{\mathcal{W}}}
19.43 +\newcommand{\isasymX}{\isamath{\mathcal{X}}}
19.44 +\newcommand{\isasymY}{\isamath{\mathcal{Y}}}
19.45 +\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
19.46 +\newcommand{\isasyma}{\isamath{\mathrm{a}}}
19.47 +\newcommand{\isasymb}{\isamath{\mathrm{b}}}
19.48 +\newcommand{\isasymc}{\isamath{\mathrm{c}}}
19.49 +\newcommand{\isasymd}{\isamath{\mathrm{d}}}
19.50 +\newcommand{\isasyme}{\isamath{\mathrm{e}}}
19.51 +\newcommand{\isasymf}{\isamath{\mathrm{f}}}
19.52 +\newcommand{\isasymg}{\isamath{\mathrm{g}}}
19.53 +\newcommand{\isasymh}{\isamath{\mathrm{h}}}
19.54 +\newcommand{\isasymi}{\isamath{\mathrm{i}}}
19.55 +\newcommand{\isasymj}{\isamath{\mathrm{j}}}
19.56 +\newcommand{\isasymk}{\isamath{\mathrm{k}}}
19.57 +\newcommand{\isasyml}{\isamath{\mathrm{l}}}
19.58 +\newcommand{\isasymm}{\isamath{\mathrm{m}}}
19.59 +\newcommand{\isasymn}{\isamath{\mathrm{n}}}
19.60 +\newcommand{\isasymo}{\isamath{\mathrm{o}}}
19.61 +\newcommand{\isasymp}{\isamath{\mathrm{p}}}
19.62 +\newcommand{\isasymq}{\isamath{\mathrm{q}}}
19.63 +\newcommand{\isasymr}{\isamath{\mathrm{r}}}
19.64 +\newcommand{\isasyms}{\isamath{\mathrm{s}}}
19.65 +\newcommand{\isasymt}{\isamath{\mathrm{t}}}
19.66 +\newcommand{\isasymu}{\isamath{\mathrm{u}}}
19.67 +\newcommand{\isasymv}{\isamath{\mathrm{v}}}
19.68 +\newcommand{\isasymw}{\isamath{\mathrm{w}}}
19.69 +\newcommand{\isasymx}{\isamath{\mathrm{x}}}
19.70 +\newcommand{\isasymy}{\isamath{\mathrm{y}}}
19.71 +\newcommand{\isasymz}{\isamath{\mathrm{z}}}
19.72 +\newcommand{\isasymAA}{\isamath{\mathfrak{A}}} %requires eufrak
19.73 +\newcommand{\isasymBB}{\isamath{\mathfrak{B}}} %requires eufrak
19.74 +\newcommand{\isasymCC}{\isamath{\mathfrak{C}}} %requires eufrak
19.75 +\newcommand{\isasymDD}{\isamath{\mathfrak{D}}} %requires eufrak
19.76 +\newcommand{\isasymEE}{\isamath{\mathfrak{E}}} %requires eufrak
19.77 +\newcommand{\isasymFF}{\isamath{\mathfrak{F}}} %requires eufrak
19.78 +\newcommand{\isasymGG}{\isamath{\mathfrak{G}}} %requires eufrak
19.79 +\newcommand{\isasymHH}{\isamath{\mathfrak{H}}} %requires eufrak
19.80 +\newcommand{\isasymII}{\isamath{\mathfrak{I}}} %requires eufrak
19.81 +\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}} %requires eufrak
19.82 +\newcommand{\isasymKK}{\isamath{\mathfrak{K}}} %requires eufrak
19.83 +\newcommand{\isasymLL}{\isamath{\mathfrak{L}}} %requires eufrak
19.84 +\newcommand{\isasymMM}{\isamath{\mathfrak{M}}} %requires eufrak
19.85 +\newcommand{\isasymNN}{\isamath{\mathfrak{N}}} %requires eufrak
19.86 +\newcommand{\isasymOO}{\isamath{\mathfrak{O}}} %requires eufrak
19.87 +\newcommand{\isasymPP}{\isamath{\mathfrak{P}}} %requires eufrak
19.88 +\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}} %requires eufrak
19.89 +\newcommand{\isasymRR}{\isamath{\mathfrak{R}}} %requires eufrak
19.90 +\newcommand{\isasymSS}{\isamath{\mathfrak{S}}} %requires eufrak
19.91 +\newcommand{\isasymTT}{\isamath{\mathfrak{T}}} %requires eufrak
19.92 +\newcommand{\isasymUU}{\isamath{\mathfrak{U}}} %requires eufrak
19.93 +\newcommand{\isasymVV}{\isamath{\mathfrak{V}}} %requires eufrak
19.94 +\newcommand{\isasymWW}{\isamath{\mathfrak{W}}} %requires eufrak
19.95 +\newcommand{\isasymXX}{\isamath{\mathfrak{X}}} %requires eufrak
19.96 +\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}} %requires eufrak
19.97 +\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}} %requires eufrak
19.98 +\newcommand{\isasymaa}{\isamath{\mathfrak{a}}} %requires eufrak
19.99 +\newcommand{\isasymbb}{\isamath{\mathfrak{b}}} %requires eufrak
19.100 +\newcommand{\isasymcc}{\isamath{\mathfrak{c}}} %requires eufrak
19.101 +\newcommand{\isasymdd}{\isamath{\mathfrak{d}}} %requires eufrak
19.102 +\newcommand{\isasymee}{\isamath{\mathfrak{e}}} %requires eufrak
19.103 +\newcommand{\isasymff}{\isamath{\mathfrak{f}}} %requires eufrak
19.104 +\newcommand{\isasymgg}{\isamath{\mathfrak{g}}} %requires eufrak
19.105 +\newcommand{\isasymhh}{\isamath{\mathfrak{h}}} %requires eufrak
19.106 +\newcommand{\isasymii}{\isamath{\mathfrak{i}}} %requires eufrak
19.107 +\newcommand{\isasymjj}{\isamath{\mathfrak{j}}} %requires eufrak
19.108 +\newcommand{\isasymkk}{\isamath{\mathfrak{k}}} %requires eufrak
19.109 +\newcommand{\isasymll}{\isamath{\mathfrak{l}}} %requires eufrak
19.110 +\newcommand{\isasymmm}{\isamath{\mathfrak{m}}} %requires eufrak
19.111 +\newcommand{\isasymnn}{\isamath{\mathfrak{n}}} %requires eufrak
19.112 +\newcommand{\isasymoo}{\isamath{\mathfrak{o}}} %requires eufrak
19.113 +\newcommand{\isasympp}{\isamath{\mathfrak{p}}} %requires eufrak
19.114 +\newcommand{\isasymqq}{\isamath{\mathfrak{q}}} %requires eufrak
19.115 +\newcommand{\isasymrr}{\isamath{\mathfrak{r}}} %requires eufrak
19.116 +\newcommand{\isasymss}{\isamath{\mathfrak{s}}} %requires eufrak
19.117 +\newcommand{\isasymtt}{\isamath{\mathfrak{t}}} %requires eufrak
19.118 +\newcommand{\isasymuu}{\isamath{\mathfrak{u}}} %requires eufrak
19.119 +\newcommand{\isasymvv}{\isamath{\mathfrak{v}}} %requires eufrak
19.120 +\newcommand{\isasymww}{\isamath{\mathfrak{w}}} %requires eufrak
19.121 +\newcommand{\isasymxx}{\isamath{\mathfrak{x}}} %requires eufrak
19.122 +\newcommand{\isasymyy}{\isamath{\mathfrak{y}}} %requires eufrak
19.123 +\newcommand{\isasymzz}{\isamath{\mathfrak{z}}} %requires eufrak
19.124 +\newcommand{\isasymalpha}{\isamath{\alpha}}
19.125 +\newcommand{\isasymbeta}{\isamath{\beta}}
19.126 +\newcommand{\isasymgamma}{\isamath{\gamma}}
19.127 +\newcommand{\isasymdelta}{\isamath{\delta}}
19.128 +\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
19.129 +\newcommand{\isasymzeta}{\isamath{\zeta}}
19.130 +\newcommand{\isasymeta}{\isamath{\eta}}
19.131 +\newcommand{\isasymtheta}{\isamath{\vartheta}}
19.132 +\newcommand{\isasymiota}{\isamath{\iota}}
19.133 +\newcommand{\isasymkappa}{\isamath{\kappa}}
19.134 +\newcommand{\isasymlambda}{\isamath{\lambda}}
19.135 +\newcommand{\isasymmu}{\isamath{\mu}}
19.136 +\newcommand{\isasymnu}{\isamath{\nu}}
19.137 +\newcommand{\isasymxi}{\isamath{\xi}}
19.138 +\newcommand{\isasympi}{\isamath{\pi}}
19.139 +\newcommand{\isasymrho}{\isamath{\varrho}}
19.140 +\newcommand{\isasymsigma}{\isamath{\sigma}}
19.141 +\newcommand{\isasymtau}{\isamath{\tau}}
19.142 +\newcommand{\isasymupsilon}{\isamath{\upsilon}}
19.143 +\newcommand{\isasymphi}{\isamath{\varphi}}
19.144 +\newcommand{\isasymchi}{\isamath{\chi}}
19.145 +\newcommand{\isasympsi}{\isamath{\psi}}
19.146 +\newcommand{\isasymomega}{\isamath{\omega}}
19.147 +\newcommand{\isasymGamma}{\isamath{\Gamma}}
19.148 +\newcommand{\isasymDelta}{\isamath{\Delta}}
19.149 +\newcommand{\isasymTheta}{\isamath{\Theta}}
19.150 +\newcommand{\isasymLambda}{\isamath{\Lambda}}
19.151 +\newcommand{\isasymXi}{\isamath{\Xi}}
19.152 +\newcommand{\isasymPi}{\isamath{\Pi}}
19.153 +\newcommand{\isasymSigma}{\isamath{\Sigma}}
19.154 +\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
19.155 +\newcommand{\isasymPhi}{\isamath{\Phi}}
19.156 +\newcommand{\isasymPsi}{\isamath{\Psi}}
19.157 +\newcommand{\isasymOmega}{\isamath{\Omega}}
19.158 +\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
19.159 +\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
19.160 +\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
19.161 +\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
19.162 +\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
19.163 +\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
19.164 +\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
19.165 +\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
19.166 +\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
19.167 +\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
19.168 +\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
19.169 +\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
19.170 +\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
19.171 +\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
19.172 +\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
19.173 +\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
19.174 +\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
19.175 +\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
19.176 +\newcommand{\isasymmapsto}{\isamath{\mapsto}}
19.177 +\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
19.178 +\newcommand{\isasymmidarrow}{\isamath{\relbar}}
19.179 +\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
19.180 +\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
19.181 +\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
19.182 +\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
19.183 +\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
19.184 +\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
19.185 +\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
19.186 +\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
19.187 +\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
19.188 +\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}} %requires amssymb
19.189 +\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}} %requires amssymb
19.190 +\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}} %requires amssymb
19.191 +\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}} %requires amssymb
19.192 +\newcommand{\isasymrestriction}{\isamath{\restriction}} %requires amssymb
19.193 +\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
19.194 +\newcommand{\isasymup}{\isamath{\uparrow}}
19.195 +\newcommand{\isasymUp}{\isamath{\Uparrow}}
19.196 +\newcommand{\isasymdown}{\isamath{\downarrow}}
19.197 +\newcommand{\isasymDown}{\isamath{\Downarrow}}
19.198 +\newcommand{\isasymupdown}{\isamath{\updownarrow}}
19.199 +\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
19.200 +\newcommand{\isasymlangle}{\isamath{\langle}}
19.201 +\newcommand{\isasymrangle}{\isamath{\rangle}}
19.202 +\newcommand{\isasymlceil}{\isamath{\lceil}}
19.203 +\newcommand{\isasymrceil}{\isamath{\rceil}}
19.204 +\newcommand{\isasymlfloor}{\isamath{\lfloor}}
19.205 +\newcommand{\isasymrfloor}{\isamath{\rfloor}}
19.206 +\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
19.207 +\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}
19.208 +\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
19.209 +\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
19.210 +\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
19.211 +\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
19.212 +\newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel
19.213 +\newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel
19.214 +\newcommand{\isasymbottom}{\isamath{\bot}}
19.215 +\newcommand{\isasymtop}{\isamath{\top}}
19.216 +\newcommand{\isasymand}{\isamath{\wedge}}
19.217 +\newcommand{\isasymAnd}{\isamath{\bigwedge}}
19.218 +\newcommand{\isasymor}{\isamath{\vee}}
19.219 +\newcommand{\isasymOr}{\isamath{\bigvee}}
19.220 +\newcommand{\isasymforall}{\isamath{\forall\,}}
19.221 +\newcommand{\isasymexists}{\isamath{\exists\,}}
19.222 +\newcommand{\isasymnexists}{\isamath{\nexists\,}} %requires amssymb
19.223 +\newcommand{\isasymnot}{\isamath{\neg}}
19.224 +\newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb
19.225 +\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb
19.226 +\newcommand{\isasymturnstile}{\isamath{\vdash}}
19.227 +\newcommand{\isasymTurnstile}{\isamath{\models}}
19.228 +\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
19.229 +\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
19.230 +\newcommand{\isasymstileturn}{\isamath{\dashv}}
19.231 +\newcommand{\isasymsurd}{\isamath{\surd}}
19.232 +\newcommand{\isasymle}{\isamath{\le}}
19.233 +\newcommand{\isasymge}{\isamath{\ge}}
19.234 +\newcommand{\isasymlless}{\isamath{\ll}}
19.235 +\newcommand{\isasymggreater}{\isamath{\gg}}
19.236 +\newcommand{\isasymlesssim}{\isamath{\lesssim}} %requires amssymb
19.237 +\newcommand{\isasymgreatersim}{\isamath{\gtrsim}} %requires amssymb
19.238 +\newcommand{\isasymlessapprox}{\isamath{\lessapprox}} %requires amssymb
19.239 +\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}} %requires amssymb
19.240 +\newcommand{\isasymin}{\isamath{\in}}
19.241 +\newcommand{\isasymnotin}{\isamath{\notin}}
19.242 +\newcommand{\isasymsubset}{\isamath{\subset}}
19.243 +\newcommand{\isasymsupset}{\isamath{\supset}}
19.244 +\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
19.245 +\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
19.246 +\newcommand{\isasymsqsubset}{\isamath{\sqsubset}} %requires amssymb
19.247 +\newcommand{\isasymsqsupset}{\isamath{\sqsupset}} %requires amssymb
19.248 +\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
19.249 +\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
19.250 +\newcommand{\isasyminter}{\isamath{\cap}}
19.251 +\newcommand{\isasymInter}{\isamath{\bigcap\,}}
19.252 +\newcommand{\isasymunion}{\isamath{\cup}}
19.253 +\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
19.254 +\newcommand{\isasymsqunion}{\isamath{\sqcup}}
19.255 +\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
19.256 +\newcommand{\isasymsqinter}{\isamath{\sqcap}}
19.257 +\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires amsmath
19.258 +\newcommand{\isasymsetminus}{\isamath{\setminus}}
19.259 +\newcommand{\isasympropto}{\isamath{\propto}}
19.260 +\newcommand{\isasymuplus}{\isamath{\uplus}}
19.261 +\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
19.262 +\newcommand{\isasymnoteq}{\isamath{\not=}}
19.263 +\newcommand{\isasymsim}{\isamath{\sim}}
19.264 +\newcommand{\isasymdoteq}{\isamath{\doteq}}
19.265 +\newcommand{\isasymsimeq}{\isamath{\simeq}}
19.266 +\newcommand{\isasymapprox}{\isamath{\approx}}
19.267 +\newcommand{\isasymasymp}{\isamath{\asymp}}
19.268 +\newcommand{\isasymcong}{\isamath{\cong}}
19.269 +\newcommand{\isasymsmile}{\isamath{\smile}}
19.270 +\newcommand{\isasymequiv}{\isamath{\equiv}}
19.271 +\newcommand{\isasymfrown}{\isamath{\frown}}
19.272 +\newcommand{\isasymJoin}{\isamath{\Join}} %requires amssymb
19.273 +\newcommand{\isasymbowtie}{\isamath{\bowtie}}
19.274 +\newcommand{\isasymprec}{\isamath{\prec}}
19.275 +\newcommand{\isasymsucc}{\isamath{\succ}}
19.276 +\newcommand{\isasympreceq}{\isamath{\preceq}}
19.277 +\newcommand{\isasymsucceq}{\isamath{\succeq}}
19.278 +\newcommand{\isasymparallel}{\isamath{\parallel}}
19.279 +\newcommand{\isasymbar}{\isamath{\mid}}
19.280 +\newcommand{\isasymplusminus}{\isamath{\pm}}
19.281 +\newcommand{\isasymminusplus}{\isamath{\mp}}
19.282 +\newcommand{\isasymtimes}{\isamath{\times}}
19.283 +\newcommand{\isasymdiv}{\isamath{\div}}
19.284 +\newcommand{\isasymcdot}{\isamath{\cdot}}
19.285 +\newcommand{\isasymstar}{\isamath{\star}}
19.286 +\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
19.287 +\newcommand{\isasymcirc}{\isamath{\circ}}
19.288 +\newcommand{\isasymdagger}{\isamath{\dagger}}
19.289 +\newcommand{\isasymddagger}{\isamath{\ddagger}}
19.290 +\newcommand{\isasymlhd}{\isamath{\lhd}} %requires amssymb
19.291 +\newcommand{\isasymrhd}{\isamath{\rhd}} %requires amssymb
19.292 +\newcommand{\isasymunlhd}{\isamath{\unlhd}} %requires amssymb
19.293 +\newcommand{\isasymunrhd}{\isamath{\unrhd}} %requires amssymb
19.294 +\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
19.295 +\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
19.296 +\newcommand{\isasymtriangle}{\isamath{\triangle}}
19.297 +\newcommand{\isasymtriangleq}{\isamath{\triangleq}} %requires amssymb
19.298 +\newcommand{\isasymoplus}{\isamath{\oplus}}
19.299 +\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}
19.300 +\newcommand{\isasymotimes}{\isamath{\otimes}}
19.301 +\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}
19.302 +\newcommand{\isasymodot}{\isamath{\odot}}
19.303 +\newcommand{\isasymOdot}{\isamath{\bigodot\,}}
19.304 +\newcommand{\isasymominus}{\isamath{\ominus}}
19.305 +\newcommand{\isasymoslash}{\isamath{\oslash}}
19.306 +\newcommand{\isasymdots}{\isamath{\dots}}
19.307 +\newcommand{\isasymcdots}{\isamath{\cdots}}
19.308 +\newcommand{\isasymSum}{\isamath{\sum\,}}
19.309 +\newcommand{\isasymProd}{\isamath{\prod\,}}
19.310 +\newcommand{\isasymCoprod}{\isamath{\coprod\,}}
19.311 +\newcommand{\isasyminfinity}{\isamath{\infty}}
19.312 +\newcommand{\isasymintegral}{\isamath{\int\,}}
19.313 +\newcommand{\isasymointegral}{\isamath{\oint\,}}
19.314 +\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
19.315 +\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
19.316 +\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
19.317 +\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
19.318 +\newcommand{\isasymaleph}{\isamath{\aleph}}
19.319 +\newcommand{\isasymemptyset}{\isamath{\emptyset}}
19.320 +\newcommand{\isasymnabla}{\isamath{\nabla}}
19.321 +\newcommand{\isasympartial}{\isamath{\partial}}
19.322 +\newcommand{\isasymRe}{\isamath{\Re}}
19.323 +\newcommand{\isasymIm}{\isamath{\Im}}
19.324 +\newcommand{\isasymflat}{\isamath{\flat}}
19.325 +\newcommand{\isasymnatural}{\isamath{\natural}}
19.326 +\newcommand{\isasymsharp}{\isamath{\sharp}}
19.327 +\newcommand{\isasymangle}{\isamath{\angle}}
19.328 +\newcommand{\isasymcopyright}{\isatext{\rm\copyright}}
19.329 +\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
19.330 +\newcommand{\isasymhyphen}{\isatext{\rm-}}
19.331 +\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
19.332 +\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}} %requires latin1
19.333 +\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}} %requires latin1
19.334 +\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}} %requires latin1
19.335 +\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}} %requires latin1
19.336 +\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}} %requires latin1
19.337 +\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}} %requires latin1
19.338 +\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
19.339 +\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
19.340 +\newcommand{\isasymsection}{\isatext{\rm\S}}
19.341 +\newcommand{\isasymparagraph}{\isatext{\rm\P}}
19.342 +\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
19.343 +\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
19.344 +\newcommand{\isasymeuro}{\isatext{\textgreek{\euro}}} %requires greek babel
19.345 +\newcommand{\isasympounds}{\isamath{\pounds}}
19.346 +\newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb
19.347 +\newcommand{\isasymcent}{\isatext{\textcent}} %requires textcomp
19.348 +\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
19.349 +\newcommand{\isasymdegree}{\isatext{\rm\textdegree}} %requires latin1
19.350 +\newcommand{\isasymamalg}{\isamath{\amalg}}
19.351 +\newcommand{\isasymmho}{\isamath{\mho}} %requires amssymb
19.352 +\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssymb
19.353 +\newcommand{\isasymwp}{\isamath{\wp}}
19.354 +\newcommand{\isasymwrong}{\isamath{\wr}}
19.355 +\newcommand{\isasymstruct}{\isamath{\diamond}}
19.356 +\newcommand{\isasymacute}{\isatext{\'\relax}}
19.357 +\newcommand{\isasymindex}{\isatext{\i}}
19.358 +\newcommand{\isasymdieresis}{\isatext{\"\relax}}
19.359 +\newcommand{\isasymcedilla}{\isatext{\c\relax}}
19.360 +\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
19.361 +\newcommand{\isasymspacespace}{\isamath{~~}}
19.362 +\newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}
19.363 +\newcommand{\isasymsome}{\isamath{\epsilon\,}}