# HG changeset patch # User blanchet # Date 1346167023 -7200 # Node ID 2d17c305f4bcc4c057b96bc1ed8705719e6fbbfa # Parent 7f79f94a432cdf8c257f39cf4d22868578fbc5a5 documentation cleanup diff -r 7f79f94a432c -r 2d17c305f4bc src/HOL/Ordinals_and_Cardinals/Wellorder_Embedding.thy --- a/src/HOL/Ordinals_and_Cardinals/Wellorder_Embedding.thy Tue Aug 28 17:16:00 2012 +0200 +++ b/src/HOL/Ordinals_and_Cardinals/Wellorder_Embedding.thy Tue Aug 28 17:17:03 2012 +0200 @@ -2,10 +2,10 @@ Author: Andrei Popescu, TU Muenchen Copyright 2012 -Well-order embeddings (full). +Well-order embeddings. *) -header {* Well-Order Embeddings (Full) *} +header {* Well-Order Embeddings *} theory Wellorder_Embedding imports diff -r 7f79f94a432c -r 2d17c305f4bc src/HOL/Ordinals_and_Cardinals/document/isabelle.sty --- a/src/HOL/Ordinals_and_Cardinals/document/isabelle.sty Tue Aug 28 17:16:00 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,233 +0,0 @@ -%% -%% macros for Isabelle generated LaTeX output -%% - -%%% Simple document preparation (based on theory token language and symbols) - -% isabelle environments - -\newcommand{\isabellecontext}{UNKNOWN} - -\newcommand{\isastyle}{\UNDEF} -\newcommand{\isastyleminor}{\UNDEF} -\newcommand{\isastylescript}{\UNDEF} -\newcommand{\isastyletext}{\normalsize\rm} -\newcommand{\isastyletxt}{\rm} -\newcommand{\isastylecmt}{\rm} - -\newcommand{\isaspacing}{% - \sfcode 42 1000 % . - \sfcode 63 1000 % ? - \sfcode 33 1000 % ! - \sfcode 58 1000 % : - \sfcode 59 1000 % ; - \sfcode 44 1000 % , -} - -%symbol markup -- \emph achieves decent spacing via italic corrections -\newcommand{\isamath}[1]{\emph{$#1$}} -\newcommand{\isatext}[1]{\emph{#1}} -\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isaspacing\isastylescript##1}}} -\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} -\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} -\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} -\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} -\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isaspacing\isastylescript} -\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup} -\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\isastylescript} -\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup} -\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}} - -\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}} -\newcommand{\isaantiqopen}{\isakeyword{\isacharbraceleft}} -\newcommand{\isaantiqclose}{\isakeyword{\isacharbraceright}} - -\newdimen\isa@parindent\newdimen\isa@parskip - -\newenvironment{isabellebody}{% -\isamarkuptrue\par% -\isa@parindent\parindent\parindent0pt% -\isa@parskip\parskip\parskip0pt% -\isaspacing\isastyle}{\par} - -\newenvironment{isabelle} -{\begin{trivlist}\begin{isabellebody}\item\relax} -{\end{isabellebody}\end{trivlist}} - -\newcommand{\isa}[1]{\emph{\isaspacing\isastyleminor #1}} - -\newcommand{\isaindent}[1]{\hphantom{#1}} -\newcommand{\isanewline}{\mbox{}\par\mbox{}} -\newcommand{\isasep}{} -\newcommand{\isadigit}[1]{#1} - -\newcommand{\isachardefaults}{% -\chardef\isacharbang=`\!% -\chardef\isachardoublequote=`\"% -\chardef\isachardoublequoteopen=`\"% -\chardef\isachardoublequoteclose=`\"% -\chardef\isacharhash=`\#% -\chardef\isachardollar=`\$% -\chardef\isacharpercent=`\%% -\chardef\isacharampersand=`\&% -\chardef\isacharprime=`\'% -\chardef\isacharparenleft=`\(% -\chardef\isacharparenright=`\)% -\chardef\isacharasterisk=`\*% -\chardef\isacharplus=`\+% -\chardef\isacharcomma=`\,% -\chardef\isacharminus=`\-% -\chardef\isachardot=`\.% -\chardef\isacharslash=`\/% -\chardef\isacharcolon=`\:% -\chardef\isacharsemicolon=`\;% -\chardef\isacharless=`\<% -\chardef\isacharequal=`\=% -\chardef\isachargreater=`\>% -\chardef\isacharquery=`\?% -\chardef\isacharat=`\@% -\chardef\isacharbrackleft=`\[% -\chardef\isacharbackslash=`\\% -\chardef\isacharbrackright=`\]% -\chardef\isacharcircum=`\^% -\chardef\isacharunderscore=`\_% -\def\isacharunderscorekeyword{\_}% -\chardef\isacharbackquote=`\`% -\chardef\isacharbackquoteopen=`\`% -\chardef\isacharbackquoteclose=`\`% -\chardef\isacharbraceleft=`\{% -\chardef\isacharbar=`\|% -\chardef\isacharbraceright=`\}% -\chardef\isachartilde=`\~% -\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}% -\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}% -} - -\newcommand{\isaliteral}[2]{#2} -\newcommand{\isanil}{} - - -% keyword and section markup - -\newcommand{\isakeyword}[1] -{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}% -\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}} -\newcommand{\isacommand}[1]{\isakeyword{#1}} - -\newcommand{\isamarkupheader}[1]{\section{#1}} -\newcommand{\isamarkupchapter}[1]{\chapter{#1}} -\newcommand{\isamarkupsection}[1]{\section{#1}} -\newcommand{\isamarkupsubsection}[1]{\subsection{#1}} -\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}} -\newcommand{\isamarkupsect}[1]{\section{#1}} -\newcommand{\isamarkupsubsect}[1]{\subsection{#1}} -\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}} - -\newif\ifisamarkup -\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi} -\newcommand{\isaendpar}{\par\medskip} -\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar} -\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}} -\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}} -\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}} - - -% styles - -\def\isabellestyle#1{\csname isabellestyle#1\endcsname} - -\newcommand{\isabellestyledefault}{% -\def\isastyle{\small\tt\slshape}% -\def\isastyleminor{\small\tt\slshape}% -\def\isastylescript{\footnotesize\tt\slshape}% -\isachardefaults% -} -\isabellestyledefault - -\newcommand{\isabellestylett}{% -\def\isastyle{\small\tt}% -\def\isastyleminor{\small\tt}% -\def\isastylescript{\footnotesize\tt}% -\isachardefaults% -} - -\newcommand{\isabellestyleit}{% -\def\isastyle{\small\it}% -\def\isastyleminor{\it}% -\def\isastylescript{\footnotesize\it}% -\isachardefaults% -\def\isacharunderscorekeyword{\mbox{-}}% -\def\isacharbang{\isamath{!}}% -\def\isachardoublequote{\isanil}% -\def\isachardoublequoteopen{\isanil}% -\def\isachardoublequoteclose{\isanil}% -\def\isacharhash{\isamath{\#}}% -\def\isachardollar{\isamath{\$}}% -\def\isacharpercent{\isamath{\%}}% -\def\isacharampersand{\isamath{\&}}% -\def\isacharprime{\isamath{\mskip2mu{'}\mskip-2mu}}% -\def\isacharparenleft{\isamath{(}}% -\def\isacharparenright{\isamath{)}}% -\def\isacharasterisk{\isamath{*}}% -\def\isacharplus{\isamath{+}}% -\def\isacharcomma{\isamath{\mathord,}}% -\def\isacharminus{\isamath{-}}% -\def\isachardot{\isamath{\mathord.}}% -\def\isacharslash{\isamath{/}}% -\def\isacharcolon{\isamath{\mathord:}}% -\def\isacharsemicolon{\isamath{\mathord;}}% -\def\isacharless{\isamath{<}}% -\def\isacharequal{\isamath{=}}% -\def\isachargreater{\isamath{>}}% -\def\isacharat{\isamath{@}}% -\def\isacharbrackleft{\isamath{[}}% -\def\isacharbackslash{\isamath{\backslash}}% -\def\isacharbrackright{\isamath{]}}% -\def\isacharunderscore{\mbox{-}}% -\def\isacharbraceleft{\isamath{\{}}% -\def\isacharbar{\isamath{\mid}}% -\def\isacharbraceright{\isamath{\}}}% -\def\isachartilde{\isamath{{}\sp{\sim}}}% -\def\isacharbackquoteopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}% -\def\isacharbackquoteclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}% -\def\isacharverbatimopen{\isamath{\langle\!\langle}}% -\def\isacharverbatimclose{\isamath{\rangle\!\rangle}}% -} - -\newcommand{\isabellestyleitunderscore}{% -\isabellestyleit% -\def\isacharunderscore{\_}% -\def\isacharunderscorekeyword{\_}% -} - -\newcommand{\isabellestylesl}{% -\isabellestyleit% -\def\isastyle{\small\sl}% -\def\isastyleminor{\sl}% -\def\isastylescript{\footnotesize\sl}% -} - - -% tagged regions - -%plain TeX version of comment package -- much faster! -\let\isafmtname\fmtname\def\fmtname{plain} -\usepackage{comment} -\let\fmtname\isafmtname - -\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}} - -\newcommand{\isakeeptag}[1]% -{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}} -\newcommand{\isadroptag}[1]% -{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}} -\newcommand{\isafoldtag}[1]% -{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}} - -\isakeeptag{theory} -\isakeeptag{proof} -\isakeeptag{ML} -\isakeeptag{visible} -\isadroptag{invisible} - -\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{} diff -r 7f79f94a432c -r 2d17c305f4bc src/HOL/Ordinals_and_Cardinals/document/isabellesym.sty --- a/src/HOL/Ordinals_and_Cardinals/document/isabellesym.sty Tue Aug 28 17:16:00 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,360 +0,0 @@ -%% -%% definitions of standard Isabelle symbols -%% - -\newcommand{\isasymzero}{\isamath{\mathbf{0}}} %requires amssymb -\newcommand{\isasymone}{\isamath{\mathbf{1}}} %requires amssymb -\newcommand{\isasymtwo}{\isamath{\mathbf{2}}} %requires amssymb -\newcommand{\isasymthree}{\isamath{\mathbf{3}}} %requires amssymb -\newcommand{\isasymfour}{\isamath{\mathbf{4}}} %requires amssymb -\newcommand{\isasymfive}{\isamath{\mathbf{5}}} %requires amssymb -\newcommand{\isasymsix}{\isamath{\mathbf{6}}} %requires amssymb -\newcommand{\isasymseven}{\isamath{\mathbf{7}}} %requires amssymb -\newcommand{\isasymeight}{\isamath{\mathbf{8}}} %requires amssymb -\newcommand{\isasymnine}{\isamath{\mathbf{9}}} %requires amssymb -\newcommand{\isasymA}{\isamath{\mathcal{A}}} -\newcommand{\isasymB}{\isamath{\mathcal{B}}} -\newcommand{\isasymC}{\isamath{\mathcal{C}}} -\newcommand{\isasymD}{\isamath{\mathcal{D}}} -\newcommand{\isasymE}{\isamath{\mathcal{E}}} -\newcommand{\isasymF}{\isamath{\mathcal{F}}} -\newcommand{\isasymG}{\isamath{\mathcal{G}}} -\newcommand{\isasymH}{\isamath{\mathcal{H}}} -\newcommand{\isasymI}{\isamath{\mathcal{I}}} -\newcommand{\isasymJ}{\isamath{\mathcal{J}}} -\newcommand{\isasymK}{\isamath{\mathcal{K}}} -\newcommand{\isasymL}{\isamath{\mathcal{L}}} -\newcommand{\isasymM}{\isamath{\mathcal{M}}} -\newcommand{\isasymN}{\isamath{\mathcal{N}}} -\newcommand{\isasymO}{\isamath{\mathcal{O}}} -\newcommand{\isasymP}{\isamath{\mathcal{P}}} -\newcommand{\isasymQ}{\isamath{\mathcal{Q}}} -\newcommand{\isasymR}{\isamath{\mathcal{R}}} -\newcommand{\isasymS}{\isamath{\mathcal{S}}} -\newcommand{\isasymT}{\isamath{\mathcal{T}}} -\newcommand{\isasymU}{\isamath{\mathcal{U}}} -\newcommand{\isasymV}{\isamath{\mathcal{V}}} -\newcommand{\isasymW}{\isamath{\mathcal{W}}} -\newcommand{\isasymX}{\isamath{\mathcal{X}}} -\newcommand{\isasymY}{\isamath{\mathcal{Y}}} -\newcommand{\isasymZ}{\isamath{\mathcal{Z}}} -\newcommand{\isasyma}{\isamath{\mathrm{a}}} -\newcommand{\isasymb}{\isamath{\mathrm{b}}} -\newcommand{\isasymc}{\isamath{\mathrm{c}}} -\newcommand{\isasymd}{\isamath{\mathrm{d}}} -\newcommand{\isasyme}{\isamath{\mathrm{e}}} -\newcommand{\isasymf}{\isamath{\mathrm{f}}} -\newcommand{\isasymg}{\isamath{\mathrm{g}}} -\newcommand{\isasymh}{\isamath{\mathrm{h}}} -\newcommand{\isasymi}{\isamath{\mathrm{i}}} -\newcommand{\isasymj}{\isamath{\mathrm{j}}} -\newcommand{\isasymk}{\isamath{\mathrm{k}}} -\newcommand{\isasyml}{\isamath{\mathrm{l}}} -\newcommand{\isasymm}{\isamath{\mathrm{m}}} -\newcommand{\isasymn}{\isamath{\mathrm{n}}} -\newcommand{\isasymo}{\isamath{\mathrm{o}}} -\newcommand{\isasymp}{\isamath{\mathrm{p}}} -\newcommand{\isasymq}{\isamath{\mathrm{q}}} -\newcommand{\isasymr}{\isamath{\mathrm{r}}} -\newcommand{\isasyms}{\isamath{\mathrm{s}}} -\newcommand{\isasymt}{\isamath{\mathrm{t}}} -\newcommand{\isasymu}{\isamath{\mathrm{u}}} -\newcommand{\isasymv}{\isamath{\mathrm{v}}} -\newcommand{\isasymw}{\isamath{\mathrm{w}}} -\newcommand{\isasymx}{\isamath{\mathrm{x}}} -\newcommand{\isasymy}{\isamath{\mathrm{y}}} -\newcommand{\isasymz}{\isamath{\mathrm{z}}} -\newcommand{\isasymAA}{\isamath{\mathfrak{A}}} %requires eufrak -\newcommand{\isasymBB}{\isamath{\mathfrak{B}}} %requires eufrak -\newcommand{\isasymCC}{\isamath{\mathfrak{C}}} %requires eufrak -\newcommand{\isasymDD}{\isamath{\mathfrak{D}}} %requires eufrak -\newcommand{\isasymEE}{\isamath{\mathfrak{E}}} %requires eufrak -\newcommand{\isasymFF}{\isamath{\mathfrak{F}}} %requires eufrak -\newcommand{\isasymGG}{\isamath{\mathfrak{G}}} %requires eufrak -\newcommand{\isasymHH}{\isamath{\mathfrak{H}}} %requires eufrak -\newcommand{\isasymII}{\isamath{\mathfrak{I}}} %requires eufrak -\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}} %requires eufrak -\newcommand{\isasymKK}{\isamath{\mathfrak{K}}} %requires eufrak -\newcommand{\isasymLL}{\isamath{\mathfrak{L}}} %requires eufrak -\newcommand{\isasymMM}{\isamath{\mathfrak{M}}} %requires eufrak -\newcommand{\isasymNN}{\isamath{\mathfrak{N}}} %requires eufrak -\newcommand{\isasymOO}{\isamath{\mathfrak{O}}} %requires eufrak -\newcommand{\isasymPP}{\isamath{\mathfrak{P}}} %requires eufrak -\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}} %requires eufrak -\newcommand{\isasymRR}{\isamath{\mathfrak{R}}} %requires eufrak -\newcommand{\isasymSS}{\isamath{\mathfrak{S}}} %requires eufrak -\newcommand{\isasymTT}{\isamath{\mathfrak{T}}} %requires eufrak -\newcommand{\isasymUU}{\isamath{\mathfrak{U}}} %requires eufrak -\newcommand{\isasymVV}{\isamath{\mathfrak{V}}} %requires eufrak -\newcommand{\isasymWW}{\isamath{\mathfrak{W}}} %requires eufrak -\newcommand{\isasymXX}{\isamath{\mathfrak{X}}} %requires eufrak -\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}} %requires eufrak -\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}} %requires eufrak -\newcommand{\isasymaa}{\isamath{\mathfrak{a}}} %requires eufrak -\newcommand{\isasymbb}{\isamath{\mathfrak{b}}} %requires eufrak -\newcommand{\isasymcc}{\isamath{\mathfrak{c}}} %requires eufrak -\newcommand{\isasymdd}{\isamath{\mathfrak{d}}} %requires eufrak -\newcommand{\isasymee}{\isamath{\mathfrak{e}}} %requires eufrak -\newcommand{\isasymff}{\isamath{\mathfrak{f}}} %requires eufrak -\newcommand{\isasymgg}{\isamath{\mathfrak{g}}} %requires eufrak -\newcommand{\isasymhh}{\isamath{\mathfrak{h}}} %requires eufrak -\newcommand{\isasymii}{\isamath{\mathfrak{i}}} %requires eufrak -\newcommand{\isasymjj}{\isamath{\mathfrak{j}}} %requires eufrak -\newcommand{\isasymkk}{\isamath{\mathfrak{k}}} %requires eufrak -\newcommand{\isasymll}{\isamath{\mathfrak{l}}} %requires eufrak -\newcommand{\isasymmm}{\isamath{\mathfrak{m}}} %requires eufrak -\newcommand{\isasymnn}{\isamath{\mathfrak{n}}} %requires eufrak -\newcommand{\isasymoo}{\isamath{\mathfrak{o}}} %requires eufrak -\newcommand{\isasympp}{\isamath{\mathfrak{p}}} %requires eufrak -\newcommand{\isasymqq}{\isamath{\mathfrak{q}}} %requires eufrak -\newcommand{\isasymrr}{\isamath{\mathfrak{r}}} %requires eufrak -\newcommand{\isasymss}{\isamath{\mathfrak{s}}} %requires eufrak -\newcommand{\isasymtt}{\isamath{\mathfrak{t}}} %requires eufrak -\newcommand{\isasymuu}{\isamath{\mathfrak{u}}} %requires eufrak -\newcommand{\isasymvv}{\isamath{\mathfrak{v}}} %requires eufrak -\newcommand{\isasymww}{\isamath{\mathfrak{w}}} %requires eufrak -\newcommand{\isasymxx}{\isamath{\mathfrak{x}}} %requires eufrak -\newcommand{\isasymyy}{\isamath{\mathfrak{y}}} %requires eufrak -\newcommand{\isasymzz}{\isamath{\mathfrak{z}}} %requires eufrak -\newcommand{\isasymalpha}{\isamath{\alpha}} -\newcommand{\isasymbeta}{\isamath{\beta}} -\newcommand{\isasymgamma}{\isamath{\gamma}} -\newcommand{\isasymdelta}{\isamath{\delta}} -\newcommand{\isasymepsilon}{\isamath{\varepsilon}} -\newcommand{\isasymzeta}{\isamath{\zeta}} -\newcommand{\isasymeta}{\isamath{\eta}} -\newcommand{\isasymtheta}{\isamath{\vartheta}} -\newcommand{\isasymiota}{\isamath{\iota}} -\newcommand{\isasymkappa}{\isamath{\kappa}} -\newcommand{\isasymlambda}{\isamath{\lambda}} -\newcommand{\isasymmu}{\isamath{\mu}} -\newcommand{\isasymnu}{\isamath{\nu}} -\newcommand{\isasymxi}{\isamath{\xi}} -\newcommand{\isasympi}{\isamath{\pi}} -\newcommand{\isasymrho}{\isamath{\varrho}} -\newcommand{\isasymsigma}{\isamath{\sigma}} -\newcommand{\isasymtau}{\isamath{\tau}} -\newcommand{\isasymupsilon}{\isamath{\upsilon}} -\newcommand{\isasymphi}{\isamath{\varphi}} -\newcommand{\isasymchi}{\isamath{\chi}} -\newcommand{\isasympsi}{\isamath{\psi}} -\newcommand{\isasymomega}{\isamath{\omega}} -\newcommand{\isasymGamma}{\isamath{\Gamma}} -\newcommand{\isasymDelta}{\isamath{\Delta}} -\newcommand{\isasymTheta}{\isamath{\Theta}} -\newcommand{\isasymLambda}{\isamath{\Lambda}} -\newcommand{\isasymXi}{\isamath{\Xi}} -\newcommand{\isasymPi}{\isamath{\Pi}} -\newcommand{\isasymSigma}{\isamath{\Sigma}} -\newcommand{\isasymUpsilon}{\isamath{\Upsilon}} -\newcommand{\isasymPhi}{\isamath{\Phi}} -\newcommand{\isasymPsi}{\isamath{\Psi}} -\newcommand{\isasymOmega}{\isamath{\Omega}} -\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}} -\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}} -\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}} -\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}} -\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}} -\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}} -\newcommand{\isasymleftarrow}{\isamath{\leftarrow}} -\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}} -\newcommand{\isasymrightarrow}{\isamath{\rightarrow}} -\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}} -\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}} -\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}} -\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}} -\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}} -\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}} -\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}} -\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}} -\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}} -\newcommand{\isasymmapsto}{\isamath{\mapsto}} -\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}} -\newcommand{\isasymmidarrow}{\isamath{\relbar}} -\newcommand{\isasymMidarrow}{\isamath{\Relbar}} -\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}} -\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}} -\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}} -\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}} -\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}} -\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}} -\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}} -\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb -\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}} %requires amssymb -\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}} %requires amssymb -\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}} %requires amssymb -\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}} %requires amssymb -\newcommand{\isasymrestriction}{\isamath{\restriction}} %requires amssymb -\newcommand{\isasymColon}{\isamath{\mathrel{::}}} -\newcommand{\isasymup}{\isamath{\uparrow}} -\newcommand{\isasymUp}{\isamath{\Uparrow}} -\newcommand{\isasymdown}{\isamath{\downarrow}} -\newcommand{\isasymDown}{\isamath{\Downarrow}} -\newcommand{\isasymupdown}{\isamath{\updownarrow}} -\newcommand{\isasymUpdown}{\isamath{\Updownarrow}} -\newcommand{\isasymlangle}{\isamath{\langle}} -\newcommand{\isasymrangle}{\isamath{\rangle}} -\newcommand{\isasymlceil}{\isamath{\lceil}} -\newcommand{\isasymrceil}{\isamath{\rceil}} -\newcommand{\isasymlfloor}{\isamath{\lfloor}} -\newcommand{\isasymrfloor}{\isamath{\rfloor}} -\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}} -\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}} -\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}} -\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}} -\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}} -\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}} -\newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel -\newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel -\newcommand{\isasymbottom}{\isamath{\bot}} -\newcommand{\isasymtop}{\isamath{\top}} -\newcommand{\isasymand}{\isamath{\wedge}} -\newcommand{\isasymAnd}{\isamath{\bigwedge}} -\newcommand{\isasymor}{\isamath{\vee}} -\newcommand{\isasymOr}{\isamath{\bigvee}} -\newcommand{\isasymforall}{\isamath{\forall\,}} -\newcommand{\isasymexists}{\isamath{\exists\,}} -\newcommand{\isasymnexists}{\isamath{\nexists\,}} %requires amssymb -\newcommand{\isasymnot}{\isamath{\neg}} -\newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb -\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb -\newcommand{\isasymturnstile}{\isamath{\vdash}} -\newcommand{\isasymTurnstile}{\isamath{\models}} -\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}} -\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}} -\newcommand{\isasymstileturn}{\isamath{\dashv}} -\newcommand{\isasymsurd}{\isamath{\surd}} -\newcommand{\isasymle}{\isamath{\le}} -\newcommand{\isasymge}{\isamath{\ge}} -\newcommand{\isasymlless}{\isamath{\ll}} -\newcommand{\isasymggreater}{\isamath{\gg}} -\newcommand{\isasymlesssim}{\isamath{\lesssim}} %requires amssymb -\newcommand{\isasymgreatersim}{\isamath{\gtrsim}} %requires amssymb -\newcommand{\isasymlessapprox}{\isamath{\lessapprox}} %requires amssymb -\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}} %requires amssymb -\newcommand{\isasymin}{\isamath{\in}} -\newcommand{\isasymnotin}{\isamath{\notin}} -\newcommand{\isasymsubset}{\isamath{\subset}} -\newcommand{\isasymsupset}{\isamath{\supset}} -\newcommand{\isasymsubseteq}{\isamath{\subseteq}} -\newcommand{\isasymsupseteq}{\isamath{\supseteq}} -\newcommand{\isasymsqsubset}{\isamath{\sqsubset}} %requires amssymb -\newcommand{\isasymsqsupset}{\isamath{\sqsupset}} %requires amssymb -\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}} -\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}} -\newcommand{\isasyminter}{\isamath{\cap}} -\newcommand{\isasymInter}{\isamath{\bigcap\,}} -\newcommand{\isasymunion}{\isamath{\cup}} -\newcommand{\isasymUnion}{\isamath{\bigcup\,}} -\newcommand{\isasymsqunion}{\isamath{\sqcup}} -\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}} -\newcommand{\isasymsqinter}{\isamath{\sqcap}} -\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires stmaryrd -\newcommand{\isasymsetminus}{\isamath{\setminus}} -\newcommand{\isasympropto}{\isamath{\propto}} -\newcommand{\isasymuplus}{\isamath{\uplus}} -\newcommand{\isasymUplus}{\isamath{\biguplus\,}} -\newcommand{\isasymnoteq}{\isamath{\not=}} -\newcommand{\isasymsim}{\isamath{\sim}} -\newcommand{\isasymdoteq}{\isamath{\doteq}} -\newcommand{\isasymsimeq}{\isamath{\simeq}} -\newcommand{\isasymapprox}{\isamath{\approx}} -\newcommand{\isasymasymp}{\isamath{\asymp}} -\newcommand{\isasymcong}{\isamath{\cong}} -\newcommand{\isasymsmile}{\isamath{\smile}} -\newcommand{\isasymequiv}{\isamath{\equiv}} -\newcommand{\isasymfrown}{\isamath{\frown}} -\newcommand{\isasymJoin}{\isamath{\Join}} %requires amssymb -\newcommand{\isasymbowtie}{\isamath{\bowtie}} -\newcommand{\isasymprec}{\isamath{\prec}} -\newcommand{\isasymsucc}{\isamath{\succ}} -\newcommand{\isasympreceq}{\isamath{\preceq}} -\newcommand{\isasymsucceq}{\isamath{\succeq}} -\newcommand{\isasymparallel}{\isamath{\parallel}} -\newcommand{\isasymbar}{\isamath{\mid}} -\newcommand{\isasymplusminus}{\isamath{\pm}} -\newcommand{\isasymminusplus}{\isamath{\mp}} -\newcommand{\isasymtimes}{\isamath{\times}} -\newcommand{\isasymdiv}{\isamath{\div}} -\newcommand{\isasymcdot}{\isamath{\cdot}} -\newcommand{\isasymstar}{\isamath{\star}} -\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}} -\newcommand{\isasymcirc}{\isamath{\circ}} -\newcommand{\isasymdagger}{\isamath{\dagger}} -\newcommand{\isasymddagger}{\isamath{\ddagger}} -\newcommand{\isasymlhd}{\isamath{\lhd}} %requires amssymb -\newcommand{\isasymrhd}{\isamath{\rhd}} %requires amssymb -\newcommand{\isasymunlhd}{\isamath{\unlhd}} %requires amssymb -\newcommand{\isasymunrhd}{\isamath{\unrhd}} %requires amssymb -\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}} -\newcommand{\isasymtriangleright}{\isamath{\triangleright}} -\newcommand{\isasymtriangle}{\isamath{\triangle}} -\newcommand{\isasymtriangleq}{\isamath{\triangleq}} %requires amssymb -\newcommand{\isasymoplus}{\isamath{\oplus}} -\newcommand{\isasymOplus}{\isamath{\bigoplus\,}} -\newcommand{\isasymotimes}{\isamath{\otimes}} -\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}} -\newcommand{\isasymodot}{\isamath{\odot}} -\newcommand{\isasymOdot}{\isamath{\bigodot\,}} -\newcommand{\isasymominus}{\isamath{\ominus}} -\newcommand{\isasymoslash}{\isamath{\oslash}} -\newcommand{\isasymdots}{\isamath{\dots}} -\newcommand{\isasymcdots}{\isamath{\cdots}} -\newcommand{\isasymSum}{\isamath{\sum\,}} -\newcommand{\isasymProd}{\isamath{\prod\,}} -\newcommand{\isasymCoprod}{\isamath{\coprod\,}} -\newcommand{\isasyminfinity}{\isamath{\infty}} -\newcommand{\isasymintegral}{\isamath{\int\,}} -\newcommand{\isasymointegral}{\isamath{\oint\,}} -\newcommand{\isasymclubsuit}{\isamath{\clubsuit}} -\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}} -\newcommand{\isasymheartsuit}{\isamath{\heartsuit}} -\newcommand{\isasymspadesuit}{\isamath{\spadesuit}} -\newcommand{\isasymaleph}{\isamath{\aleph}} -\newcommand{\isasymemptyset}{\isamath{\emptyset}} -\newcommand{\isasymnabla}{\isamath{\nabla}} -\newcommand{\isasympartial}{\isamath{\partial}} -\newcommand{\isasymRe}{\isamath{\Re}} -\newcommand{\isasymIm}{\isamath{\Im}} -\newcommand{\isasymflat}{\isamath{\flat}} -\newcommand{\isasymnatural}{\isamath{\natural}} -\newcommand{\isasymsharp}{\isamath{\sharp}} -\newcommand{\isasymangle}{\isamath{\angle}} -\newcommand{\isasymcopyright}{\isatext{\rm\copyright}} -\newcommand{\isasymregistered}{\isatext{\rm\textregistered}} -\newcommand{\isasymhyphen}{\isatext{\rm-}} -\newcommand{\isasyminverse}{\isamath{{}^{-1}}} -\newcommand{\isasymonesuperior}{\isamath{{}^1}} -\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}} %requires textcomp -\newcommand{\isasymtwosuperior}{\isamath{{}^2}} -\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}} %requires textcomp -\newcommand{\isasymthreesuperior}{\isamath{{}^3}} -\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}} %requires textcomp -\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}} -\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}} -\newcommand{\isasymsection}{\isatext{\rm\S}} -\newcommand{\isasymparagraph}{\isatext{\rm\P}} -\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}} -\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}} -\newcommand{\isasymeuro}{\isatext{\textgreek{\euro}}} %requires greek babel -\newcommand{\isasympounds}{\isamath{\pounds}} -\newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb -\newcommand{\isasymcent}{\isatext{\textcent}} %requires textcomp -\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp -\newcommand{\isasymdegree}{\isatext{\rm\textdegree}} %requires textcomp -\newcommand{\isasymamalg}{\isamath{\amalg}} -\newcommand{\isasymmho}{\isamath{\mho}} %requires amssymb -\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssymb -\newcommand{\isasymwp}{\isamath{\wp}} -\newcommand{\isasymwrong}{\isamath{\wr}} -\newcommand{\isasymstruct}{\isamath{\diamond}} -\newcommand{\isasymacute}{\isatext{\'\relax}} -\newcommand{\isasymindex}{\isatext{\i}} -\newcommand{\isasymdieresis}{\isatext{\"\relax}} -\newcommand{\isasymcedilla}{\isatext{\c\relax}} -\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}} -\newcommand{\isasymspacespace}{\isamath{~~}} -\newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}} -\newcommand{\isasymsome}{\isamath{\epsilon\,}} -\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}} -\newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}} diff -r 7f79f94a432c -r 2d17c305f4bc src/HOL/Ordinals_and_Cardinals/document/isabelletags.sty diff -r 7f79f94a432c -r 2d17c305f4bc src/HOL/Ordinals_and_Cardinals/document/pdfsetup.sty --- a/src/HOL/Ordinals_and_Cardinals/document/pdfsetup.sty Tue Aug 28 17:16:00 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,7 +0,0 @@ -%% -%% default hyperref setup (both for pdf and dvi output) -%% - -\usepackage{color} -\definecolor{linkcolor}{rgb}{0,0,0.5} -\usepackage[colorlinks=true,linkcolor=linkcolor,citecolor=linkcolor,filecolor=linkcolor,pagecolor=linkcolor,urlcolor=linkcolor]{hyperref} diff -r 7f79f94a432c -r 2d17c305f4bc src/HOL/Ordinals_and_Cardinals/document/railsetup.sty --- a/src/HOL/Ordinals_and_Cardinals/document/railsetup.sty Tue Aug 28 17:16:00 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1202 +0,0 @@ -% rail.sty - style file to support railroad diagrams -% -% 09-Jul-90 L. Rooijakkers -% 08-Oct-90 L. Rooijakkers fixed centering bug when \rail@tmpc<0. -% 07-Feb-91 L. Rooijakkers added \railoptions command, indexing -% 08-Feb-91 L. Rooijakkers minor fixes -% 28-Jun-94 K. Barthelmann turned into LaTeX2e package -% 08-Dec-96 K. Barthelmann replaced \@writefile -% 13-Dec-96 K. Barthelmann cleanup -% 22-Feb-98 K. Barthelmann fixed catcodes of special characters -% 18-Apr-98 K. Barthelmann fixed \par handling -% 19-May-98 J. Olsson Added new macros to support arrow heads. -% 26-Jul-98 K. Barthelmann changed \par to output newlines -% 02-May-11 M. Wenzel default setup for Isabelle -% -% This style file needs to be used in conjunction with the 'rail' -% program. Running LaTeX as 'latex file' produces file.rai, which should be -% processed by Rail with 'rail file'. This produces file.rao, which will -% be picked up by LaTeX on the next 'latex file' run. -% -% LaTeX will warn if there is no file.rao or it's out of date. -% -% The macros in this file thus consist of two parts: those that read and -% write the .rai and .rao files, and those that do the actual formatting -% of the railroad diagrams. - -\NeedsTeXFormat{LaTeX2e} -\ProvidesPackage{rail}[1998/05/19] - -% railroad diagram formatting parameters (user level) -% all of these are copied into their internal versions by \railinit -% -% \railunit : \unitlength within railroad diagrams -% \railextra : extra length at outside of diagram -% \railboxheight : height of ovals and frames -% \railboxskip : vertical space between lines -% \railboxleft : space to the left of a box -% \railboxright : space to the right of a box -% \railovalspace : extra space around contents of oval -% \railframespace : extra space around contents of frame -% \railtextleft : space to the left of text -% \railtextright : space to the right of text -% \railtextup : space to lift text up -% \railjoinsize : circle size of join/split arcs -% \railjoinadjust : space to adjust join -% -% \railnamesep : separator between name and rule body - -\newlength\railunit -\newlength\railextra -\newlength\railboxheight -\newlength\railboxskip -\newlength\railboxleft -\newlength\railboxright -\newlength\railovalspace -\newlength\railframespace -\newlength\railtextleft -\newlength\railtextright -\newlength\railtextup -\newlength\railjoinsize -\newlength\railjoinadjust -\newlength\railnamesep - -% initialize the parameters - -\setlength\railunit{1sp} -\setlength\railextra{4ex} -\setlength\railboxleft{1ex} -\setlength\railboxright{1ex} -\setlength\railovalspace{2ex} -\setlength\railframespace{2ex} -\setlength\railtextleft{1ex} -\setlength\railtextright{1ex} -\setlength\railjoinadjust{0pt} -\setlength\railnamesep{1ex} - -\DeclareOption{10pt}{ - \setlength\railboxheight{16pt} - \setlength\railboxskip{24pt} - \setlength\railtextup{5pt} - \setlength\railjoinsize{16pt} -} -\DeclareOption{11pt}{ - \setlength\railboxheight{16pt} - \setlength\railboxskip{24pt} - \setlength\railtextup{5pt} - \setlength\railjoinsize{16pt} -} -\DeclareOption{12pt}{ - \setlength\railboxheight{20pt} - \setlength\railboxskip{28pt} - \setlength\railtextup{6pt} - \setlength\railjoinsize{20pt} -} - -\ExecuteOptions{10pt} -\ProcessOptions - -% internal versions of the formatting parameters -% -% \rail@extra : \railextra -% \rail@boxht : \railboxheight -% \rail@boxsp : \railboxskip -% \rail@boxlf : \railboxleft -% \rail@boxrt : \railboxright -% \rail@boxhht : \railboxheight / 2 -% \rail@ovalsp : \railovalspace -% \rail@framesp : \railframespace -% \rail@textlf : \railtextleft -% \rail@textrt : \railtextright -% \rail@textup : \railtextup -% \rail@joinsz : \railjoinsize -% \rail@joinhsz : \railjoinsize / 2 -% \rail@joinadj : \railjoinadjust -% -% \railinit : internalize all of the parameters. - -\newcount\rail@extra -\newcount\rail@boxht -\newcount\rail@boxsp -\newcount\rail@boxlf -\newcount\rail@boxrt -\newcount\rail@boxhht -\newcount\rail@ovalsp -\newcount\rail@framesp -\newcount\rail@textlf -\newcount\rail@textrt -\newcount\rail@textup -\newcount\rail@joinsz -\newcount\rail@joinhsz -\newcount\rail@joinadj - -\newcommand\railinit{ -\rail@extra=\railextra -\divide\rail@extra by \railunit -\rail@boxht=\railboxheight -\divide\rail@boxht by \railunit -\rail@boxsp=\railboxskip -\divide\rail@boxsp by \railunit -\rail@boxlf=\railboxleft -\divide\rail@boxlf by \railunit -\rail@boxrt=\railboxright -\divide\rail@boxrt by \railunit -\rail@boxhht=\railboxheight -\divide\rail@boxhht by \railunit -\divide\rail@boxhht by 2 -\rail@ovalsp=\railovalspace -\divide\rail@ovalsp by \railunit -\rail@framesp=\railframespace -\divide\rail@framesp by \railunit -\rail@textlf=\railtextleft -\divide\rail@textlf by \railunit -\rail@textrt=\railtextright -\divide\rail@textrt by \railunit -\rail@textup=\railtextup -\divide\rail@textup by \railunit -\rail@joinsz=\railjoinsize -\divide\rail@joinsz by \railunit -\rail@joinhsz=\railjoinsize -\divide\rail@joinhsz by \railunit -\divide\rail@joinhsz by 2 -\rail@joinadj=\railjoinadjust -\divide\rail@joinadj by \railunit -} - -\AtBeginDocument{\railinit} - -% \rail@param : declarations for list environment -% -% \railparam{TEXT} : sets \rail@param to TEXT -% -% \rail@reserved : characters reserved for grammar - -\newcommand\railparam[1]{ -\def\rail@param{ - \setlength\leftmargin{0pt}\setlength\rightmargin{0pt} - \setlength\labelwidth{0pt}\setlength\labelsep{0pt} - \setlength\itemindent{0pt}\setlength\listparindent{0pt} - #1 -} -} -\railparam{} - -\newtoks\rail@reserved -\rail@reserved={:;|*+?[]()'"} - -% \rail@termfont : format setup for terminals -% -% \rail@nontfont : format setup for nonterminals -% -% \rail@annofont : format setup for annotations -% -% \rail@rulefont : format setup for rule names -% -% \rail@indexfont : format setup for index entry -% -% \railtermfont{TEXT} : set terminal format setup to TEXT -% -% \railnontermfont{TEXT} : set nonterminal format setup to TEXT -% -% \railannotatefont{TEXT} : set annotation format setup to TEXT -% -% \railnamefont{TEXT} : set rule name format setup to TEXT -% -% \railindexfont{TEXT} : set index entry format setup to TEXT - -\def\rail@termfont{\ttfamily\upshape} -\def\rail@nontfont{\rmfamily\upshape} -\def\rail@annofont{\rmfamily\itshape} -\def\rail@namefont{\rmfamily\itshape} -\def\rail@indexfont{\rmfamily\itshape} - -\newcommand\railtermfont[1]{ -\def\rail@termfont{#1} -} - -\newcommand\railnontermfont[1]{ -\def\rail@nontfont{#1} -} - -\newcommand\railannotatefont[1]{ -\def\rail@annofont{#1} -} - -\newcommand\railnamefont[1]{ -\def\rail@namefont{#1} -} - -\newcommand\railindexfont[1]{ -\def\rail@indexfont{#1} -} - -% railroad read/write macros -% -% \begin{rail} TEXT \end{rail} : TEXT is written out to the .rai file, -% as \rail@i{NR}{TEXT}. Then the matching -% \rail@o{NR}{FMT} from the .rao file is -% executed (if defined). -% -% \railoptions{OPTIONS} : OPTIONS are written out to the .rai file, -% as \rail@p{OPTIONS}. -% -% \railterm{IDENT,IDENT,...} : format IDENT as terminals. writes out -% \rail@t{IDENT} to the .rai file -% -% \railalias{IDENT}{TEXT} : format IDENT as TEXT. defines \rail@t@IDENT as -% TEXT. -% -% \railtoken{IDENT}{TEXT} : abbreviates \railalias{IDENT}{TEXT}\railterm{IDENT} -% (for backward compatibility) -% -% \rail@setcodes : guards special characters -% -% \rail@makeother{CHARACTER} : sets \catcode of CHARACTER to "other" -% used inside a loop for \rail@setcodes -% -% \rail@nr : railroad diagram counter -% -% \ifrail@match : current \rail@i{NR}{TEXT} matches -% -% \rail@first : actions to be done first. read in .rao file, -% open .rai file if \@filesw true, undefine \rail@first. -% executed from \begin{rail}, \railoptions and \railterm. -% -% \rail@i{NR}{TEXT} : defines \rail@i@NR as TEXT. written to the .rai -% file by \rail, read from the .rao file by -% \rail@first -% -% \rail@t{IDENT} : tells Rail that IDENT is to be custom formatted, -% written to the .rai file by \railterm. -% -% \rail@o{NR}{TEXT} : defines \rail@o@NR as TEXT, read from the .rao -% file by \rail@first. -% -% \rail@p{OPTIONS} : pass options to rail, written to the .rai file by -% \railoptions -% -% \rail@write{TEXT} : write TEXT to the .rai file -% -% \rail@warn : warn user for mismatching diagrams -% -% \rail@endwarn : either \relax or \rail@warn -% -% \ifrail@all : checked at the end of the document - -\def\rail@makeother#1{ - \expandafter\catcode\expandafter`\csname\string #1\endcsname=12 -} - -\def\rail@setcodes{ -\let\par=\relax -\let\\=\relax -\expandafter\@tfor\expandafter\rail@symbol\expandafter:\expandafter=% - \the\rail@reserved -\do{\expandafter\rail@makeother\rail@symbol} -} - -\newcount\rail@nr - -\newif\ifrail@all -\rail@alltrue - -\newif\ifrail@match - -\def\rail@first{ -\begingroup -\makeatletter -\rail@setcodes -\InputIfFileExists{\jobname.rao}{}{\PackageInfo{rail}{No file \jobname.rao}} -\makeatother -\endgroup -\if@filesw -\newwrite\tf@rai -\immediate\openout\tf@rai=\jobname.rai -\fi -\global\let\rail@first=\relax -} - -\long\def\rail@body#1\end{ -{ -\newlinechar=`^^J -\def\par{\string\par^^J} -\rail@write{\string\rail@i{\number\rail@nr}{#1}} -} -\xdef\rail@i@{#1} -\end -} - -\newenvironment{rail}{ -\global\advance\rail@nr by 1 -\rail@first -\begingroup -\rail@setcodes -\rail@body -}{ -\endgroup -\rail@matchtrue -\@ifundefined{rail@o@\number\rail@nr}{\rail@matchfalse}{} -\expandafter\ifx\csname rail@i@\number\rail@nr\endcsname\rail@i@ -\else -\rail@matchfalse -\fi -\ifrail@match -\csname rail@o@\number\rail@nr\endcsname -\else -\PackageWarning{rail}{Railroad diagram {\number\rail@nr} doesn't match} -\global\let\rail@endwarn=\rail@warn -\begin{list}{}{\rail@param} -\rail@begin{1}{} -\rail@setbox{\bfseries ???} -\rail@oval -\rail@end -\end{list} -\fi -} - -\newcommand\railoptions[1]{ -\rail@first -\rail@write{\string\rail@p{#1}} -} - -\newcommand\railterm[1]{ -\rail@first -\@for\rail@@:=#1\do{ -\rail@write{\string\rail@t{\rail@@}} -} -} - -\newcommand\railalias[2]{ -\expandafter\def\csname rail@t@#1\endcsname{#2} -} - -\newcommand\railtoken[2]{\railalias{#1}{#2}\railterm{#1}} - -\long\def\rail@i#1#2{ -\expandafter\gdef\csname rail@i@#1\endcsname{#2} -} - -\def\rail@o#1#2{ -\expandafter\gdef\csname rail@o@#1\endcsname{ -\begin{list}{}{\rail@param} -#2 -\end{list} -} -} - -\def\rail@t#1{} - -\def\rail@p#1{} - -\long\def\rail@write#1{\@ifundefined{tf@rai}{}{\immediate\write\tf@rai{#1}}} - -\def\rail@warn{ -\PackageWarningNoLine{rail}{Railroad diagram(s) may have changed. - Use 'rail' and rerun} -} - -\let\rail@endwarn=\relax - -\AtEndDocument{\rail@endwarn} - -% index entry macro -% -% \rail@index{IDENT} : add index entry for IDENT - -\def\rail@index#1{ -\index{\rail@indexfont#1} -} - -% railroad formatting primitives -% -% \rail@x : current x -% \rail@y : current y -% \rail@ex : current end x -% \rail@sx : starting x for \rail@cr -% \rail@rx : rightmost previous x for \rail@cr -% -% \rail@tmpa : temporary count -% \rail@tmpb : temporary count -% \rail@tmpc : temporary count -% -% \rail@put : put at (\rail@x,\rail@y) -% \rail@vput : put vector at (\rail@x,\rail@y) -% -% \rail@eline : end line by drawing from \rail@ex to \rail@x -% -% \rail@vreline : end line by drawing a vector from \rail@x to \rail@ex -% -% \rail@vleline : end line by drawing a vector from \rail@ex to \rail@x -% -% \rail@sety{LEVEL} : set \rail@y to level LEVEL - -\newcount\rail@x -\newcount\rail@y -\newcount\rail@ex -\newcount\rail@sx -\newcount\rail@rx - -\newcount\rail@tmpa -\newcount\rail@tmpb -\newcount\rail@tmpc - -\def\rail@put{\put(\number\rail@x,\number\rail@y)} - -\def\rail@vput{\put(\number\rail@ex,\number\rail@y)} - -\def\rail@eline{ -\rail@tmpb=\rail@x -\advance\rail@tmpb by -\rail@ex -\rail@put{\line(-1,0){\number\rail@tmpb}} -} - -\def\rail@vreline{ -\rail@tmpb=\rail@x -\advance\rail@tmpb by -\rail@ex -\rail@vput{\vector(1,0){\number\rail@tmpb}} -} - -\def\rail@vleline{ -\rail@tmpb=\rail@x -\advance\rail@tmpb by -\rail@ex -\rail@put{\vector(-1,0){\number\rail@tmpb}} -} - -\def\rail@sety#1{ -\rail@y=#1 -\multiply\rail@y by -\rail@boxsp -\advance\rail@y by -\rail@boxht -} - -% \rail@begin{HEIGHT}{NAME} : begin a railroad diagram of height HEIGHT -% -% \rail@end : end a railroad diagram -% -% \rail@expand{IDENT} : expand IDENT - -\def\rail@begin#1#2{ -\item -\begin{minipage}[t]{\linewidth} -\ifx\@empty#2\else -{\rail@namefont \rail@expand{#2}}\\*[\railnamesep] -\fi -\unitlength=\railunit -\rail@tmpa=#1 -\multiply\rail@tmpa by \rail@boxsp -\begin{picture}(0,\number\rail@tmpa)(0,-\number\rail@tmpa) -\rail@ex=0 -\rail@rx=0 -\rail@x=\rail@extra -\rail@sx=\rail@x -\rail@sety{0} -} - -\def\rail@end{ -\advance\rail@x by \rail@extra -\rail@eline -\end{picture} -\end{minipage} -} - -\def\rail@vend{ -\advance\rail@x by \rail@extra -\rail@vreline -\end{picture} -\end{minipage} -} - -\def\rail@expand#1{\@ifundefined{rail@t@#1}{#1}{\csname rail@t@#1\endcsname}} - -% \rail@token{TEXT}[ANNOT] : format token TEXT with annotation -% \rail@ltoken{TEXT}[ANNOT] : format token TEXT with annotation, arrow left -% \rail@rtoken{TEXT}[ANNOT] : format token TEXT with annotation, arrow right -% -% \rail@ctoken{TEXT}[ANNOT] : format token TEXT centered with annotation -% \rail@lctoken{TEXT}[ANNOT] : format token TEXT centered with annotation, arrow left -% \rail@rctoken{TEXT}[ANNOT] : format token TEXT centered with annotation, arrow right -% -% \rail@nont{TEXT}[ANNOT] : format nonterminal TEXT with annotation -% \rail@lnont{TEXT}[ANNOT] : format nonterminal TEXT with annotation, arrow left -% \rail@rnont{TEXT}[ANNOT] : format nonterminal TEXT with annotation. arrow right -% -% \rail@cnont{TEXT}[ANNOT] : format nonterminal TEXT centered with annotation -% \rail@lcnont{TEXT}[ANNOT] : format nonterminal TEXT centered with annotation, -% arrow left -% \rail@rcnont{TEXT}[ANNOT] : format nonterminal TEXT centered with annotation, -% arrow right -% -% \rail@term{TEXT}[ANNOT] : format terminal TEXT with annotation -% \rail@lterm{TEXT}[ANNOT] : format terminal TEXT with annotation, arrow left -% \rail@rterm{TEXT}[ANNOT] : format terminal TEXT with annotation, arrow right -% -% \rail@cterm{TEXT}[ANNOT] : format terminal TEXT centered with annotation -% \rail@lcterm{TEXT}[ANNOT] : format terminal TEXT centered with annotation, arrow left -% \rail@rcterm{TEXT}[ANNOT] : format terminal TEXT centered with annotation, -% arrow right -% -% \rail@annote[TEXT] : format TEXT as annotation - -\def\rail@token#1[#2]{ -\rail@setbox{% -{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi -} -\rail@oval -} - -\def\rail@ltoken#1[#2]{ -\rail@setbox{% -{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi -} -\rail@vloval -} - -\def\rail@rtoken#1[#2]{ -\rail@setbox{% -{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi -} -\rail@vroval -} - -\def\rail@ctoken#1[#2]{ -\rail@setbox{% -{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi -} -\rail@coval -} - -\def\rail@lctoken#1[#2]{ -\rail@setbox{% -{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi -} -\rail@vlcoval -} - -\def\rail@rctoken#1[#2]{ -\rail@setbox{% -{\rail@termfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi -} -\rail@vrcoval -} - -\def\rail@nont#1[#2]{ -\rail@setbox{% -{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi -} -\rail@frame -} - -\def\rail@lnont#1[#2]{ -\rail@setbox{% -{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi -} -\rail@vlframe -} - -\def\rail@rnont#1[#2]{ -\rail@setbox{% -{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi -} -\rail@vrframe -} - -\def\rail@cnont#1[#2]{ -\rail@setbox{% -{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi -} -\rail@cframe -} - -\def\rail@lcnont#1[#2]{ -\rail@setbox{% -{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi -} -\rail@vlcframe -} - -\def\rail@rcnont#1[#2]{ -\rail@setbox{% -{\rail@nontfont \rail@expand{#1}}\ifx\@empty#2\else\ {\rail@annofont #2}\fi -} -\rail@vrcframe -} - -\def\rail@term#1[#2]{ -\rail@setbox{% -{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi -} -\rail@oval -} - -\def\rail@lterm#1[#2]{ -\rail@setbox{% -{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi -} -\rail@vloval -} - -\def\rail@rterm#1[#2]{ -\rail@setbox{% -{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi -} -\rail@vroval -} - -\def\rail@cterm#1[#2]{ -\rail@setbox{% -{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi -} -\rail@coval -} - -\def\rail@lcterm#1[#2]{ -\rail@setbox{% -{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi -} -\rail@vlcoval -} - -\def\rail@rcterm#1[#2]{ -\rail@setbox{% -{\rail@termfont #1}\ifx\@empty#2\else\ {\rail@annofont #2}\fi -} -\rail@vrcoval -} - -\def\rail@annote[#1]{ -\rail@setbox{\rail@annofont #1} -\rail@text -} - -% \rail@box : temporary box for \rail@oval and \rail@frame -% -% \rail@setbox{TEXT} : set \rail@box to TEXT, set \rail@tmpa to width -% -% \rail@oval : format \rail@box of width \rail@tmpa inside an oval -% \rail@vloval : format \rail@box of width \rail@tmpa inside an oval, vector left -% \rail@vroval : format \rail@box of width \rail@tmpa inside an oval, vector right -% -% \rail@coval : same as \rail@oval, but centered between \rail@x and -% \rail@mx -% \rail@vlcoval : same as \rail@oval, but centered between \rail@x and -% \rail@mx, vector left -% \rail@vrcoval : same as \rail@oval, but centered between \rail@x and -% \rail@mx, vector right -% -% \rail@frame : format \rail@box of width \rail@tmpa inside a frame -% \rail@vlframe : format \rail@box of width \rail@tmpa inside a frame, vector left -% \rail@vrframe : format \rail@box of width \rail@tmpa inside a frame, vector right -% -% \rail@cframe : same as \rail@frame, but centered between \rail@x and -% \rail@mx -% \rail@vlcframe : same as \rail@frame, but centered between \rail@x and -% \rail@mx, vector left -% \rail@vrcframe : same as \rail@frame, but centered between \rail@x and -% \rail@mx, vector right -% -% \rail@text : format \rail@box of width \rail@tmpa above the line - -\newbox\rail@box - -\def\rail@setbox#1{ -\setbox\rail@box\hbox{\strut#1} -\rail@tmpa=\wd\rail@box -\divide\rail@tmpa by \railunit -} - -\def\rail@oval{ -\advance\rail@x by \rail@boxlf -\rail@eline -\advance\rail@tmpa by \rail@ovalsp -\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi -\rail@tmpb=\rail@tmpa -\divide\rail@tmpb by 2 -\advance\rail@y by -\rail@boxhht -\rail@put{\makebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}} -\advance\rail@y by \rail@boxhht -\advance\rail@x by \rail@tmpb -\rail@put{\oval(\number\rail@tmpa,\number\rail@boxht)} -\advance\rail@x by \rail@tmpb -\rail@ex=\rail@x -\advance\rail@x by \rail@boxrt -} - -\def\rail@vloval{ -\advance\rail@x by \rail@boxlf -\rail@eline -\advance\rail@tmpa by \rail@ovalsp -\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi -\rail@tmpb=\rail@tmpa -\divide\rail@tmpb by 2 -\advance\rail@y by -\rail@boxhht -\rail@put{\makebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}} -\advance\rail@y by \rail@boxhht -\advance\rail@x by \rail@tmpb -\rail@put{\oval(\number\rail@tmpa,\number\rail@boxht)} -\advance\rail@x by \rail@tmpb -\rail@ex=\rail@x -\advance\rail@x by \rail@boxrt -\rail@vleline -} - -\def\rail@vroval{ -\advance\rail@x by \rail@boxlf -\rail@vreline -\advance\rail@tmpa by \rail@ovalsp -\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi -\rail@tmpb=\rail@tmpa -\divide\rail@tmpb by 2 -\advance\rail@y by -\rail@boxhht -\rail@put{\makebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}} -\advance\rail@y by \rail@boxhht -\advance\rail@x by \rail@tmpb -\rail@put{\oval(\number\rail@tmpa,\number\rail@boxht)} -\advance\rail@x by \rail@tmpb -\rail@ex=\rail@x -\advance\rail@x by \rail@boxrt -} - -\def\rail@coval{ -\rail@tmpb=\rail@tmpa -\advance\rail@tmpb by \rail@ovalsp -\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi -\advance\rail@tmpb by \rail@boxlf -\advance\rail@tmpb by \rail@boxrt -\rail@tmpc=\rail@mx -\advance\rail@tmpc by -\rail@x -\advance\rail@tmpc by -\rail@tmpb -\divide\rail@tmpc by 2 -\ifnum\rail@tmpc>0 -\advance\rail@x by \rail@tmpc -\fi -\rail@oval -} - -\def\rail@vlcoval{ -\rail@tmpb=\rail@tmpa -\advance\rail@tmpb by \rail@ovalsp -\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi -\advance\rail@tmpb by \rail@boxlf -\advance\rail@tmpb by \rail@boxrt -\rail@tmpc=\rail@mx -\advance\rail@tmpc by -\rail@x -\advance\rail@tmpc by -\rail@tmpb -\divide\rail@tmpc by 2 -\ifnum\rail@tmpc>0 -\advance\rail@x by \rail@tmpc -\fi -\rail@vloval -} - -\def\rail@vrcoval{ -\rail@tmpb=\rail@tmpa -\advance\rail@tmpb by \rail@ovalsp -\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi -\advance\rail@tmpb by \rail@boxlf -\advance\rail@tmpb by \rail@boxrt -\rail@tmpc=\rail@mx -\advance\rail@tmpc by -\rail@x -\advance\rail@tmpc by -\rail@tmpb -\divide\rail@tmpc by 2 -\ifnum\rail@tmpc>0 -\advance\rail@x by \rail@tmpc -\fi -\rail@vroval -} - -\def\rail@frame{ -\advance\rail@x by \rail@boxlf -\rail@eline -\advance\rail@tmpa by \rail@framesp -\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi -\advance\rail@y by -\rail@boxhht -\rail@put{\framebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}} -\advance\rail@y by \rail@boxhht -\advance\rail@x by \rail@tmpa -\rail@ex=\rail@x -\advance\rail@x by \rail@boxrt -} - -\def\rail@vlframe{ -\advance\rail@x by \rail@boxlf -\rail@eline -\advance\rail@tmpa by \rail@framesp -\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi -\advance\rail@y by -\rail@boxhht -\rail@put{\framebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}} -\advance\rail@y by \rail@boxhht -\advance\rail@x by \rail@tmpa -\rail@ex=\rail@x -\advance\rail@x by \rail@boxrt -\rail@vleline -} - -\def\rail@vrframe{ -\advance\rail@x by \rail@boxlf -\rail@vreline -\advance\rail@tmpa by \rail@framesp -\ifnum\rail@tmpa<\rail@boxht\rail@tmpa=\rail@boxht\fi -\advance\rail@y by -\rail@boxhht -\rail@put{\framebox(\number\rail@tmpa,\number\rail@boxht){\box\rail@box}} -\advance\rail@y by \rail@boxhht -\advance\rail@x by \rail@tmpa -\rail@ex=\rail@x -\advance\rail@x by \rail@boxrt -} - -\def\rail@cframe{ -\rail@tmpb=\rail@tmpa -\advance\rail@tmpb by \rail@framesp -\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi -\advance\rail@tmpb by \rail@boxlf -\advance\rail@tmpb by \rail@boxrt -\rail@tmpc=\rail@mx -\advance\rail@tmpc by -\rail@x -\advance\rail@tmpc by -\rail@tmpb -\divide\rail@tmpc by 2 -\ifnum\rail@tmpc>0 -\advance\rail@x by \rail@tmpc -\fi -\rail@frame -} - -\def\rail@vlcframe{ -\rail@tmpb=\rail@tmpa -\advance\rail@tmpb by \rail@framesp -\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi -\advance\rail@tmpb by \rail@boxlf -\advance\rail@tmpb by \rail@boxrt -\rail@tmpc=\rail@mx -\advance\rail@tmpc by -\rail@x -\advance\rail@tmpc by -\rail@tmpb -\divide\rail@tmpc by 2 -\ifnum\rail@tmpc>0 -\advance\rail@x by \rail@tmpc -\fi -\rail@vlframe -} - -\def\rail@vrcframe{ -\rail@tmpb=\rail@tmpa -\advance\rail@tmpb by \rail@framesp -\ifnum\rail@tmpb<\rail@boxht\rail@tmpb=\rail@boxht\fi -\advance\rail@tmpb by \rail@boxlf -\advance\rail@tmpb by \rail@boxrt -\rail@tmpc=\rail@mx -\advance\rail@tmpc by -\rail@x -\advance\rail@tmpc by -\rail@tmpb -\divide\rail@tmpc by 2 -\ifnum\rail@tmpc>0 -\advance\rail@x by \rail@tmpc -\fi -\rail@vrframe -} - -\def\rail@text{ -\advance\rail@x by \rail@textlf -\advance\rail@y by \rail@textup -\rail@put{\box\rail@box} -\advance\rail@y by -\rail@textup -\advance\rail@x by \rail@tmpa -\advance\rail@x by \rail@textrt -} - -% alternatives -% -% \rail@jx \rail@jy : current join point -% -% \rail@gx \rail@gy \rail@gex \rail@grx : global versions of \rail@x etc, -% to pass values over group closings -% -% \rail@mx : maximum x so far -% -% \rail@sy : starting \rail@y for alternatives -% -% \rail@jput : put at (\rail@jx,\rail@jy) -% -% \rail@joval[PART] : put \oval[PART] with adjust - -\newcount\rail@jx -\newcount\rail@jy - -\newcount\rail@gx -\newcount\rail@gy -\newcount\rail@gex -\newcount\rail@grx - -\newcount\rail@sy -\newcount\rail@mx - -\def\rail@jput{ -\put(\number\rail@jx,\number\rail@jy) -} - -\def\rail@joval[#1]{ -\advance\rail@jx by \rail@joinadj -\rail@jput{\oval(\number\rail@joinsz,\number\rail@joinsz)[#1]} -\advance\rail@jx by -\rail@joinadj -} - -% \rail@barsplit : incoming split for '|' -% -% \rail@plussplit : incoming split for '+' -% - -\def\rail@barsplit{ -\advance\rail@jy by -\rail@joinhsz -\rail@joval[tr] -\advance\rail@jx by \rail@joinhsz -} - -\def\rail@plussplit{ -\advance\rail@jy by -\rail@joinhsz -\advance\rail@jx by \rail@joinsz -\rail@joval[tl] -\advance\rail@jx by -\rail@joinhsz -} - -% \rail@alt{SPLIT} : start alternatives with incoming split SPLIT -% - -\def\rail@alt#1{ -\rail@sy=\rail@y -\rail@jx=\rail@x -\rail@jy=\rail@y -\advance\rail@x by \rail@joinsz -\rail@mx=0 -\let\rail@list=\@empty -\let\rail@comma=\@empty -\let\rail@split=#1 -\begingroup -\rail@sx=\rail@x -\rail@rx=0 -} - -% \rail@nextalt{FIX}{Y} : start next alternative at vertical position Y -% and fix-up FIX -% - -\def\rail@nextalt#1#2{ -\global\rail@gx=\rail@x -\global\rail@gy=\rail@y -\global\rail@gex=\rail@ex -\global\rail@grx=\rail@rx -\endgroup -#1 -\ifnum\rail@gx>\rail@mx\rail@mx=\rail@gx\fi -\ifnum\rail@grx>\rail@mx\rail@mx=\rail@grx\fi -\edef\rail@list{\rail@list\rail@comma\number\rail@gex:\number\rail@gy} -\def\rail@comma{,} -\rail@split -\let\rail@split=\@empty -\rail@sety{#2} -\rail@tmpa=\rail@jy -\advance\rail@tmpa by -\rail@y -\advance\rail@tmpa by -\rail@joinhsz -\rail@jput{\line(0,-1){\number\rail@tmpa}} -\rail@jy=\rail@y -\advance\rail@jy by \rail@joinhsz -\advance\rail@jx by \rail@joinhsz -\rail@joval[bl] -\advance\rail@jx by -\rail@joinhsz -\rail@ex=\rail@x -\begingroup -\rail@sx=\rail@x -\rail@rx=0 -} - -% \rail@barjoin : outgoing join for first '|' alternative -% -% \rail@plusjoin : outgoing join for first '+' alternative -% -% \rail@altjoin : join for subsequent alternative -% - -\def\rail@barjoin{ -\ifnum\rail@y<\rail@sy -\global\rail@gex=\rail@jx -\else -\global\rail@gex=\rail@ex -\fi -\advance\rail@jy by -\rail@joinhsz -\rail@joval[tl] -\advance\rail@jx by -\rail@joinhsz -\ifnum\rail@y<\rail@sy -\rail@altjoin -\fi -} - -\def\rail@plusjoin{ -\global\rail@gex=\rail@ex -\advance\rail@jy by -\rail@joinhsz -\advance\rail@jx by -\rail@joinsz -\rail@joval[tr] -\advance\rail@jx by \rail@joinhsz -} - -\def\rail@altjoin{ -\rail@eline -\rail@tmpa=\rail@jy -\advance\rail@tmpa by -\rail@y -\advance\rail@tmpa by -\rail@joinhsz -\rail@jput{\line(0,-1){\number\rail@tmpa}} -\rail@jy=\rail@y -\advance\rail@jy by \rail@joinhsz -\advance\rail@jx by -\rail@joinhsz -\rail@joval[br] -\advance\rail@jx by \rail@joinhsz -} - -% \rail@eltsplit EX:Y; : split EX:Y into \rail@ex \rail@y -% -% \rail@endalt{JOIN} : end alternatives with outgoing join JOIN - -\def\rail@eltsplit#1:#2;{\rail@ex=#1\rail@y=#2} - -\def\rail@endalt#1{ -\global\rail@gx=\rail@x -\global\rail@gy=\rail@y -\global\rail@gex=\rail@ex -\global\rail@grx=\rail@rx -\endgroup -\ifnum\rail@gx>\rail@mx\rail@mx=\rail@gx\fi -\ifnum\rail@grx>\rail@mx\rail@mx=\rail@grx\fi -\edef\rail@list{\rail@list\rail@comma\number\rail@gex:\number\rail@gy} -\rail@x=\rail@mx -\rail@jx=\rail@x -\rail@jy=\rail@sy -\advance\rail@jx by \rail@joinsz -\let\rail@join=#1 -\@for\rail@elt:=\rail@list\do{ -\expandafter\rail@eltsplit\rail@elt; -\rail@join -\let\rail@join=\rail@altjoin -} -\rail@x=\rail@mx -\rail@y=\rail@sy -\rail@ex=\rail@gex -\advance\rail@x by \rail@joinsz -} - -% \rail@bar : start '|' alternatives -% -% \rail@nextbar : next '|' alternative -% -% \rail@endbar : end '|' alternatives -% - -\def\rail@bar{ -\rail@alt\rail@barsplit -} - -\def\rail@nextbar{ -\rail@nextalt\relax -} - -\def\rail@endbar{ -\rail@endalt\rail@barjoin -} - -% \rail@plus : start '+' alternatives -% -% \rail@nextplus: next '+' alternative -% -% \rail@endplus : end '+' alternatives -% - -\def\rail@plus{ -\rail@alt\rail@plussplit -} - -\def\rail@nextplus{ -\rail@nextalt\rail@fixplus -} - -\def\rail@fixplus{ -\ifnum\rail@gy<\rail@sy -\begingroup -\rail@x=\rail@gx -\rail@y=\rail@gy -\rail@ex=\rail@gex -\rail@rx=\rail@grx -\ifnum\rail@x<\rail@rx -\rail@x=\rail@rx -\fi -\rail@eline -\rail@jx=\rail@x -\rail@jy=\rail@y -\advance\rail@jy by \rail@joinhsz -\rail@joval[br] -\advance\rail@jx by \rail@joinhsz -\rail@tmpa=\rail@sy -\advance\rail@tmpa by -\rail@joinhsz -\advance\rail@tmpa by -\rail@jy -\rail@jput{\line(0,1){\number\rail@tmpa}} -\rail@jy=\rail@sy -\advance\rail@jy by -\rail@joinhsz -\advance\rail@jx by \rail@joinhsz -\rail@joval[tl] -\advance\rail@jy by \rail@joinhsz -\global\rail@gx=\rail@jx -\global\rail@gy=\rail@jy -\global\rail@gex=\rail@gx -\global\rail@grx=\rail@rx -\endgroup -\fi -} - -\def\rail@endplus{ -\rail@endalt\rail@plusjoin -} - -% \rail@cr{Y} : carriage return to vertical position Y - -\def\rail@cr#1{ -\rail@tmpa=\rail@sx -\advance\rail@tmpa by \rail@joinsz -\ifnum\rail@x<\rail@tmpa\rail@x=\rail@tmpa\fi -\rail@eline -\rail@jx=\rail@x -\rail@jy=\rail@y -\advance\rail@x by \rail@joinsz -\ifnum\rail@x>\rail@rx\rail@rx=\rail@x\fi -\advance\rail@jy by -\rail@joinhsz -\rail@joval[tr] -\advance\rail@jx by \rail@joinhsz -\rail@sety{#1} -\rail@tmpa=\rail@jy -\advance\rail@tmpa by -\rail@y -\advance\rail@tmpa by -\rail@boxsp -\advance\rail@tmpa by -\rail@joinhsz -\rail@jput{\line(0,-1){\number\rail@tmpa}} -\rail@jy=\rail@y -\advance\rail@jy by \rail@boxsp -\advance\rail@jy by \rail@joinhsz -\advance\rail@jx by -\rail@joinhsz -\rail@joval[br] -\advance\rail@jy by -\rail@joinhsz -\rail@tmpa=\rail@jx -\advance\rail@tmpa by -\rail@sx -\advance\rail@tmpa by -\rail@joinhsz -\rail@jput{\line(-1,0){\number\rail@tmpa}} -\rail@jx=\rail@sx -\advance\rail@jx by \rail@joinhsz -\advance\rail@jy by -\rail@joinhsz -\rail@joval[tl] -\advance\rail@jx by -\rail@joinhsz -\rail@tmpa=\rail@boxsp -\advance\rail@tmpa by -\rail@joinsz -\rail@jput{\line(0,-1){\number\rail@tmpa}} -\advance\rail@jy by -\rail@tmpa -\advance\rail@jx by \rail@joinhsz -\rail@joval[bl] -\rail@x=\rail@jx -\rail@ex=\rail@x -} - -% default setup for Isabelle -\newenvironment{railoutput}% -{\begin{list}{}{\rail@param}\def\rail@expand{\relax}\makeatletter}{\makeatother\end{list}} - -\def\rail@termfont{\isabellestyle{tt}} -\def\rail@nontfont{\isabellestyle{it}} -\def\rail@namefont{\isabellestyle{it}} diff -r 7f79f94a432c -r 2d17c305f4bc src/HOL/ROOT --- a/src/HOL/ROOT Tue Aug 28 17:16:00 2012 +0200 +++ b/src/HOL/ROOT Tue Aug 28 17:17:03 2012 +0200 @@ -603,8 +603,9 @@ session "HOL-Ordinals_and_Cardinals" in Ordinals_and_Cardinals = "HOL-Ordinals_and_Cardinals-Base" + - options [document = false] + options [document = pdf, document_output = "."] theories Cardinal_Order_Relation + files "document/intro.tex" "document/root.tex" "document/root.bib" session "HOL-Codatatype" in Codatatype = "HOL-Ordinals_and_Cardinals-Base" + options [document = false]