diff --git a/thys/MDP-Algorithms/ROOT b/thys/MDP-Algorithms/ROOT --- a/thys/MDP-Algorithms/ROOT +++ b/thys/MDP-Algorithms/ROOT @@ -1,15 +1,15 @@ chapter AFP session "MDP-Algorithms" (AFP) = "MDP-Rewards" + - options [document = pdf, document_output = "output", timeout = 600] + options [timeout = 600] sessions Gauss_Jordan directories code examples theories Algorithms Code_Mod Examples document_files "root.bib" "root.tex" diff --git a/thys/MDP-Algorithms/output/document.pdf b/thys/MDP-Algorithms/output/document.pdf deleted file mode 100644 index f79aa81fe9ef01b8402802d0652cb0cc4209582b..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 GIT binary patch literal 0 Hc$@\endcsname{} -} -\def\CSgobbleescape#1{\ifnum`\\=`#1 \else #1\fi} -\def\WriteCommentLine#1{\def\CStmp{#1}% - \immediate\write\CommentStream{\CSstringmeaning\CStmp}} - -% 3.1 change: in LaTeX and LaTeX2e prevent grouping -\if 0% -\ifx\fmtname\latexename - 0% -\else \ifx\fmtname\latexname - 0% - \else - 1% -\fi \fi -%%%% -%%%% definitions for LaTeX -%%%% -\def\AfterIncludedComment - {\immediate\closeout\CommentStream - \input{\CommentCutFile}\relax - }% -\def\TossComment{\immediate\closeout\CommentStream} -\def\BeforeIncludedComment - {\immediate\openout\CommentStream=\CommentCutFile - \let\ThisComment\WriteCommentLine} -\def\includecomment - #1{\message{Include comment '#1'}% - \csarg\let{After#1Comment}\AfterIncludedComment - \csarg\def{#1}{\BeforeIncludedComment - \ProcessComment{#1}}% - \CommentEndDef{#1}} -\long\def\specialcomment - #1#2#3{\message{Special comment '#1'}% - % note: \AfterIncludedComment does \input, so #2 goes here! - \csarg\def{After#1Comment}{#2\AfterIncludedComment#3}% - \csarg\def{#1}{\BeforeIncludedComment\relax - \ProcessComment{#1}}% - \CommentEndDef{#1}} -\long\def\processcomment - #1#2#3#4{\message{Lines-Processing comment '#1'}% - \csarg\def{After#1Comment}{#3\AfterIncludedComment#4}% - \csarg\def{#1}{\BeforeIncludedComment#2\relax - \ProcessComment{#1}}% - \CommentEndDef{#1}} -\def\leveledcomment - #1#2{\message{Include comment '#1' up to level '#2'}% - %\csname #1IsLeveledCommenttrue\endcsname - \csarg\let{After#1Comment}\AfterIncludedComment - \csarg\def{#1}{\BeforeIncludedComment - \ProcessCommentWithArg{#1}}% - \CommentEndDef{#1}} -\else -%%%% -%%%%plain TeX and other formats -%%%% -\def\includecomment - #1{\message{Including comment '#1'}% - \csarg\def{#1}{}% - \csarg\def{end#1}{}} -\long\def\specialcomment - #1#2#3{\message{Special comment '#1'}% - \csarg\def{#1}{\def\ThisComment{}\def\AfterComment{#3}#2% - \ProcessComment{#1}}% - \CommentEndDef{#1}} -\fi - -%%%% -%%%% general definition of skipped comment -%%%% -\def\excludecomment - #1{\message{Excluding comment '#1'}% - \csarg\def{#1}{\let\AfterComment\relax - \def\ThisComment####1{}\ProcessComment{#1}}% - \csarg\let{After#1Comment}\TossComment - \CommentEndDef{#1}} - -\if 0% -\ifx\fmtname\latexename - 0% -\else \ifx\fmtname\latexname - 0% - \else - 1% -\fi \fi -% latex & latex2e: -\def\EndOfComment#1{\endgroup\end{#1}% - \csname After#1Comment\endcsname} -\def\CommentEndDef#1{{\escapechar=-1\relax - \csarg\xdef{End#1Test}{\string\\end\string\{#1\string\}}% - }} -\else -% plain & other -\def\EndOfComment#1{\endgroup\AfterComment} -\def\CommentEndDef#1{{\escapechar=-1\relax - \csarg\xdef{End#1Test}{\string\\end#1}% - }} -\fi - -\excludecomment{comment} - -\endinput diff --git a/thys/MDP-Algorithms/output/document/isabelle.sty b/thys/MDP-Algorithms/output/document/isabelle.sty deleted file mode 100644 --- a/thys/MDP-Algorithms/output/document/isabelle.sty +++ /dev/null @@ -1,282 +0,0 @@ -%% -%% macros for Isabelle generated LaTeX output -%% - -%%% Simple document preparation (based on theory token language and symbols) - -% isabelle environments - -\newcommand{\isabellecontext}{UNKNOWN} -\newcommand{\setisabellecontext}[1]{\def\isabellecontext{#1}} - -\newcommand{\isastyle}{\UNDEF} -\newcommand{\isastylett}{\UNDEF} -\newcommand{\isastyleminor}{\UNDEF} -\newcommand{\isastyleminortt}{\UNDEF} -\newcommand{\isastylescript}{\UNDEF} -\newcommand{\isastyletext}{\normalsize\normalfont\rmfamily} -\newcommand{\isastyletxt}{\normalfont\rmfamily} -\newcommand{\isastylecmt}{\normalfont\rmfamily} - -\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}$}} -\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}} - -%blackboard-bold (requires font txmia from pxfonts) -\DeclareSymbolFont{bbbfont}{U}{txmia}{m}{it} -\SetSymbolFont{bbbfont}{bold}{U}{txmia}{bx}{it} -\DeclareMathSymbol{\bbbA}{\mathord}{bbbfont}{129} -\DeclareMathSymbol{\bbbB}{\mathord}{bbbfont}{130} -\DeclareMathSymbol{\bbbC}{\mathord}{bbbfont}{131} -\DeclareMathSymbol{\bbbD}{\mathord}{bbbfont}{132} -\DeclareMathSymbol{\bbbE}{\mathord}{bbbfont}{133} -\DeclareMathSymbol{\bbbF}{\mathord}{bbbfont}{134} -\DeclareMathSymbol{\bbbG}{\mathord}{bbbfont}{135} -\DeclareMathSymbol{\bbbH}{\mathord}{bbbfont}{136} -\DeclareMathSymbol{\bbbI}{\mathord}{bbbfont}{137} -\DeclareMathSymbol{\bbbJ}{\mathord}{bbbfont}{138} -\DeclareMathSymbol{\bbbK}{\mathord}{bbbfont}{139} -\DeclareMathSymbol{\bbbL}{\mathord}{bbbfont}{140} -\DeclareMathSymbol{\bbbM}{\mathord}{bbbfont}{141} -\DeclareMathSymbol{\bbbN}{\mathord}{bbbfont}{142} -\DeclareMathSymbol{\bbbO}{\mathord}{bbbfont}{143} -\DeclareMathSymbol{\bbbP}{\mathord}{bbbfont}{144} -\DeclareMathSymbol{\bbbQ}{\mathord}{bbbfont}{145} -\DeclareMathSymbol{\bbbR}{\mathord}{bbbfont}{146} -\DeclareMathSymbol{\bbbS}{\mathord}{bbbfont}{147} -\DeclareMathSymbol{\bbbT}{\mathord}{bbbfont}{148} -\DeclareMathSymbol{\bbbU}{\mathord}{bbbfont}{149} -\DeclareMathSymbol{\bbbV}{\mathord}{bbbfont}{150} -\DeclareMathSymbol{\bbbW}{\mathord}{bbbfont}{151} -\DeclareMathSymbol{\bbbX}{\mathord}{bbbfont}{152} -\DeclareMathSymbol{\bbbY}{\mathord}{bbbfont}{153} -\DeclareMathSymbol{\bbbZ}{\mathord}{bbbfont}{154} - -\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}} - -\newdimen\isa@parindent\newdimen\isa@parskip - -\newenvironment{isabellebody}{% -\isamarkuptrue\par% -\isa@parindent\parindent\parindent0pt% -\isa@parskip\parskip\parskip0pt% -\isaspacing\isastyle}{\par} - -\newenvironment{isabellebodytt}{% -\isamarkuptrue\par% -\isa@parindent\parindent\parindent0pt% -\isa@parskip\parskip\parskip0pt% -\isaspacing\isastylett}{\par} - -\newenvironment{isabelle} -{\begin{trivlist}\begin{isabellebody}\item\relax} -{\end{isabellebody}\end{trivlist}} - -\newenvironment{isabellett} -{\begin{trivlist}\begin{isabellebodytt}\item\relax} -{\end{isabellebodytt}\end{trivlist}} - -\newcommand{\isa}[1]{\emph{\isaspacing\isastyleminor #1}} -\newcommand{\isatt}[1]{\emph{\isaspacing\isastyleminortt #1}} - -\newcommand{\isaindent}[1]{\hphantom{#1}} -\newcommand{\isanewline}{\mbox{}\par\mbox{}} -\newcommand{\isasep}{} -\newcommand{\isadigit}[1]{#1} - -\newcommand{\isachardefaults}{% -\def\isacharbell{\isamath{\bigbox}}%requires stmaryrd -\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}% -\def\isacartoucheopen{\isatext{\guilsinglleft}}% -\def\isacartoucheclose{\isatext{\guilsinglright}}% -} - - -% keyword and section markup - -\newcommand{\isakeyword}[1] -{\emph{\normalfont\bfseries\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}% -\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}} -\newcommand{\isacommand}[1]{\isakeyword{#1}} - -\newcommand{\isakeywordcontrol}[1] -{\emph{\normalfont\bfseries\itshape\def\isacharunderscore{\isacharunderscorekeyword}#1\,}} - -\newcommand{\isamarkupchapter}[1]{\chapter{#1}} -\newcommand{\isamarkupsection}[1]{\section{#1}} -\newcommand{\isamarkupsubsection}[1]{\subsection{#1}} -\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}} -\newcommand{\isamarkupparagraph}[1]{\paragraph{#1}} -\newcommand{\isamarkupsubparagraph}[1]{\subparagraph{#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}} - - -% index entries - -\newcommand{\isaindexdef}[1]{\textbf{#1}} -\newcommand{\isaindexref}[1]{#1} - - -% styles - -\def\isabellestyle#1{\csname isabellestyle#1\endcsname} - -\newcommand{\isabellestyledefault}{% -\def\isastyle{\small\normalfont\ttfamily\slshape}% -\def\isastylett{\small\normalfont\ttfamily}% -\def\isastyleminor{\small\normalfont\ttfamily\slshape}% -\def\isastyleminortt{\small\normalfont\ttfamily}% -\def\isastylescript{\footnotesize\normalfont\ttfamily\slshape}% -\isachardefaults% -} -\isabellestyledefault - -\newcommand{\isabellestylett}{% -\def\isastyle{\small\normalfont\ttfamily}% -\def\isastylett{\small\normalfont\ttfamily}% -\def\isastyleminor{\small\normalfont\ttfamily}% -\def\isastyleminortt{\small\normalfont\ttfamily}% -\def\isastylescript{\footnotesize\normalfont\ttfamily}% -\isachardefaults% -} - -\newcommand{\isabellestyleit}{% -\def\isastyle{\small\normalfont\itshape}% -\def\isastylett{\small\normalfont\ttfamily}% -\def\isastyleminor{\normalfont\itshape}% -\def\isastyleminortt{\normalfont\ttfamily}% -\def\isastylescript{\footnotesize\normalfont\itshape}% -\isachardefaults% -\def\isacharunderscorekeyword{\mbox{-}}% -\def\isacharbang{\isamath{!}}% -\def\isachardoublequote{}% -\def\isachardoublequoteopen{}% -\def\isachardoublequoteclose{}% -\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{\guilsinglleft}}% -\def\isacharbackquoteclose{\isatext{\guilsinglright}}% -} - -\newcommand{\isabellestyleliteral}{% -\isabellestyleit% -\def\isacharunderscore{\_}% -\def\isacharunderscorekeyword{\_}% -\chardef\isacharbackquoteopen=`\`% -\chardef\isacharbackquoteclose=`\`% -} - -\newcommand{\isabellestyleliteralunderscore}{% -\isabellestyleliteral% -\def\isacharunderscore{\textunderscore}% -\def\isacharunderscorekeyword{\textunderscore}% -} - -\newcommand{\isabellestylesl}{% -\isabellestyleit% -\def\isastyle{\small\normalfont\slshape}% -\def\isastylett{\small\normalfont\ttfamily}% -\def\isastyleminor{\normalfont\slshape}% -\def\isastyleminortt{\normalfont\ttfamily}% -\def\isastylescript{\footnotesize\normalfont\slshape}% -} - - -% cancel text - -\usepackage[normalem]{ulem} -\newcommand{\isamarkupcancel}[1]{\isa{\xout{#1}}} - - -% tags - -\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}} - -\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{} diff --git a/thys/MDP-Algorithms/output/document/isabellesym.sty b/thys/MDP-Algorithms/output/document/isabellesym.sty deleted file mode 100644 --- a/thys/MDP-Algorithms/output/document/isabellesym.sty +++ /dev/null @@ -1,496 +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{\isasymbbbA}{\isamath{\bbbA}} %requires font txmia from txfonts -\newcommand{\isasymbool}{\isamath{\bbbB}} %requires font txmia from txfonts -\newcommand{\isasymcomplex}{\isamath{\bbbC}} %requires font txmia from txfonts -\newcommand{\isasymbbbD}{\isamath{\bbbD}} %requires font txmia from txfonts -\newcommand{\isasymbbbE}{\isamath{\bbbE}} %requires font txmia from txfonts -\newcommand{\isasymbbbF}{\isamath{\bbbF}} %requires font txmia from txfonts -\newcommand{\isasymbbbG}{\isamath{\bbbG}} %requires font txmia from txfonts -\newcommand{\isasymbbbH}{\isamath{\bbbH}} %requires font txmia from txfonts -\newcommand{\isasymbbbI}{\isamath{\bbbI}} %requires font txmia from txfonts -\newcommand{\isasymbbbJ}{\isamath{\bbbJ}} %requires font txmia from txfonts -\newcommand{\isasymbbbK}{\isamath{\bbbK}} %requires font txmia from txfonts -\newcommand{\isasymbbbL}{\isamath{\bbbL}} %requires font txmia from txfonts -\newcommand{\isasymbbbM}{\isamath{\bbbM}} %requires font txmia from txfonts -\newcommand{\isasymnat}{\isamath{\bbbN}} %requires font txmia from txfonts -\newcommand{\isasymbbbO}{\isamath{\bbbO}} %requires font txmia from txfonts -\newcommand{\isasymbbbP}{\isamath{\bbbP}} %requires font txmia from txfonts -\newcommand{\isasymrat}{\isamath{\bbbQ}} %requires font txmia from txfonts -\newcommand{\isasymreal}{\isamath{\bbbR}} %requires font txmia from txfonts -\newcommand{\isasymbbbS}{\isamath{\bbbS}} %requires font txmia from txfonts -\newcommand{\isasymbbbT}{\isamath{\bbbT}} %requires font txmia from txfonts -\newcommand{\isasymbbbU}{\isamath{\bbbU}} %requires font txmia from txfonts -\newcommand{\isasymbbbV}{\isamath{\bbbV}} %requires font txmia from txfonts -\newcommand{\isasymbbbW}{\isamath{\bbbW}} %requires font txmia from txfonts -\newcommand{\isasymbbbX}{\isamath{\bbbX}} %requires font txmia from txfonts -\newcommand{\isasymbbbY}{\isamath{\bbbY}} %requires font txmia from txfonts -\newcommand{\isasymint}{\isamath{\bbbZ}} %requires font txmia from txfonts -\newcommand{\isasymleftarrow}{\isamath{\leftarrow}} -\newcommand{\isasymrightarrow}{\isamath{\rightarrow}} -\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}} -\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}} -\newcommand{\isasymlonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAA}}}} %requires amsmath -\newcommand{\isasymlonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAA}}}} %requires amsmath -\newcommand{\isasymlonglonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAAA}}}} %requires amsmath -\newcommand{\isasymlonglonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAAA}}}} %requires amsmath -\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}} -\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}} -\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}} -\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}} -\newcommand{\isasymLleftarrow}{\isamath{\Lleftarrow}} %requires amssymb -\newcommand{\isasymRrightarrow}{\isamath{\Rrightarrow}} %requires amssymb -\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}} -\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}} -\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}} -\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{\isasymllangle}{\isamath{\langle\mskip-5mu\langle}} -\newcommand{\isasymrrangle}{\isamath{\rangle\mskip-5mu\rangle}} -\newcommand{\isasymlceil}{\isamath{\lceil}} -\newcommand{\isasymrceil}{\isamath{\rceil}} -\newcommand{\isasymlfloor}{\isamath{\lfloor}} -\newcommand{\isasymrfloor}{\isamath{\rfloor}} -\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3.3mu\mid}}} -\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3.3mu)}}} -\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}} -\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}} -\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.3mu\mid}}} -\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.3mu\rbrace}}} -\newcommand{\isasymlblot}{\isamath{{\langle}\mkern -3.5mu{|}}} -\newcommand{\isasymrblot}{\isamath{{|}\mkern -3.5mu{\rangle}}} -\newcommand{\isasymguillemotleft}{\isatext{\guillemotleft}} -\newcommand{\isasymguillemotright}{\isatext{\guillemotright}} -\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{\isasymnot}{\isamath{\neg}} -\newcommand{\isasymnexists}{\isamath{\nexists\,}} %requires amssymb -\newcommand{\isasymcircle}{\isamath{\ocircle}} %requires wasysym -\newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb -\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb -\newcommand{\isasymdiamondop}{\isamath{\diamond}} -\newcommand{\isasymsurd}{\isamath{\surd}} -\newcommand{\isasymturnstile}{\isamath{\vdash}} -\newcommand{\isasymTurnstile}{\isamath{\models}} -\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}} -\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}} -\newcommand{\isasymstileturn}{\isamath{\dashv}} -\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{\isasymParallel}{\isamath{\bigparallel}} %requires stmaryrd -\newcommand{\isasyminterleace}{\isamath{\interleave}} %requires stmaryrd -\newcommand{\isasymsslash}{\isamath{\sslash}} %requires stmaryrd -\newcommand{\isasymbar}{\isamath{\mid}} -\newcommand{\isasymbbar}{\isamath{[\mskip-1.5mu]}} -\newcommand{\isasymplusminus}{\isamath{\pm}} -\newcommand{\isasymminusplus}{\isamath{\mp}} -\newcommand{\isasymtimes}{\isamath{\times}} -\newcommand{\isasymdiv}{\isamath{\div}} -\newcommand{\isasymcdot}{\isamath{\cdot}} -\newcommand{\isasymsqdot}{\isamath{\sbox\z@{$\centerdot$}\ht\z@=.33333\ht\z@\vcenter{\box\z@}}} %requires amssymb -\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{\normalfont\rmfamily\copyright}} -\newcommand{\isasymregistered}{\isatext{\normalfont\rmfamily\textregistered}} -\newcommand{\isasyminverse}{\isamath{{}^{-1}}} -\newcommand{\isasymonequarter}{\isatext{\normalfont\rmfamily\textonequarter}} %requires textcomp -\newcommand{\isasymonehalf}{\isatext{\normalfont\rmfamily\textonehalf}} %requires textcomp -\newcommand{\isasymthreequarters}{\isatext{\normalfont\rmfamily\textthreequarters}} %requires textcomp -\newcommand{\isasymordfeminine}{\isatext{\normalfont\rmfamily\textordfeminine}} -\newcommand{\isasymordmasculine}{\isatext{\normalfont\rmfamily\textordmasculine}} -\newcommand{\isasymsection}{\isatext{\normalfont\rmfamily\S}} -\newcommand{\isasymparagraph}{\isatext{\normalfont\rmfamily\P}} -\newcommand{\isasymexclamdown}{\isatext{\normalfont\rmfamily\textexclamdown}} -\newcommand{\isasymquestiondown}{\isatext{\normalfont\rmfamily\textquestiondown}} -\newcommand{\isasymeuro}{\isatext{\euro}} %requires eurosym -\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{\normalfont\rmfamily\textdegree}} %requires textcomp -\newcommand{\isasymhyphen}{\isatext{\normalfont\rmfamily-}} -\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{\isasymacute}{\isatext{\'\relax}} -\newcommand{\isasymindex}{\isatext{\i}} -\newcommand{\isasymdieresis}{\isatext{\"\relax}} -\newcommand{\isasymcedilla}{\isatext{\c\relax}} -\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}} -\newcommand{\isasymsome}{\isamath{\epsilon\,}} -\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}} -\newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}} - -%Z notation -\newcommand{\isaZhbar}[1]{\rlap{\raise.0001ex\hbox{\isamath{-}}}#1} -\newcommand{\isaZpvbar}[1]{\ooalign{\hfil\isamath{\mapstochar\mkern 5mu}\hfil\cr#1}} -\newcommand{\isaZfvbar}[1]{\ooalign{\hfil\isamath{\mapstochar\mkern 3mu\mapstochar\mkern 5mu}\hfil\cr#1}} -\newcommand{\isaZdarrow}[3]{\ooalign{\isamath{#1}\hfil\cr\isamath{\mkern#3mu\isamath{#2}}}} -\newcommand{\isasymZcomp}{\isamath{\fatsemi}} %requires stmaryrd -\newcommand{\isasymZinj}{\isamath{\rightarrowtail}} %requires amssymb -\newcommand{\isasymZpinj}{\isaZpvbar{\isamath{\rightarrowtail}}} %requires amssymb -\newcommand{\isasymZfinj}{\isaZfvbar{\isasymZinj}} %requires amssymb -\newcommand{\isasymZsurj}{\isaZdarrow{\rightarrow}{\rightarrow}{4}} %requires amssymb -\newcommand{\isasymZpsurj}{\isaZpvbar{\isasymZsurj}} %requires amssymb -\newcommand{\isasymZbij}{\isaZdarrow{\rightarrowtail}{\rightarrow}{5}} %requires amssymb -\newcommand{\isasymZpfun}{\isaZpvbar{\isamath{\rightarrow}}} -\newcommand{\isasymZffun}{\isaZfvbar{\isamath{\rightarrow}}} -\newcommand{\isasymZdres}{\isamath{\lhd}} %requires amssymb -\newcommand{\isasymZndres}{\isaZhbar{\isamath{\lhd}}} %requires amssymb -\newcommand{\isasymZrres}{\isamath{\rhd}} %requires amssymb -\newcommand{\isasymZnrres}{\isaZhbar{\isamath{\rhd}}} %requires amssymb -\newcommand{\isasymZspot}{\isamath{\bullet}} -\newcommand{\isasymZproject}{\isamath{\upharpoonright}} %requires amssymb -\newcommand{\isasymZsemi}{\isatext{\raise 0.66ex\hbox{\oalign{\hfil\isamath{\scriptscriptstyle\mathrm{o}}\hfil\cr\hfil\isamath{\scriptscriptstyle\mathrm{9}}\hfil}}}} -\newcommand{\isasymZtypecolon}{\isatext{\raise 0.6ex\hbox{\oalign{\hfil\isamath{\scriptscriptstyle\mathrm{o}}\hfil\cr\hfil\isamath{\scriptscriptstyle\mathrm{o}}\hfil}}}} -\newcommand{\isasymZhide}{\isamath{\backslash}} -\newcommand{\isasymZcat}{\isatext{\raise 0.8ex\hbox{\isamath{\mathchar\frown}}}} -\newcommand{\isasymZinbag}{\isatext{\ooalign{\isamath{\sqsubset\mkern-1mu}\cr\isamath{-\mkern-1mu}\cr}}} - -\newcommand{\isasymhole}{\isatext{\normalfont\rmfamily\wasylozenge}} %requires wasysym -\newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}} -\newcommand{\isasymcomment}{\isatext{\isastylecmt---}} -\newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}} -\newcommand{\isasymopen}{\isatext{\guilsinglleft}} -\newcommand{\isasymclose}{\isatext{\guilsinglright}} -\newcommand{\isasymcheckmark}{\isatext{\ding{51}}} %requires pifont -\newcommand{\isasymcrossmark}{\isatext{\ding{55}}} %requires pifont -\newcommand{\isactrlmarker}{\isatext{\ding{48}}} %requires pifont -\newcommand{\isactrltry}{\isakeywordcontrol{try}} -\newcommand{\isactrlcan}{\isakeywordcontrol{can}} -\newcommand{\isactrlassert}{\isakeywordcontrol{assert}} -\newcommand{\isactrlcancel}{\isakeywordcontrol{cancel}} -\newcommand{\isactrlbinding}{\isakeywordcontrol{binding}} -\newcommand{\isactrlclass}{\isakeywordcontrol{class}} -\newcommand{\isactrlclassUNDERSCOREsyntax}{\isakeywordcontrol{class{\isacharunderscore}syntax}} -\newcommand{\isactrlcommandUNDERSCOREkeyword}{\isakeywordcontrol{command{\isacharunderscore}keyword}} -\newcommand{\isactrlconst}{\isakeywordcontrol{const}} -\newcommand{\isactrlconstUNDERSCOREabbrev}{\isakeywordcontrol{const{\isacharunderscore}abbrev}} -\newcommand{\isactrlconstUNDERSCOREname}{\isakeywordcontrol{const{\isacharunderscore}name}} -\newcommand{\isactrlconstUNDERSCOREsyntax}{\isakeywordcontrol{const{\isacharunderscore}syntax}} -\newcommand{\isactrlcontext}{\isakeywordcontrol{context}} -\newcommand{\isactrlcprop}{\isakeywordcontrol{cprop}} -\newcommand{\isactrlcterm}{\isakeywordcontrol{cterm}} -\newcommand{\isactrlctyp}{\isakeywordcontrol{ctyp}} -\newcommand{\isactrldir}{\isakeywordcontrol{dir}} -\newcommand{\isactrlfile}{\isakeywordcontrol{file}} -\newcommand{\isactrlhere}{\isakeywordcontrol{here}} -\newcommand{\isactrlinstantiate}{\isakeywordcontrol{instantiate}} -\newcommand{\isactrlkeyword}{\isakeywordcontrol{keyword}} -\newcommand{\isactrllatex}{\isakeywordcontrol{latex}} -\newcommand{\isactrllocale}{\isakeywordcontrol{locale}} -\newcommand{\isactrlmakeUNDERSCOREjudgment}{\isakeywordcontrol{make{\isacharunderscore}judgment}} -\newcommand{\isactrldestUNDERSCOREjudgment}{\isakeywordcontrol{dest{\isacharunderscore}judgment}} -\newcommand{\isactrlmakeUNDERSCOREstring}{\isakeywordcontrol{make{\isacharunderscore}string}} -\newcommand{\isactrlmasterUNDERSCOREdir}{\isakeywordcontrol{master{\isacharunderscore}dir}} -\newcommand{\isactrlmethod}{\isakeywordcontrol{method}} -\newcommand{\isactrlnamedUNDERSCOREtheorems}{\isakeywordcontrol{named{\isacharunderscore}theorems}} -\newcommand{\isactrlnonterminal}{\isakeywordcontrol{nonterminal}} -\newcommand{\isactrloracleUNDERSCOREname}{\isakeywordcontrol{oracle{\isacharunderscore}name}} -\newcommand{\isactrlpath}{\isakeywordcontrol{path}} -\newcommand{\isactrlpathUNDERSCOREbinding}{\isakeywordcontrol{path{\isacharunderscore}binding}} -\newcommand{\isactrlplugin}{\isakeywordcontrol{plugin}} -\newcommand{\isactrlprint}{\isakeywordcontrol{print}} -\newcommand{\isactrlprop}{\isakeywordcontrol{prop}} -\newcommand{\isactrlscala}{\isakeywordcontrol{scala}} -\newcommand{\isactrlscalaUNDERSCOREfunction}{\isakeywordcontrol{scala{\isacharunderscore}function}} -\newcommand{\isactrlscalaUNDERSCOREmethod}{\isakeywordcontrol{scala{\isacharunderscore}method}} -\newcommand{\isactrlscalaUNDERSCOREobject}{\isakeywordcontrol{scala{\isacharunderscore}object}} -\newcommand{\isactrlscalaUNDERSCOREtype}{\isakeywordcontrol{scala{\isacharunderscore}type}} -\newcommand{\isactrlsimproc}{\isakeywordcontrol{simproc}} -\newcommand{\isactrlsort}{\isakeywordcontrol{sort}} -\newcommand{\isactrlsyntaxUNDERSCOREconst}{\isakeywordcontrol{syntax{\isacharunderscore}const}} -\newcommand{\isactrlsystemUNDERSCOREoption}{\isakeywordcontrol{system{\isacharunderscore}option}} -\newcommand{\isactrlterm}{\isakeywordcontrol{term}} -\newcommand{\isactrltheory}{\isakeywordcontrol{theory}} -\newcommand{\isactrltheoryUNDERSCOREcontext}{\isakeywordcontrol{theory{\isacharunderscore}context}} -\newcommand{\isactrltyp}{\isakeywordcontrol{typ}} -\newcommand{\isactrltypeUNDERSCOREabbrev}{\isakeywordcontrol{type{\isacharunderscore}abbrev}} -\newcommand{\isactrltypeUNDERSCOREname}{\isakeywordcontrol{type{\isacharunderscore}name}} -\newcommand{\isactrltypeUNDERSCOREsyntax}{\isakeywordcontrol{type{\isacharunderscore}syntax}} -\newcommand{\isactrlundefined}{\isakeywordcontrol{undefined}} -\newcommand{\isactrltvar}{\isakeywordcontrol{tvar}} -\newcommand{\isactrlvar}{\isakeywordcontrol{var}} -\newcommand{\isactrlConst}{\isakeywordcontrol{Const}} -\newcommand{\isactrlConstUNDERSCORE}{\isakeywordcontrol{Const{\isacharunderscore}}} -\newcommand{\isactrlConstUNDERSCOREfn}{\isakeywordcontrol{Const{\isacharunderscore}fn}} -\newcommand{\isactrlType}{\isakeywordcontrol{Type}} -\newcommand{\isactrlTypeUNDERSCOREfn}{\isakeywordcontrol{Type{\isacharunderscore}fn}} - -\newcommand{\isactrlcode}{\isakeywordcontrol{code}} -\newcommand{\isactrlcomputation}{\isakeywordcontrol{computation}} -\newcommand{\isactrlcomputationUNDERSCOREconv}{\isakeywordcontrol{computation{\isacharunderscore}conv}} -\newcommand{\isactrlcomputationUNDERSCOREcheck}{\isakeywordcontrol{computation{\isacharunderscore}check}} -\newcommand{\isactrlifUNDERSCORElinux}{\isakeywordcontrol{if{\isacharunderscore}linux}} -\newcommand{\isactrlifUNDERSCOREmacos}{\isakeywordcontrol{if{\isacharunderscore}macos}} -\newcommand{\isactrlifUNDERSCOREwindows}{\isakeywordcontrol{if{\isacharunderscore}windows}} -\newcommand{\isactrlifUNDERSCOREunix}{\isakeywordcontrol{if{\isacharunderscore}unix}} diff --git a/thys/MDP-Algorithms/output/document/isabelletags.sty b/thys/MDP-Algorithms/output/document/isabelletags.sty deleted file mode 100644 --- a/thys/MDP-Algorithms/output/document/isabelletags.sty +++ /dev/null @@ -1,20 +0,0 @@ -%plain TeX version of comment package -- much faster! -\let\isafmtname\fmtname\def\fmtname{plain} -\usepackage{comment} -\let\fmtname\isafmtname - -\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{ML} -\isakeeptag{document} -\isakeeptag{important} -\isadroptag{invisible} -\isakeeptag{proof} -\isakeeptag{theory} -\isakeeptag{unimportant} -\isakeeptag{visible} diff --git a/thys/MDP-Algorithms/output/document/pdfsetup.sty b/thys/MDP-Algorithms/output/document/pdfsetup.sty deleted file mode 100644 --- a/thys/MDP-Algorithms/output/document/pdfsetup.sty +++ /dev/null @@ -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,urlcolor=linkcolor,pdfpagelabels]{hyperref} diff --git a/thys/MDP-Algorithms/output/document/railsetup.sty b/thys/MDP-Algorithms/output/document/railsetup.sty deleted file mode 100644 --- a/thys/MDP-Algorithms/output/document/railsetup.sty +++ /dev/null @@ -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 --git a/thys/MDP-Algorithms/output/document/root.bib b/thys/MDP-Algorithms/output/document/root.bib deleted file mode 100644 --- a/thys/MDP-Algorithms/output/document/root.bib +++ /dev/null @@ -1,13 +0,0 @@ -@book{Puterman, - author = {Martin L. Puterman}, - title = {Markov Decision Processes: Discrete Stochastic Dynamic Programming}, - series = {Wiley Series in Probability and Statistics}, - publisher = {Wiley}, - year = {1994}, - url = {https://doi.org/10.1002/9780470316887}, - doi = {10.1002/9780470316887}, - isbn = {978-0-47161977-2}, - timestamp = {Mon, 22 Jul 2019 15:00:49 +0200}, - biburl = {https://dblp.org/rec/books/wi/Puterman94.bib}, - bibsource = {dblp computer science bibliography, https://dblp.org} -} diff --git a/thys/MDP-Algorithms/output/document/root.tex b/thys/MDP-Algorithms/output/document/root.tex deleted file mode 100644 --- a/thys/MDP-Algorithms/output/document/root.tex +++ /dev/null @@ -1,69 +0,0 @@ -\documentclass[11pt,a4paper]{article} -\usepackage{isabelle,isabellesym} - -% further packages required for unusual symbols (see also -% isabellesym.sty), use only when needed - -\usepackage{amssymb, amsmath, amsfonts} - %for \, \, \, \, \, \, - %\, \, \, \, \, - %\, \, \ - -%\usepackage{eurosym} - %for \ - -\usepackage[only,bigsqcap]{stmaryrd} - %for \ - -%\usepackage{eufrak} - %for \ ... \, \ ... \ (also included in amssymb) - -%\usepackage{textcomp} - %for \, \, \, \, \, - %\ - -% this should be the last package used -\usepackage{pdfsetup} - -% urls in roman style, theory text in math-similar italics -\urlstyle{rm} -\isabellestyle{it} - -% for uniform font size -%\renewcommand{\isastyle}{\isastyleminor} - - -\begin{document} - -\title{Verified Algorithms for Solving Markov Decision Processes} -\author{Maximilian Schäffeler and Mohammad Abdulaziz} -\maketitle - -\abstract{ -We present a formalization of algorithms for solving Markov Decision Processes (MDPs) with formal guarantees on the optimality of their -solutions. -In particular we build on our analysis of the Bellman operator for discounted infinite horizon MDPs. -From the iterator rule on the Bellman operator we directly derive executable value iteration and policy iteration algorithms to iteratively solve finite MDPs. -We also prove correct optimized versions of value iteration that use matrix splittings to improve the convergence rate. In particular, we formally verify Gauss-Seidel value iteration and modified policy iteration. -The algorithms are evaluated on two standard examples from the literature, namely, inventory management and gridworld. -Our formalization covers most of chapter 6 in Puterman's book \cite{Puterman}. -} - -\tableofcontents - -% sane default for proof documents -\parindent 0pt\parskip 0.5ex - -% generated text of all theories -\input{session} - -% optional bibliography -\bibliographystyle{abbrv} -\bibliography{root} - -\end{document} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: t -%%% End: diff --git a/thys/MDP-Algorithms/output/document/session.tex b/thys/MDP-Algorithms/output/document/session.tex deleted file mode 100644 --- a/thys/MDP-Algorithms/output/document/session.tex +++ /dev/null @@ -1,13 +0,0 @@ -\input{Value_Iteration.tex} -\input{Policy_Iteration.tex} -\input{Modified_Policy_Iteration.tex} -\input{Matrix_Util.tex} -\input{Blinfun_Matrix.tex} -\input{Splitting_Methods.tex} -\input{Algorithms.tex} -\input{Code_DP.tex} -\input{Code_Mod.tex} -\input{Code_Real_Approx_By_Float_Fix.tex} -\input{Code_Inventory.tex} -\input{Code_Gridworld.tex} -\input{Examples.tex} diff --git a/thys/MDP-Algorithms/output/document/session_graph.pdf b/thys/MDP-Algorithms/output/document/session_graph.pdf deleted file mode 100644 index b03b483f5536b1b7b1f0209d0e8065bb41570191..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 GIT binary patch literal 0 Hc$@\endcsname{} -} -\def\CSgobbleescape#1{\ifnum`\\=`#1 \else #1\fi} -\def\WriteCommentLine#1{\def\CStmp{#1}% - \immediate\write\CommentStream{\CSstringmeaning\CStmp}} - -% 3.1 change: in LaTeX and LaTeX2e prevent grouping -\if 0% -\ifx\fmtname\latexename - 0% -\else \ifx\fmtname\latexname - 0% - \else - 1% -\fi \fi -%%%% -%%%% definitions for LaTeX -%%%% -\def\AfterIncludedComment - {\immediate\closeout\CommentStream - \input{\CommentCutFile}\relax - }% -\def\TossComment{\immediate\closeout\CommentStream} -\def\BeforeIncludedComment - {\immediate\openout\CommentStream=\CommentCutFile - \let\ThisComment\WriteCommentLine} -\def\includecomment - #1{\message{Include comment '#1'}% - \csarg\let{After#1Comment}\AfterIncludedComment - \csarg\def{#1}{\BeforeIncludedComment - \ProcessComment{#1}}% - \CommentEndDef{#1}} -\long\def\specialcomment - #1#2#3{\message{Special comment '#1'}% - % note: \AfterIncludedComment does \input, so #2 goes here! - \csarg\def{After#1Comment}{#2\AfterIncludedComment#3}% - \csarg\def{#1}{\BeforeIncludedComment\relax - \ProcessComment{#1}}% - \CommentEndDef{#1}} -\long\def\processcomment - #1#2#3#4{\message{Lines-Processing comment '#1'}% - \csarg\def{After#1Comment}{#3\AfterIncludedComment#4}% - \csarg\def{#1}{\BeforeIncludedComment#2\relax - \ProcessComment{#1}}% - \CommentEndDef{#1}} -\def\leveledcomment - #1#2{\message{Include comment '#1' up to level '#2'}% - %\csname #1IsLeveledCommenttrue\endcsname - \csarg\let{After#1Comment}\AfterIncludedComment - \csarg\def{#1}{\BeforeIncludedComment - \ProcessCommentWithArg{#1}}% - \CommentEndDef{#1}} -\else -%%%% -%%%%plain TeX and other formats -%%%% -\def\includecomment - #1{\message{Including comment '#1'}% - \csarg\def{#1}{}% - \csarg\def{end#1}{}} -\long\def\specialcomment - #1#2#3{\message{Special comment '#1'}% - \csarg\def{#1}{\def\ThisComment{}\def\AfterComment{#3}#2% - \ProcessComment{#1}}% - \CommentEndDef{#1}} -\fi - -%%%% -%%%% general definition of skipped comment -%%%% -\def\excludecomment - #1{\message{Excluding comment '#1'}% - \csarg\def{#1}{\let\AfterComment\relax - \def\ThisComment####1{}\ProcessComment{#1}}% - \csarg\let{After#1Comment}\TossComment - \CommentEndDef{#1}} - -\if 0% -\ifx\fmtname\latexename - 0% -\else \ifx\fmtname\latexname - 0% - \else - 1% -\fi \fi -% latex & latex2e: -\def\EndOfComment#1{\endgroup\end{#1}% - \csname After#1Comment\endcsname} -\def\CommentEndDef#1{{\escapechar=-1\relax - \csarg\xdef{End#1Test}{\string\\end\string\{#1\string\}}% - }} -\else -% plain & other -\def\EndOfComment#1{\endgroup\AfterComment} -\def\CommentEndDef#1{{\escapechar=-1\relax - \csarg\xdef{End#1Test}{\string\\end#1}% - }} -\fi - -\excludecomment{comment} - -\endinput diff --git a/thys/MDP-Algorithms/output/outline/isabelle.sty b/thys/MDP-Algorithms/output/outline/isabelle.sty deleted file mode 100644 --- a/thys/MDP-Algorithms/output/outline/isabelle.sty +++ /dev/null @@ -1,282 +0,0 @@ -%% -%% macros for Isabelle generated LaTeX output -%% - -%%% Simple document preparation (based on theory token language and symbols) - -% isabelle environments - -\newcommand{\isabellecontext}{UNKNOWN} -\newcommand{\setisabellecontext}[1]{\def\isabellecontext{#1}} - -\newcommand{\isastyle}{\UNDEF} -\newcommand{\isastylett}{\UNDEF} -\newcommand{\isastyleminor}{\UNDEF} -\newcommand{\isastyleminortt}{\UNDEF} -\newcommand{\isastylescript}{\UNDEF} -\newcommand{\isastyletext}{\normalsize\normalfont\rmfamily} -\newcommand{\isastyletxt}{\normalfont\rmfamily} -\newcommand{\isastylecmt}{\normalfont\rmfamily} - -\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}$}} -\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}} - -%blackboard-bold (requires font txmia from pxfonts) -\DeclareSymbolFont{bbbfont}{U}{txmia}{m}{it} -\SetSymbolFont{bbbfont}{bold}{U}{txmia}{bx}{it} -\DeclareMathSymbol{\bbbA}{\mathord}{bbbfont}{129} -\DeclareMathSymbol{\bbbB}{\mathord}{bbbfont}{130} -\DeclareMathSymbol{\bbbC}{\mathord}{bbbfont}{131} -\DeclareMathSymbol{\bbbD}{\mathord}{bbbfont}{132} -\DeclareMathSymbol{\bbbE}{\mathord}{bbbfont}{133} -\DeclareMathSymbol{\bbbF}{\mathord}{bbbfont}{134} -\DeclareMathSymbol{\bbbG}{\mathord}{bbbfont}{135} -\DeclareMathSymbol{\bbbH}{\mathord}{bbbfont}{136} -\DeclareMathSymbol{\bbbI}{\mathord}{bbbfont}{137} -\DeclareMathSymbol{\bbbJ}{\mathord}{bbbfont}{138} -\DeclareMathSymbol{\bbbK}{\mathord}{bbbfont}{139} -\DeclareMathSymbol{\bbbL}{\mathord}{bbbfont}{140} -\DeclareMathSymbol{\bbbM}{\mathord}{bbbfont}{141} -\DeclareMathSymbol{\bbbN}{\mathord}{bbbfont}{142} -\DeclareMathSymbol{\bbbO}{\mathord}{bbbfont}{143} -\DeclareMathSymbol{\bbbP}{\mathord}{bbbfont}{144} -\DeclareMathSymbol{\bbbQ}{\mathord}{bbbfont}{145} -\DeclareMathSymbol{\bbbR}{\mathord}{bbbfont}{146} -\DeclareMathSymbol{\bbbS}{\mathord}{bbbfont}{147} -\DeclareMathSymbol{\bbbT}{\mathord}{bbbfont}{148} -\DeclareMathSymbol{\bbbU}{\mathord}{bbbfont}{149} -\DeclareMathSymbol{\bbbV}{\mathord}{bbbfont}{150} -\DeclareMathSymbol{\bbbW}{\mathord}{bbbfont}{151} -\DeclareMathSymbol{\bbbX}{\mathord}{bbbfont}{152} -\DeclareMathSymbol{\bbbY}{\mathord}{bbbfont}{153} -\DeclareMathSymbol{\bbbZ}{\mathord}{bbbfont}{154} - -\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}} - -\newdimen\isa@parindent\newdimen\isa@parskip - -\newenvironment{isabellebody}{% -\isamarkuptrue\par% -\isa@parindent\parindent\parindent0pt% -\isa@parskip\parskip\parskip0pt% -\isaspacing\isastyle}{\par} - -\newenvironment{isabellebodytt}{% -\isamarkuptrue\par% -\isa@parindent\parindent\parindent0pt% -\isa@parskip\parskip\parskip0pt% -\isaspacing\isastylett}{\par} - -\newenvironment{isabelle} -{\begin{trivlist}\begin{isabellebody}\item\relax} -{\end{isabellebody}\end{trivlist}} - -\newenvironment{isabellett} -{\begin{trivlist}\begin{isabellebodytt}\item\relax} -{\end{isabellebodytt}\end{trivlist}} - -\newcommand{\isa}[1]{\emph{\isaspacing\isastyleminor #1}} -\newcommand{\isatt}[1]{\emph{\isaspacing\isastyleminortt #1}} - -\newcommand{\isaindent}[1]{\hphantom{#1}} -\newcommand{\isanewline}{\mbox{}\par\mbox{}} -\newcommand{\isasep}{} -\newcommand{\isadigit}[1]{#1} - -\newcommand{\isachardefaults}{% -\def\isacharbell{\isamath{\bigbox}}%requires stmaryrd -\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}% -\def\isacartoucheopen{\isatext{\guilsinglleft}}% -\def\isacartoucheclose{\isatext{\guilsinglright}}% -} - - -% keyword and section markup - -\newcommand{\isakeyword}[1] -{\emph{\normalfont\bfseries\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}% -\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}} -\newcommand{\isacommand}[1]{\isakeyword{#1}} - -\newcommand{\isakeywordcontrol}[1] -{\emph{\normalfont\bfseries\itshape\def\isacharunderscore{\isacharunderscorekeyword}#1\,}} - -\newcommand{\isamarkupchapter}[1]{\chapter{#1}} -\newcommand{\isamarkupsection}[1]{\section{#1}} -\newcommand{\isamarkupsubsection}[1]{\subsection{#1}} -\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}} -\newcommand{\isamarkupparagraph}[1]{\paragraph{#1}} -\newcommand{\isamarkupsubparagraph}[1]{\subparagraph{#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}} - - -% index entries - -\newcommand{\isaindexdef}[1]{\textbf{#1}} -\newcommand{\isaindexref}[1]{#1} - - -% styles - -\def\isabellestyle#1{\csname isabellestyle#1\endcsname} - -\newcommand{\isabellestyledefault}{% -\def\isastyle{\small\normalfont\ttfamily\slshape}% -\def\isastylett{\small\normalfont\ttfamily}% -\def\isastyleminor{\small\normalfont\ttfamily\slshape}% -\def\isastyleminortt{\small\normalfont\ttfamily}% -\def\isastylescript{\footnotesize\normalfont\ttfamily\slshape}% -\isachardefaults% -} -\isabellestyledefault - -\newcommand{\isabellestylett}{% -\def\isastyle{\small\normalfont\ttfamily}% -\def\isastylett{\small\normalfont\ttfamily}% -\def\isastyleminor{\small\normalfont\ttfamily}% -\def\isastyleminortt{\small\normalfont\ttfamily}% -\def\isastylescript{\footnotesize\normalfont\ttfamily}% -\isachardefaults% -} - -\newcommand{\isabellestyleit}{% -\def\isastyle{\small\normalfont\itshape}% -\def\isastylett{\small\normalfont\ttfamily}% -\def\isastyleminor{\normalfont\itshape}% -\def\isastyleminortt{\normalfont\ttfamily}% -\def\isastylescript{\footnotesize\normalfont\itshape}% -\isachardefaults% -\def\isacharunderscorekeyword{\mbox{-}}% -\def\isacharbang{\isamath{!}}% -\def\isachardoublequote{}% -\def\isachardoublequoteopen{}% -\def\isachardoublequoteclose{}% -\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{\guilsinglleft}}% -\def\isacharbackquoteclose{\isatext{\guilsinglright}}% -} - -\newcommand{\isabellestyleliteral}{% -\isabellestyleit% -\def\isacharunderscore{\_}% -\def\isacharunderscorekeyword{\_}% -\chardef\isacharbackquoteopen=`\`% -\chardef\isacharbackquoteclose=`\`% -} - -\newcommand{\isabellestyleliteralunderscore}{% -\isabellestyleliteral% -\def\isacharunderscore{\textunderscore}% -\def\isacharunderscorekeyword{\textunderscore}% -} - -\newcommand{\isabellestylesl}{% -\isabellestyleit% -\def\isastyle{\small\normalfont\slshape}% -\def\isastylett{\small\normalfont\ttfamily}% -\def\isastyleminor{\normalfont\slshape}% -\def\isastyleminortt{\normalfont\ttfamily}% -\def\isastylescript{\footnotesize\normalfont\slshape}% -} - - -% cancel text - -\usepackage[normalem]{ulem} -\newcommand{\isamarkupcancel}[1]{\isa{\xout{#1}}} - - -% tags - -\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}} - -\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{} diff --git a/thys/MDP-Algorithms/output/outline/isabellesym.sty b/thys/MDP-Algorithms/output/outline/isabellesym.sty deleted file mode 100644 --- a/thys/MDP-Algorithms/output/outline/isabellesym.sty +++ /dev/null @@ -1,496 +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{\isasymbbbA}{\isamath{\bbbA}} %requires font txmia from txfonts -\newcommand{\isasymbool}{\isamath{\bbbB}} %requires font txmia from txfonts -\newcommand{\isasymcomplex}{\isamath{\bbbC}} %requires font txmia from txfonts -\newcommand{\isasymbbbD}{\isamath{\bbbD}} %requires font txmia from txfonts -\newcommand{\isasymbbbE}{\isamath{\bbbE}} %requires font txmia from txfonts -\newcommand{\isasymbbbF}{\isamath{\bbbF}} %requires font txmia from txfonts -\newcommand{\isasymbbbG}{\isamath{\bbbG}} %requires font txmia from txfonts -\newcommand{\isasymbbbH}{\isamath{\bbbH}} %requires font txmia from txfonts -\newcommand{\isasymbbbI}{\isamath{\bbbI}} %requires font txmia from txfonts -\newcommand{\isasymbbbJ}{\isamath{\bbbJ}} %requires font txmia from txfonts -\newcommand{\isasymbbbK}{\isamath{\bbbK}} %requires font txmia from txfonts -\newcommand{\isasymbbbL}{\isamath{\bbbL}} %requires font txmia from txfonts -\newcommand{\isasymbbbM}{\isamath{\bbbM}} %requires font txmia from txfonts -\newcommand{\isasymnat}{\isamath{\bbbN}} %requires font txmia from txfonts -\newcommand{\isasymbbbO}{\isamath{\bbbO}} %requires font txmia from txfonts -\newcommand{\isasymbbbP}{\isamath{\bbbP}} %requires font txmia from txfonts -\newcommand{\isasymrat}{\isamath{\bbbQ}} %requires font txmia from txfonts -\newcommand{\isasymreal}{\isamath{\bbbR}} %requires font txmia from txfonts -\newcommand{\isasymbbbS}{\isamath{\bbbS}} %requires font txmia from txfonts -\newcommand{\isasymbbbT}{\isamath{\bbbT}} %requires font txmia from txfonts -\newcommand{\isasymbbbU}{\isamath{\bbbU}} %requires font txmia from txfonts -\newcommand{\isasymbbbV}{\isamath{\bbbV}} %requires font txmia from txfonts -\newcommand{\isasymbbbW}{\isamath{\bbbW}} %requires font txmia from txfonts -\newcommand{\isasymbbbX}{\isamath{\bbbX}} %requires font txmia from txfonts -\newcommand{\isasymbbbY}{\isamath{\bbbY}} %requires font txmia from txfonts -\newcommand{\isasymint}{\isamath{\bbbZ}} %requires font txmia from txfonts -\newcommand{\isasymleftarrow}{\isamath{\leftarrow}} -\newcommand{\isasymrightarrow}{\isamath{\rightarrow}} -\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}} -\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}} -\newcommand{\isasymlonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAA}}}} %requires amsmath -\newcommand{\isasymlonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAA}}}} %requires amsmath -\newcommand{\isasymlonglonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAAA}}}} %requires amsmath -\newcommand{\isasymlonglonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAAA}}}} %requires amsmath -\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}} -\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}} -\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}} -\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}} -\newcommand{\isasymLleftarrow}{\isamath{\Lleftarrow}} %requires amssymb -\newcommand{\isasymRrightarrow}{\isamath{\Rrightarrow}} %requires amssymb -\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}} -\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}} -\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}} -\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{\isasymllangle}{\isamath{\langle\mskip-5mu\langle}} -\newcommand{\isasymrrangle}{\isamath{\rangle\mskip-5mu\rangle}} -\newcommand{\isasymlceil}{\isamath{\lceil}} -\newcommand{\isasymrceil}{\isamath{\rceil}} -\newcommand{\isasymlfloor}{\isamath{\lfloor}} -\newcommand{\isasymrfloor}{\isamath{\rfloor}} -\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3.3mu\mid}}} -\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3.3mu)}}} -\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}} -\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}} -\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.3mu\mid}}} -\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.3mu\rbrace}}} -\newcommand{\isasymlblot}{\isamath{{\langle}\mkern -3.5mu{|}}} -\newcommand{\isasymrblot}{\isamath{{|}\mkern -3.5mu{\rangle}}} -\newcommand{\isasymguillemotleft}{\isatext{\guillemotleft}} -\newcommand{\isasymguillemotright}{\isatext{\guillemotright}} -\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{\isasymnot}{\isamath{\neg}} -\newcommand{\isasymnexists}{\isamath{\nexists\,}} %requires amssymb -\newcommand{\isasymcircle}{\isamath{\ocircle}} %requires wasysym -\newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb -\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb -\newcommand{\isasymdiamondop}{\isamath{\diamond}} -\newcommand{\isasymsurd}{\isamath{\surd}} -\newcommand{\isasymturnstile}{\isamath{\vdash}} -\newcommand{\isasymTurnstile}{\isamath{\models}} -\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}} -\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}} -\newcommand{\isasymstileturn}{\isamath{\dashv}} -\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{\isasymParallel}{\isamath{\bigparallel}} %requires stmaryrd -\newcommand{\isasyminterleace}{\isamath{\interleave}} %requires stmaryrd -\newcommand{\isasymsslash}{\isamath{\sslash}} %requires stmaryrd -\newcommand{\isasymbar}{\isamath{\mid}} -\newcommand{\isasymbbar}{\isamath{[\mskip-1.5mu]}} -\newcommand{\isasymplusminus}{\isamath{\pm}} -\newcommand{\isasymminusplus}{\isamath{\mp}} -\newcommand{\isasymtimes}{\isamath{\times}} -\newcommand{\isasymdiv}{\isamath{\div}} -\newcommand{\isasymcdot}{\isamath{\cdot}} -\newcommand{\isasymsqdot}{\isamath{\sbox\z@{$\centerdot$}\ht\z@=.33333\ht\z@\vcenter{\box\z@}}} %requires amssymb -\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{\normalfont\rmfamily\copyright}} -\newcommand{\isasymregistered}{\isatext{\normalfont\rmfamily\textregistered}} -\newcommand{\isasyminverse}{\isamath{{}^{-1}}} -\newcommand{\isasymonequarter}{\isatext{\normalfont\rmfamily\textonequarter}} %requires textcomp -\newcommand{\isasymonehalf}{\isatext{\normalfont\rmfamily\textonehalf}} %requires textcomp -\newcommand{\isasymthreequarters}{\isatext{\normalfont\rmfamily\textthreequarters}} %requires textcomp -\newcommand{\isasymordfeminine}{\isatext{\normalfont\rmfamily\textordfeminine}} -\newcommand{\isasymordmasculine}{\isatext{\normalfont\rmfamily\textordmasculine}} -\newcommand{\isasymsection}{\isatext{\normalfont\rmfamily\S}} -\newcommand{\isasymparagraph}{\isatext{\normalfont\rmfamily\P}} -\newcommand{\isasymexclamdown}{\isatext{\normalfont\rmfamily\textexclamdown}} -\newcommand{\isasymquestiondown}{\isatext{\normalfont\rmfamily\textquestiondown}} -\newcommand{\isasymeuro}{\isatext{\euro}} %requires eurosym -\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{\normalfont\rmfamily\textdegree}} %requires textcomp -\newcommand{\isasymhyphen}{\isatext{\normalfont\rmfamily-}} -\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{\isasymacute}{\isatext{\'\relax}} -\newcommand{\isasymindex}{\isatext{\i}} -\newcommand{\isasymdieresis}{\isatext{\"\relax}} -\newcommand{\isasymcedilla}{\isatext{\c\relax}} -\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}} -\newcommand{\isasymsome}{\isamath{\epsilon\,}} -\newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}} -\newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}} - -%Z notation -\newcommand{\isaZhbar}[1]{\rlap{\raise.0001ex\hbox{\isamath{-}}}#1} -\newcommand{\isaZpvbar}[1]{\ooalign{\hfil\isamath{\mapstochar\mkern 5mu}\hfil\cr#1}} -\newcommand{\isaZfvbar}[1]{\ooalign{\hfil\isamath{\mapstochar\mkern 3mu\mapstochar\mkern 5mu}\hfil\cr#1}} -\newcommand{\isaZdarrow}[3]{\ooalign{\isamath{#1}\hfil\cr\isamath{\mkern#3mu\isamath{#2}}}} -\newcommand{\isasymZcomp}{\isamath{\fatsemi}} %requires stmaryrd -\newcommand{\isasymZinj}{\isamath{\rightarrowtail}} %requires amssymb -\newcommand{\isasymZpinj}{\isaZpvbar{\isamath{\rightarrowtail}}} %requires amssymb -\newcommand{\isasymZfinj}{\isaZfvbar{\isasymZinj}} %requires amssymb -\newcommand{\isasymZsurj}{\isaZdarrow{\rightarrow}{\rightarrow}{4}} %requires amssymb -\newcommand{\isasymZpsurj}{\isaZpvbar{\isasymZsurj}} %requires amssymb -\newcommand{\isasymZbij}{\isaZdarrow{\rightarrowtail}{\rightarrow}{5}} %requires amssymb -\newcommand{\isasymZpfun}{\isaZpvbar{\isamath{\rightarrow}}} -\newcommand{\isasymZffun}{\isaZfvbar{\isamath{\rightarrow}}} -\newcommand{\isasymZdres}{\isamath{\lhd}} %requires amssymb -\newcommand{\isasymZndres}{\isaZhbar{\isamath{\lhd}}} %requires amssymb -\newcommand{\isasymZrres}{\isamath{\rhd}} %requires amssymb -\newcommand{\isasymZnrres}{\isaZhbar{\isamath{\rhd}}} %requires amssymb -\newcommand{\isasymZspot}{\isamath{\bullet}} -\newcommand{\isasymZproject}{\isamath{\upharpoonright}} %requires amssymb -\newcommand{\isasymZsemi}{\isatext{\raise 0.66ex\hbox{\oalign{\hfil\isamath{\scriptscriptstyle\mathrm{o}}\hfil\cr\hfil\isamath{\scriptscriptstyle\mathrm{9}}\hfil}}}} -\newcommand{\isasymZtypecolon}{\isatext{\raise 0.6ex\hbox{\oalign{\hfil\isamath{\scriptscriptstyle\mathrm{o}}\hfil\cr\hfil\isamath{\scriptscriptstyle\mathrm{o}}\hfil}}}} -\newcommand{\isasymZhide}{\isamath{\backslash}} -\newcommand{\isasymZcat}{\isatext{\raise 0.8ex\hbox{\isamath{\mathchar\frown}}}} -\newcommand{\isasymZinbag}{\isatext{\ooalign{\isamath{\sqsubset\mkern-1mu}\cr\isamath{-\mkern-1mu}\cr}}} - -\newcommand{\isasymhole}{\isatext{\normalfont\rmfamily\wasylozenge}} %requires wasysym -\newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}} -\newcommand{\isasymcomment}{\isatext{\isastylecmt---}} -\newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}} -\newcommand{\isasymopen}{\isatext{\guilsinglleft}} -\newcommand{\isasymclose}{\isatext{\guilsinglright}} -\newcommand{\isasymcheckmark}{\isatext{\ding{51}}} %requires pifont -\newcommand{\isasymcrossmark}{\isatext{\ding{55}}} %requires pifont -\newcommand{\isactrlmarker}{\isatext{\ding{48}}} %requires pifont -\newcommand{\isactrltry}{\isakeywordcontrol{try}} -\newcommand{\isactrlcan}{\isakeywordcontrol{can}} -\newcommand{\isactrlassert}{\isakeywordcontrol{assert}} -\newcommand{\isactrlcancel}{\isakeywordcontrol{cancel}} -\newcommand{\isactrlbinding}{\isakeywordcontrol{binding}} -\newcommand{\isactrlclass}{\isakeywordcontrol{class}} -\newcommand{\isactrlclassUNDERSCOREsyntax}{\isakeywordcontrol{class{\isacharunderscore}syntax}} -\newcommand{\isactrlcommandUNDERSCOREkeyword}{\isakeywordcontrol{command{\isacharunderscore}keyword}} -\newcommand{\isactrlconst}{\isakeywordcontrol{const}} -\newcommand{\isactrlconstUNDERSCOREabbrev}{\isakeywordcontrol{const{\isacharunderscore}abbrev}} -\newcommand{\isactrlconstUNDERSCOREname}{\isakeywordcontrol{const{\isacharunderscore}name}} -\newcommand{\isactrlconstUNDERSCOREsyntax}{\isakeywordcontrol{const{\isacharunderscore}syntax}} -\newcommand{\isactrlcontext}{\isakeywordcontrol{context}} -\newcommand{\isactrlcprop}{\isakeywordcontrol{cprop}} -\newcommand{\isactrlcterm}{\isakeywordcontrol{cterm}} -\newcommand{\isactrlctyp}{\isakeywordcontrol{ctyp}} -\newcommand{\isactrldir}{\isakeywordcontrol{dir}} -\newcommand{\isactrlfile}{\isakeywordcontrol{file}} -\newcommand{\isactrlhere}{\isakeywordcontrol{here}} -\newcommand{\isactrlinstantiate}{\isakeywordcontrol{instantiate}} -\newcommand{\isactrlkeyword}{\isakeywordcontrol{keyword}} -\newcommand{\isactrllatex}{\isakeywordcontrol{latex}} -\newcommand{\isactrllocale}{\isakeywordcontrol{locale}} -\newcommand{\isactrlmakeUNDERSCOREjudgment}{\isakeywordcontrol{make{\isacharunderscore}judgment}} -\newcommand{\isactrldestUNDERSCOREjudgment}{\isakeywordcontrol{dest{\isacharunderscore}judgment}} -\newcommand{\isactrlmakeUNDERSCOREstring}{\isakeywordcontrol{make{\isacharunderscore}string}} -\newcommand{\isactrlmasterUNDERSCOREdir}{\isakeywordcontrol{master{\isacharunderscore}dir}} -\newcommand{\isactrlmethod}{\isakeywordcontrol{method}} -\newcommand{\isactrlnamedUNDERSCOREtheorems}{\isakeywordcontrol{named{\isacharunderscore}theorems}} -\newcommand{\isactrlnonterminal}{\isakeywordcontrol{nonterminal}} -\newcommand{\isactrloracleUNDERSCOREname}{\isakeywordcontrol{oracle{\isacharunderscore}name}} -\newcommand{\isactrlpath}{\isakeywordcontrol{path}} -\newcommand{\isactrlpathUNDERSCOREbinding}{\isakeywordcontrol{path{\isacharunderscore}binding}} -\newcommand{\isactrlplugin}{\isakeywordcontrol{plugin}} -\newcommand{\isactrlprint}{\isakeywordcontrol{print}} -\newcommand{\isactrlprop}{\isakeywordcontrol{prop}} -\newcommand{\isactrlscala}{\isakeywordcontrol{scala}} -\newcommand{\isactrlscalaUNDERSCOREfunction}{\isakeywordcontrol{scala{\isacharunderscore}function}} -\newcommand{\isactrlscalaUNDERSCOREmethod}{\isakeywordcontrol{scala{\isacharunderscore}method}} -\newcommand{\isactrlscalaUNDERSCOREobject}{\isakeywordcontrol{scala{\isacharunderscore}object}} -\newcommand{\isactrlscalaUNDERSCOREtype}{\isakeywordcontrol{scala{\isacharunderscore}type}} -\newcommand{\isactrlsimproc}{\isakeywordcontrol{simproc}} -\newcommand{\isactrlsort}{\isakeywordcontrol{sort}} -\newcommand{\isactrlsyntaxUNDERSCOREconst}{\isakeywordcontrol{syntax{\isacharunderscore}const}} -\newcommand{\isactrlsystemUNDERSCOREoption}{\isakeywordcontrol{system{\isacharunderscore}option}} -\newcommand{\isactrlterm}{\isakeywordcontrol{term}} -\newcommand{\isactrltheory}{\isakeywordcontrol{theory}} -\newcommand{\isactrltheoryUNDERSCOREcontext}{\isakeywordcontrol{theory{\isacharunderscore}context}} -\newcommand{\isactrltyp}{\isakeywordcontrol{typ}} -\newcommand{\isactrltypeUNDERSCOREabbrev}{\isakeywordcontrol{type{\isacharunderscore}abbrev}} -\newcommand{\isactrltypeUNDERSCOREname}{\isakeywordcontrol{type{\isacharunderscore}name}} -\newcommand{\isactrltypeUNDERSCOREsyntax}{\isakeywordcontrol{type{\isacharunderscore}syntax}} -\newcommand{\isactrlundefined}{\isakeywordcontrol{undefined}} -\newcommand{\isactrltvar}{\isakeywordcontrol{tvar}} -\newcommand{\isactrlvar}{\isakeywordcontrol{var}} -\newcommand{\isactrlConst}{\isakeywordcontrol{Const}} -\newcommand{\isactrlConstUNDERSCORE}{\isakeywordcontrol{Const{\isacharunderscore}}} -\newcommand{\isactrlConstUNDERSCOREfn}{\isakeywordcontrol{Const{\isacharunderscore}fn}} -\newcommand{\isactrlType}{\isakeywordcontrol{Type}} -\newcommand{\isactrlTypeUNDERSCOREfn}{\isakeywordcontrol{Type{\isacharunderscore}fn}} - -\newcommand{\isactrlcode}{\isakeywordcontrol{code}} -\newcommand{\isactrlcomputation}{\isakeywordcontrol{computation}} -\newcommand{\isactrlcomputationUNDERSCOREconv}{\isakeywordcontrol{computation{\isacharunderscore}conv}} -\newcommand{\isactrlcomputationUNDERSCOREcheck}{\isakeywordcontrol{computation{\isacharunderscore}check}} -\newcommand{\isactrlifUNDERSCORElinux}{\isakeywordcontrol{if{\isacharunderscore}linux}} -\newcommand{\isactrlifUNDERSCOREmacos}{\isakeywordcontrol{if{\isacharunderscore}macos}} -\newcommand{\isactrlifUNDERSCOREwindows}{\isakeywordcontrol{if{\isacharunderscore}windows}} -\newcommand{\isactrlifUNDERSCOREunix}{\isakeywordcontrol{if{\isacharunderscore}unix}} diff --git a/thys/MDP-Algorithms/output/outline/isabelletags.sty b/thys/MDP-Algorithms/output/outline/isabelletags.sty deleted file mode 100644 --- a/thys/MDP-Algorithms/output/outline/isabelletags.sty +++ /dev/null @@ -1,20 +0,0 @@ -%plain TeX version of comment package -- much faster! -\let\isafmtname\fmtname\def\fmtname{plain} -\usepackage{comment} -\let\fmtname\isafmtname - -\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}}} - -\isafoldtag{ML} -\isakeeptag{document} -\isakeeptag{important} -\isadroptag{invisible} -\isafoldtag{proof} -\isakeeptag{theory} -\isakeeptag{unimportant} -\isakeeptag{visible} diff --git a/thys/MDP-Algorithms/output/outline/pdfsetup.sty b/thys/MDP-Algorithms/output/outline/pdfsetup.sty deleted file mode 100644 --- a/thys/MDP-Algorithms/output/outline/pdfsetup.sty +++ /dev/null @@ -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,urlcolor=linkcolor,pdfpagelabels]{hyperref} diff --git a/thys/MDP-Algorithms/output/outline/railsetup.sty b/thys/MDP-Algorithms/output/outline/railsetup.sty deleted file mode 100644 --- a/thys/MDP-Algorithms/output/outline/railsetup.sty +++ /dev/null @@ -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 --git a/thys/MDP-Algorithms/output/outline/root.bib b/thys/MDP-Algorithms/output/outline/root.bib deleted file mode 100644 --- a/thys/MDP-Algorithms/output/outline/root.bib +++ /dev/null @@ -1,13 +0,0 @@ -@book{Puterman, - author = {Martin L. Puterman}, - title = {Markov Decision Processes: Discrete Stochastic Dynamic Programming}, - series = {Wiley Series in Probability and Statistics}, - publisher = {Wiley}, - year = {1994}, - url = {https://doi.org/10.1002/9780470316887}, - doi = {10.1002/9780470316887}, - isbn = {978-0-47161977-2}, - timestamp = {Mon, 22 Jul 2019 15:00:49 +0200}, - biburl = {https://dblp.org/rec/books/wi/Puterman94.bib}, - bibsource = {dblp computer science bibliography, https://dblp.org} -} diff --git a/thys/MDP-Algorithms/output/outline/root.tex b/thys/MDP-Algorithms/output/outline/root.tex deleted file mode 100644 --- a/thys/MDP-Algorithms/output/outline/root.tex +++ /dev/null @@ -1,69 +0,0 @@ -\documentclass[11pt,a4paper]{article} -\usepackage{isabelle,isabellesym} - -% further packages required for unusual symbols (see also -% isabellesym.sty), use only when needed - -\usepackage{amssymb, amsmath, amsfonts} - %for \, \, \, \, \, \, - %\, \, \, \, \, - %\, \, \ - -%\usepackage{eurosym} - %for \ - -\usepackage[only,bigsqcap]{stmaryrd} - %for \ - -%\usepackage{eufrak} - %for \ ... \, \ ... \ (also included in amssymb) - -%\usepackage{textcomp} - %for \, \, \, \, \, - %\ - -% this should be the last package used -\usepackage{pdfsetup} - -% urls in roman style, theory text in math-similar italics -\urlstyle{rm} -\isabellestyle{it} - -% for uniform font size -%\renewcommand{\isastyle}{\isastyleminor} - - -\begin{document} - -\title{Verified Algorithms for Solving Markov Decision Processes} -\author{Maximilian Schäffeler and Mohammad Abdulaziz} -\maketitle - -\abstract{ -We present a formalization of algorithms for solving Markov Decision Processes (MDPs) with formal guarantees on the optimality of their -solutions. -In particular we build on our analysis of the Bellman operator for discounted infinite horizon MDPs. -From the iterator rule on the Bellman operator we directly derive executable value iteration and policy iteration algorithms to iteratively solve finite MDPs. -We also prove correct optimized versions of value iteration that use matrix splittings to improve the convergence rate. In particular, we formally verify Gauss-Seidel value iteration and modified policy iteration. -The algorithms are evaluated on two standard examples from the literature, namely, inventory management and gridworld. -Our formalization covers most of chapter 6 in Puterman's book \cite{Puterman}. -} - -\tableofcontents - -% sane default for proof documents -\parindent 0pt\parskip 0.5ex - -% generated text of all theories -\input{session} - -% optional bibliography -\bibliographystyle{abbrv} -\bibliography{root} - -\end{document} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: t -%%% End: diff --git a/thys/MDP-Algorithms/output/outline/session.tex b/thys/MDP-Algorithms/output/outline/session.tex deleted file mode 100644 --- a/thys/MDP-Algorithms/output/outline/session.tex +++ /dev/null @@ -1,13 +0,0 @@ -\input{Value_Iteration.tex} -\input{Policy_Iteration.tex} -\input{Modified_Policy_Iteration.tex} -\input{Matrix_Util.tex} -\input{Blinfun_Matrix.tex} -\input{Splitting_Methods.tex} -\input{Algorithms.tex} -\input{Code_DP.tex} -\input{Code_Mod.tex} -\input{Code_Real_Approx_By_Float_Fix.tex} -\input{Code_Inventory.tex} -\input{Code_Gridworld.tex} -\input{Examples.tex} diff --git a/thys/MDP-Algorithms/output/outline/session_graph.pdf b/thys/MDP-Algorithms/output/outline/session_graph.pdf deleted file mode 100644 index b03b483f5536b1b7b1f0209d0e8065bb41570191..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 GIT binary patch literal 0 Hc$@