1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/IsarRef/IsaMakefile	Tue Apr 22 13:35:26 2008 +0200
     1.3 @@ -0,0 +1,31 @@
     1.4 +
     1.5 +## targets
     1.6 +
     1.7 +default: Thy
     1.8 +images: 
     1.9 +test: Thy
    1.10 +
    1.11 +all: images test
    1.12 +
    1.13 +
    1.14 +## global settings
    1.15 +
    1.16 +SRC = $(ISABELLE_HOME)/src
    1.17 +OUT = $(ISABELLE_OUTPUT)
    1.18 +LOG = $(OUT)/log
    1.19 +
    1.20 +USEDIR = $(ISATOOL) usedir -v true -i false -d false -C false -D document
    1.21 +
    1.22 +
    1.23 +## Thy
    1.24 +
    1.25 +Thy: $(LOG)/Pure-Thy.gz
    1.26 +
    1.27 +$(LOG)/Pure-Thy.gz: Thy/ROOT.ML ../antiquote_setup.ML
    1.28 +	@$(USEDIR) Pure Thy
    1.29 +
    1.30 +
    1.31 +## clean
    1.32 +
    1.33 +clean:
    1.34 +	@rm -f $(LOG)/Pure-Thy.gz

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/doc-src/IsarRef/Thy/ROOT.ML	Tue Apr 22 13:35:26 2008 +0200
     2.3 @@ -0,0 +1,2 @@
     2.4 +
     2.5 +(* $Id$ *)

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/doc-src/IsarRef/Thy/document/isabelle.sty	Tue Apr 22 13:35:26 2008 +0200
     3.3 @@ -0,0 +1,215 @@
     3.4 +%%
     3.5 +%% 
     3.6 +%%
     3.7 +%% macros for Isabelle generated LaTeX output
     3.8 +%%
     3.9 +
    3.10 +%%% Simple document preparation (based on theory token language and symbols)
    3.11 +
    3.12 +% isabelle environments
    3.13 +
    3.14 +\newcommand{\isabellecontext}{UNKNOWN}
    3.15 +
    3.16 +\newcommand{\isastyle}{\UNDEF}
    3.17 +\newcommand{\isastyleminor}{\UNDEF}
    3.18 +\newcommand{\isastylescript}{\UNDEF}
    3.19 +\newcommand{\isastyletext}{\normalsize\rm}
    3.20 +\newcommand{\isastyletxt}{\rm}
    3.21 +\newcommand{\isastylecmt}{\rm}
    3.22 +
    3.23 +%symbol markup -- \emph achieves decent spacing via italic corrections
    3.24 +\newcommand{\isamath}[1]{\emph{$#1$}}
    3.25 +\newcommand{\isatext}[1]{\emph{#1}}
    3.26 +\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
    3.27 +\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    3.28 +\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
    3.29 +\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    3.30 +\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
    3.31 +\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isastylescript}
    3.32 +\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
    3.33 +\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isastylescript}
    3.34 +\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
    3.35 +\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
    3.36 +\newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
    3.37 +\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
    3.38 +
    3.39 +
    3.40 +\newdimen\isa@parindent\newdimen\isa@parskip
    3.41 +
    3.42 +\newenvironment{isabellebody}{%
    3.43 +\isamarkuptrue\par%
    3.44 +\isa@parindent\parindent\parindent0pt%
    3.45 +\isa@parskip\parskip\parskip0pt%
    3.46 +\isastyle}{\par}
    3.47 +
    3.48 +\newenvironment{isabelle}
    3.49 +{\begin{trivlist}\begin{isabellebody}\item\relax}
    3.50 +{\end{isabellebody}\end{trivlist}}
    3.51 +
    3.52 +\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
    3.53 +
    3.54 +\newcommand{\isaindent}[1]{\hphantom{#1}}
    3.55 +\newcommand{\isanewline}{\mbox{}\par\mbox{}}
    3.56 +\newcommand{\isasep}{}
    3.57 +\newcommand{\isadigit}[1]{#1}
    3.58 +
    3.59 +\newcommand{\isachardefaults}{%
    3.60 +\chardef\isacharbang=`\!%
    3.61 +\chardef\isachardoublequote=`\"%
    3.62 +\chardef\isachardoublequoteopen=`\"%
    3.63 +\chardef\isachardoublequoteclose=`\"%
    3.64 +\chardef\isacharhash=`\#%
    3.65 +\chardef\isachardollar=`\$%
    3.66 +\chardef\isacharpercent=`\%%
    3.67 +\chardef\isacharampersand=`\&%
    3.68 +\chardef\isacharprime=`\'%
    3.69 +\chardef\isacharparenleft=`\(%
    3.70 +\chardef\isacharparenright=`\)%
    3.71 +\chardef\isacharasterisk=`\*%
    3.72 +\chardef\isacharplus=`\+%
    3.73 +\chardef\isacharcomma=`\,%
    3.74 +\chardef\isacharminus=`\-%
    3.75 +\chardef\isachardot=`\.%
    3.76 +\chardef\isacharslash=`\/%
    3.77 +\chardef\isacharcolon=`\:%
    3.78 +\chardef\isacharsemicolon=`\;%
    3.79 +\chardef\isacharless=`\<%
    3.80 +\chardef\isacharequal=`\=%
    3.81 +\chardef\isachargreater=`\>%
    3.82 +\chardef\isacharquery=`\?%
    3.83 +\chardef\isacharat=`\@%
    3.84 +\chardef\isacharbrackleft=`\[%
    3.85 +\chardef\isacharbackslash=`\\%
    3.86 +\chardef\isacharbrackright=`\]%
    3.87 +\chardef\isacharcircum=`\^%
    3.88 +\chardef\isacharunderscore=`\_%
    3.89 +\def\isacharunderscorekeyword{\_}%
    3.90 +\chardef\isacharbackquote=`\`%
    3.91 +\chardef\isacharbackquoteopen=`\`%
    3.92 +\chardef\isacharbackquoteclose=`\`%
    3.93 +\chardef\isacharbraceleft=`\{%
    3.94 +\chardef\isacharbar=`\|%
    3.95 +\chardef\isacharbraceright=`\}%
    3.96 +\chardef\isachartilde=`\~%
    3.97 +\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
    3.98 +\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
    3.99 +}
   3.100 +
   3.101 +
   3.102 +% keyword and section markup
   3.103 +
   3.104 +\newcommand{\isakeyword}[1]
   3.105 +{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
   3.106 +\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
   3.107 +\newcommand{\isacommand}[1]{\isakeyword{#1}}
   3.108 +
   3.109 +\newcommand{\isamarkupheader}[1]{\section{#1}}
   3.110 +\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
   3.111 +\newcommand{\isamarkupsection}[1]{\section{#1}}
   3.112 +\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
   3.113 +\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
   3.114 +\newcommand{\isamarkupsect}[1]{\section{#1}}
   3.115 +\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
   3.116 +\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
   3.117 +
   3.118 +\newif\ifisamarkup
   3.119 +\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
   3.120 +\newcommand{\isaendpar}{\par\medskip}
   3.121 +\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
   3.122 +\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
   3.123 +\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
   3.124 +\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
   3.125 +
   3.126 +
   3.127 +% styles
   3.128 +
   3.129 +\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
   3.130 +
   3.131 +\newcommand{\isabellestyledefault}{%
   3.132 +\renewcommand{\isastyle}{\small\tt\slshape}%
   3.133 +\renewcommand{\isastyleminor}{\small\tt\slshape}%
   3.134 +\renewcommand{\isastylescript}{\footnotesize\tt\slshape}%
   3.135 +\isachardefaults%
   3.136 +}
   3.137 +\isabellestyledefault
   3.138 +
   3.139 +\newcommand{\isabellestylett}{%
   3.140 +\renewcommand{\isastyle}{\small\tt}%
   3.141 +\renewcommand{\isastyleminor}{\small\tt}%
   3.142 +\renewcommand{\isastylescript}{\footnotesize\tt}%
   3.143 +\isachardefaults%
   3.144 +}
   3.145 +
   3.146 +\newcommand{\isabellestyleit}{%
   3.147 +\renewcommand{\isastyle}{\small\it}%
   3.148 +\renewcommand{\isastyleminor}{\it}%
   3.149 +\renewcommand{\isastylescript}{\footnotesize\it}%
   3.150 +\renewcommand{\isacharunderscorekeyword}{\mbox{-}}%
   3.151 +\renewcommand{\isacharbang}{\isamath{!}}%
   3.152 +\renewcommand{\isachardoublequote}{}%
   3.153 +\renewcommand{\isachardoublequoteopen}{}%
   3.154 +\renewcommand{\isachardoublequoteclose}{}%
   3.155 +\renewcommand{\isacharhash}{\isamath{\#}}%
   3.156 +\renewcommand{\isachardollar}{\isamath{\$}}%
   3.157 +\renewcommand{\isacharpercent}{\isamath{\%}}%
   3.158 +\renewcommand{\isacharampersand}{\isamath{\&}}%
   3.159 +\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
   3.160 +\renewcommand{\isacharparenleft}{\isamath{(}}%
   3.161 +\renewcommand{\isacharparenright}{\isamath{)}}%
   3.162 +\renewcommand{\isacharasterisk}{\isamath{*}}%
   3.163 +\renewcommand{\isacharplus}{\isamath{+}}%
   3.164 +\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
   3.165 +\renewcommand{\isacharminus}{\isamath{-}}%
   3.166 +\renewcommand{\isachardot}{\isamath{\mathord.}}%
   3.167 +\renewcommand{\isacharslash}{\isamath{/}}%
   3.168 +\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
   3.169 +\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
   3.170 +\renewcommand{\isacharless}{\isamath{<}}%
   3.171 +\renewcommand{\isacharequal}{\isamath{=}}%
   3.172 +\renewcommand{\isachargreater}{\isamath{>}}%
   3.173 +\renewcommand{\isacharat}{\isamath{@}}%
   3.174 +\renewcommand{\isacharbrackleft}{\isamath{[}}%
   3.175 +\renewcommand{\isacharbackslash}{\isamath{\backslash}}%
   3.176 +\renewcommand{\isacharbrackright}{\isamath{]}}%
   3.177 +\renewcommand{\isacharunderscore}{\mbox{-}}%
   3.178 +\renewcommand{\isacharbraceleft}{\isamath{\{}}%
   3.179 +\renewcommand{\isacharbar}{\isamath{\mid}}%
   3.180 +\renewcommand{\isacharbraceright}{\isamath{\}}}%
   3.181 +\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
   3.182 +\renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
   3.183 +\renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
   3.184 +\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}%
   3.185 +\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}%
   3.186 +}
   3.187 +
   3.188 +\newcommand{\isabellestylesl}{%
   3.189 +\isabellestyleit%
   3.190 +\renewcommand{\isastyle}{\small\sl}%
   3.191 +\renewcommand{\isastyleminor}{\sl}%
   3.192 +\renewcommand{\isastylescript}{\footnotesize\sl}%
   3.193 +}
   3.194 +
   3.195 +
   3.196 +% tagged regions
   3.197 +
   3.198 +%plain TeX version of comment package -- much faster!
   3.199 +\let\isafmtname\fmtname\def\fmtname{plain}
   3.200 +\usepackage{comment}
   3.201 +\let\fmtname\isafmtname
   3.202 +
   3.203 +\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
   3.204 +
   3.205 +\newcommand{\isakeeptag}[1]%
   3.206 +{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
   3.207 +\newcommand{\isadroptag}[1]%
   3.208 +{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
   3.209 +\newcommand{\isafoldtag}[1]%
   3.210 +{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
   3.211 +
   3.212 +\isakeeptag{theory}
   3.213 +\isakeeptag{proof}
   3.214 +\isakeeptag{ML}
   3.215 +\isakeeptag{visible}
   3.216 +\isadroptag{invisible}
   3.217 +
   3.218 +\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/doc-src/IsarRef/Thy/document/isabellesym.sty	Tue Apr 22 13:35:26 2008 +0200
     4.3 @@ -0,0 +1,360 @@
     4.4 +%%
     4.5 +%% 
     4.6 +%%
     4.7 +%% definitions of standard Isabelle symbols
     4.8 +%%
     4.9 +
    4.10 +\newcommand{\isasymzero}{\isamath{\mathbf{0}}}  %requires amssymb
    4.11 +\newcommand{\isasymone}{\isamath{\mathbf{1}}}  %requires amssymb
    4.12 +\newcommand{\isasymtwo}{\isamath{\mathbf{2}}}  %requires amssymb
    4.13 +\newcommand{\isasymthree}{\isamath{\mathbf{3}}}  %requires amssymb
    4.14 +\newcommand{\isasymfour}{\isamath{\mathbf{4}}}  %requires amssymb
    4.15 +\newcommand{\isasymfive}{\isamath{\mathbf{5}}}  %requires amssymb
    4.16 +\newcommand{\isasymsix}{\isamath{\mathbf{6}}}  %requires amssymb
    4.17 +\newcommand{\isasymseven}{\isamath{\mathbf{7}}}  %requires amssymb
    4.18 +\newcommand{\isasymeight}{\isamath{\mathbf{8}}}  %requires amssymb
    4.19 +\newcommand{\isasymnine}{\isamath{\mathbf{9}}}  %requires amssymb
    4.20 +\newcommand{\isasymA}{\isamath{\mathcal{A}}}
    4.21 +\newcommand{\isasymB}{\isamath{\mathcal{B}}}
    4.22 +\newcommand{\isasymC}{\isamath{\mathcal{C}}}
    4.23 +\newcommand{\isasymD}{\isamath{\mathcal{D}}}
    4.24 +\newcommand{\isasymE}{\isamath{\mathcal{E}}}
    4.25 +\newcommand{\isasymF}{\isamath{\mathcal{F}}}
    4.26 +\newcommand{\isasymG}{\isamath{\mathcal{G}}}
    4.27 +\newcommand{\isasymH}{\isamath{\mathcal{H}}}
    4.28 +\newcommand{\isasymI}{\isamath{\mathcal{I}}}
    4.29 +\newcommand{\isasymJ}{\isamath{\mathcal{J}}}
    4.30 +\newcommand{\isasymK}{\isamath{\mathcal{K}}}
    4.31 +\newcommand{\isasymL}{\isamath{\mathcal{L}}}
    4.32 +\newcommand{\isasymM}{\isamath{\mathcal{M}}}
    4.33 +\newcommand{\isasymN}{\isamath{\mathcal{N}}}
    4.34 +\newcommand{\isasymO}{\isamath{\mathcal{O}}}
    4.35 +\newcommand{\isasymP}{\isamath{\mathcal{P}}}
    4.36 +\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}
    4.37 +\newcommand{\isasymR}{\isamath{\mathcal{R}}}
    4.38 +\newcommand{\isasymS}{\isamath{\mathcal{S}}}
    4.39 +\newcommand{\isasymT}{\isamath{\mathcal{T}}}
    4.40 +\newcommand{\isasymU}{\isamath{\mathcal{U}}}
    4.41 +\newcommand{\isasymV}{\isamath{\mathcal{V}}}
    4.42 +\newcommand{\isasymW}{\isamath{\mathcal{W}}}
    4.43 +\newcommand{\isasymX}{\isamath{\mathcal{X}}}
    4.44 +\newcommand{\isasymY}{\isamath{\mathcal{Y}}}
    4.45 +\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
    4.46 +\newcommand{\isasyma}{\isamath{\mathrm{a}}}
    4.47 +\newcommand{\isasymb}{\isamath{\mathrm{b}}}
    4.48 +\newcommand{\isasymc}{\isamath{\mathrm{c}}}
    4.49 +\newcommand{\isasymd}{\isamath{\mathrm{d}}}
    4.50 +\newcommand{\isasyme}{\isamath{\mathrm{e}}}
    4.51 +\newcommand{\isasymf}{\isamath{\mathrm{f}}}
    4.52 +\newcommand{\isasymg}{\isamath{\mathrm{g}}}
    4.53 +\newcommand{\isasymh}{\isamath{\mathrm{h}}}
    4.54 +\newcommand{\isasymi}{\isamath{\mathrm{i}}}
    4.55 +\newcommand{\isasymj}{\isamath{\mathrm{j}}}
    4.56 +\newcommand{\isasymk}{\isamath{\mathrm{k}}}
    4.57 +\newcommand{\isasyml}{\isamath{\mathrm{l}}}
    4.58 +\newcommand{\isasymm}{\isamath{\mathrm{m}}}
    4.59 +\newcommand{\isasymn}{\isamath{\mathrm{n}}}
    4.60 +\newcommand{\isasymo}{\isamath{\mathrm{o}}}
    4.61 +\newcommand{\isasymp}{\isamath{\mathrm{p}}}
    4.62 +\newcommand{\isasymq}{\isamath{\mathrm{q}}}
    4.63 +\newcommand{\isasymr}{\isamath{\mathrm{r}}}
    4.64 +\newcommand{\isasyms}{\isamath{\mathrm{s}}}
    4.65 +\newcommand{\isasymt}{\isamath{\mathrm{t}}}
    4.66 +\newcommand{\isasymu}{\isamath{\mathrm{u}}}
    4.67 +\newcommand{\isasymv}{\isamath{\mathrm{v}}}
    4.68 +\newcommand{\isasymw}{\isamath{\mathrm{w}}}
    4.69 +\newcommand{\isasymx}{\isamath{\mathrm{x}}}
    4.70 +\newcommand{\isasymy}{\isamath{\mathrm{y}}}
    4.71 +\newcommand{\isasymz}{\isamath{\mathrm{z}}}
    4.72 +\newcommand{\isasymAA}{\isamath{\mathfrak{A}}}  %requires eufrak
    4.73 +\newcommand{\isasymBB}{\isamath{\mathfrak{B}}}  %requires eufrak
    4.74 +\newcommand{\isasymCC}{\isamath{\mathfrak{C}}}  %requires eufrak
    4.75 +\newcommand{\isasymDD}{\isamath{\mathfrak{D}}}  %requires eufrak
    4.76 +\newcommand{\isasymEE}{\isamath{\mathfrak{E}}}  %requires eufrak
    4.77 +\newcommand{\isasymFF}{\isamath{\mathfrak{F}}}  %requires eufrak
    4.78 +\newcommand{\isasymGG}{\isamath{\mathfrak{G}}}  %requires eufrak
    4.79 +\newcommand{\isasymHH}{\isamath{\mathfrak{H}}}  %requires eufrak
    4.80 +\newcommand{\isasymII}{\isamath{\mathfrak{I}}}  %requires eufrak
    4.81 +\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}}  %requires eufrak
    4.82 +\newcommand{\isasymKK}{\isamath{\mathfrak{K}}}  %requires eufrak
    4.83 +\newcommand{\isasymLL}{\isamath{\mathfrak{L}}}  %requires eufrak
    4.84 +\newcommand{\isasymMM}{\isamath{\mathfrak{M}}}  %requires eufrak
    4.85 +\newcommand{\isasymNN}{\isamath{\mathfrak{N}}}  %requires eufrak
    4.86 +\newcommand{\isasymOO}{\isamath{\mathfrak{O}}}  %requires eufrak
    4.87 +\newcommand{\isasymPP}{\isamath{\mathfrak{P}}}  %requires eufrak
    4.88 +\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}}  %requires eufrak
    4.89 +\newcommand{\isasymRR}{\isamath{\mathfrak{R}}}  %requires eufrak
    4.90 +\newcommand{\isasymSS}{\isamath{\mathfrak{S}}}  %requires eufrak
    4.91 +\newcommand{\isasymTT}{\isamath{\mathfrak{T}}}  %requires eufrak
    4.92 +\newcommand{\isasymUU}{\isamath{\mathfrak{U}}}  %requires eufrak
    4.93 +\newcommand{\isasymVV}{\isamath{\mathfrak{V}}}  %requires eufrak
    4.94 +\newcommand{\isasymWW}{\isamath{\mathfrak{W}}}  %requires eufrak
    4.95 +\newcommand{\isasymXX}{\isamath{\mathfrak{X}}}  %requires eufrak
    4.96 +\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}}  %requires eufrak
    4.97 +\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}}  %requires eufrak
    4.98 +\newcommand{\isasymaa}{\isamath{\mathfrak{a}}}  %requires eufrak
    4.99 +\newcommand{\isasymbb}{\isamath{\mathfrak{b}}}  %requires eufrak
   4.100 +\newcommand{\isasymcc}{\isamath{\mathfrak{c}}}  %requires eufrak
   4.101 +\newcommand{\isasymdd}{\isamath{\mathfrak{d}}}  %requires eufrak
   4.102 +\newcommand{\isasymee}{\isamath{\mathfrak{e}}}  %requires eufrak
   4.103 +\newcommand{\isasymff}{\isamath{\mathfrak{f}}}  %requires eufrak
   4.104 +\newcommand{\isasymgg}{\isamath{\mathfrak{g}}}  %requires eufrak
   4.105 +\newcommand{\isasymhh}{\isamath{\mathfrak{h}}}  %requires eufrak
   4.106 +\newcommand{\isasymii}{\isamath{\mathfrak{i}}}  %requires eufrak
   4.107 +\newcommand{\isasymjj}{\isamath{\mathfrak{j}}}  %requires eufrak
   4.108 +\newcommand{\isasymkk}{\isamath{\mathfrak{k}}}  %requires eufrak
   4.109 +\newcommand{\isasymll}{\isamath{\mathfrak{l}}}  %requires eufrak
   4.110 +\newcommand{\isasymmm}{\isamath{\mathfrak{m}}}  %requires eufrak
   4.111 +\newcommand{\isasymnn}{\isamath{\mathfrak{n}}}  %requires eufrak
   4.112 +\newcommand{\isasymoo}{\isamath{\mathfrak{o}}}  %requires eufrak
   4.113 +\newcommand{\isasympp}{\isamath{\mathfrak{p}}}  %requires eufrak
   4.114 +\newcommand{\isasymqq}{\isamath{\mathfrak{q}}}  %requires eufrak
   4.115 +\newcommand{\isasymrr}{\isamath{\mathfrak{r}}}  %requires eufrak
   4.116 +\newcommand{\isasymss}{\isamath{\mathfrak{s}}}  %requires eufrak
   4.117 +\newcommand{\isasymtt}{\isamath{\mathfrak{t}}}  %requires eufrak
   4.118 +\newcommand{\isasymuu}{\isamath{\mathfrak{u}}}  %requires eufrak
   4.119 +\newcommand{\isasymvv}{\isamath{\mathfrak{v}}}  %requires eufrak
   4.120 +\newcommand{\isasymww}{\isamath{\mathfrak{w}}}  %requires eufrak
   4.121 +\newcommand{\isasymxx}{\isamath{\mathfrak{x}}}  %requires eufrak
   4.122 +\newcommand{\isasymyy}{\isamath{\mathfrak{y}}}  %requires eufrak
   4.123 +\newcommand{\isasymzz}{\isamath{\mathfrak{z}}}  %requires eufrak
   4.124 +\newcommand{\isasymalpha}{\isamath{\alpha}}
   4.125 +\newcommand{\isasymbeta}{\isamath{\beta}}
   4.126 +\newcommand{\isasymgamma}{\isamath{\gamma}}
   4.127 +\newcommand{\isasymdelta}{\isamath{\delta}}
   4.128 +\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
   4.129 +\newcommand{\isasymzeta}{\isamath{\zeta}}
   4.130 +\newcommand{\isasymeta}{\isamath{\eta}}
   4.131 +\newcommand{\isasymtheta}{\isamath{\vartheta}}
   4.132 +\newcommand{\isasymiota}{\isamath{\iota}}
   4.133 +\newcommand{\isasymkappa}{\isamath{\kappa}}
   4.134 +\newcommand{\isasymlambda}{\isamath{\lambda}}
   4.135 +\newcommand{\isasymmu}{\isamath{\mu}}
   4.136 +\newcommand{\isasymnu}{\isamath{\nu}}
   4.137 +\newcommand{\isasymxi}{\isamath{\xi}}
   4.138 +\newcommand{\isasympi}{\isamath{\pi}}
   4.139 +\newcommand{\isasymrho}{\isamath{\varrho}}
   4.140 +\newcommand{\isasymsigma}{\isamath{\sigma}}
   4.141 +\newcommand{\isasymtau}{\isamath{\tau}}
   4.142 +\newcommand{\isasymupsilon}{\isamath{\upsilon}}
   4.143 +\newcommand{\isasymphi}{\isamath{\varphi}}
   4.144 +\newcommand{\isasymchi}{\isamath{\chi}}
   4.145 +\newcommand{\isasympsi}{\isamath{\psi}}
   4.146 +\newcommand{\isasymomega}{\isamath{\omega}}
   4.147 +\newcommand{\isasymGamma}{\isamath{\Gamma}}
   4.148 +\newcommand{\isasymDelta}{\isamath{\Delta}}
   4.149 +\newcommand{\isasymTheta}{\isamath{\Theta}}
   4.150 +\newcommand{\isasymLambda}{\isamath{\Lambda}}
   4.151 +\newcommand{\isasymXi}{\isamath{\Xi}}
   4.152 +\newcommand{\isasymPi}{\isamath{\Pi}}
   4.153 +\newcommand{\isasymSigma}{\isamath{\Sigma}}
   4.154 +\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
   4.155 +\newcommand{\isasymPhi}{\isamath{\Phi}}
   4.156 +\newcommand{\isasymPsi}{\isamath{\Psi}}
   4.157 +\newcommand{\isasymOmega}{\isamath{\Omega}}
   4.158 +\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
   4.159 +\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
   4.160 +\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
   4.161 +\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
   4.162 +\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
   4.163 +\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
   4.164 +\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
   4.165 +\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
   4.166 +\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
   4.167 +\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
   4.168 +\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
   4.169 +\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
   4.170 +\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
   4.171 +\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
   4.172 +\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
   4.173 +\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
   4.174 +\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
   4.175 +\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
   4.176 +\newcommand{\isasymmapsto}{\isamath{\mapsto}}
   4.177 +\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
   4.178 +\newcommand{\isasymmidarrow}{\isamath{\relbar}}
   4.179 +\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
   4.180 +\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
   4.181 +\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
   4.182 +\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
   4.183 +\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
   4.184 +\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
   4.185 +\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
   4.186 +\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
   4.187 +\newcommand{\isasymleadsto}{\isamath{\leadsto}}  %requires amssymb
   4.188 +\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}}  %requires amssymb
   4.189 +\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}}  %requires amssymb
   4.190 +\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}}  %requires amssymb
   4.191 +\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}}  %requires amssymb
   4.192 +\newcommand{\isasymrestriction}{\isamath{\restriction}}  %requires amssymb
   4.193 +\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
   4.194 +\newcommand{\isasymup}{\isamath{\uparrow}}
   4.195 +\newcommand{\isasymUp}{\isamath{\Uparrow}}
   4.196 +\newcommand{\isasymdown}{\isamath{\downarrow}}
   4.197 +\newcommand{\isasymDown}{\isamath{\Downarrow}}
   4.198 +\newcommand{\isasymupdown}{\isamath{\updownarrow}}
   4.199 +\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
   4.200 +\newcommand{\isasymlangle}{\isamath{\langle}}
   4.201 +\newcommand{\isasymrangle}{\isamath{\rangle}}
   4.202 +\newcommand{\isasymlceil}{\isamath{\lceil}}
   4.203 +\newcommand{\isasymrceil}{\isamath{\rceil}}
   4.204 +\newcommand{\isasymlfloor}{\isamath{\lfloor}}
   4.205 +\newcommand{\isasymrfloor}{\isamath{\rfloor}}
   4.206 +\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
   4.207 +\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}
   4.208 +\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
   4.209 +\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
   4.210 +\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
   4.211 +\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
   4.212 +\newcommand{\isasymguillemotleft}{\isatext{\flqq}}  %requires babel
   4.213 +\newcommand{\isasymguillemotright}{\isatext{\frqq}}  %requires babel
   4.214 +\newcommand{\isasymbottom}{\isamath{\bot}}
   4.215 +\newcommand{\isasymtop}{\isamath{\top}}
   4.216 +\newcommand{\isasymand}{\isamath{\wedge}}
   4.217 +\newcommand{\isasymAnd}{\isamath{\bigwedge}}
   4.218 +\newcommand{\isasymor}{\isamath{\vee}}
   4.219 +\newcommand{\isasymOr}{\isamath{\bigvee}}
   4.220 +\newcommand{\isasymforall}{\isamath{\forall\,}}
   4.221 +\newcommand{\isasymexists}{\isamath{\exists\,}}
   4.222 +\newcommand{\isasymnexists}{\isamath{\nexists\,}}  %requires amssymb
   4.223 +\newcommand{\isasymnot}{\isamath{\neg}}
   4.224 +\newcommand{\isasymbox}{\isamath{\Box}}  %requires amssymb
   4.225 +\newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires amssymb
   4.226 +\newcommand{\isasymturnstile}{\isamath{\vdash}}
   4.227 +\newcommand{\isasymTurnstile}{\isamath{\models}}
   4.228 +\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
   4.229 +\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
   4.230 +\newcommand{\isasymstileturn}{\isamath{\dashv}}
   4.231 +\newcommand{\isasymsurd}{\isamath{\surd}}
   4.232 +\newcommand{\isasymle}{\isamath{\le}}
   4.233 +\newcommand{\isasymge}{\isamath{\ge}}
   4.234 +\newcommand{\isasymlless}{\isamath{\ll}}
   4.235 +\newcommand{\isasymggreater}{\isamath{\gg}}
   4.236 +\newcommand{\isasymlesssim}{\isamath{\lesssim}}  %requires amssymb
   4.237 +\newcommand{\isasymgreatersim}{\isamath{\gtrsim}}  %requires amssymb
   4.238 +\newcommand{\isasymlessapprox}{\isamath{\lessapprox}}  %requires amssymb
   4.239 +\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}}  %requires amssymb
   4.240 +\newcommand{\isasymin}{\isamath{\in}}
   4.241 +\newcommand{\isasymnotin}{\isamath{\notin}}
   4.242 +\newcommand{\isasymsubset}{\isamath{\subset}}
   4.243 +\newcommand{\isasymsupset}{\isamath{\supset}}
   4.244 +\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
   4.245 +\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
   4.246 +\newcommand{\isasymsqsubset}{\isamath{\sqsubset}}  %requires amssymb
   4.247 +\newcommand{\isasymsqsupset}{\isamath{\sqsupset}}  %requires amssymb
   4.248 +\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
   4.249 +\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
   4.250 +\newcommand{\isasyminter}{\isamath{\cap}}
   4.251 +\newcommand{\isasymInter}{\isamath{\bigcap\,}}
   4.252 +\newcommand{\isasymunion}{\isamath{\cup}}
   4.253 +\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
   4.254 +\newcommand{\isasymsqunion}{\isamath{\sqcup}}
   4.255 +\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
   4.256 +\newcommand{\isasymsqinter}{\isamath{\sqcap}}
   4.257 +\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}}  %requires amsmath
   4.258 +\newcommand{\isasymsetminus}{\isamath{\setminus}}
   4.259 +\newcommand{\isasympropto}{\isamath{\propto}}
   4.260 +\newcommand{\isasymuplus}{\isamath{\uplus}}
   4.261 +\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
   4.262 +\newcommand{\isasymnoteq}{\isamath{\not=}}
   4.263 +\newcommand{\isasymsim}{\isamath{\sim}}
   4.264 +\newcommand{\isasymdoteq}{\isamath{\doteq}}
   4.265 +\newcommand{\isasymsimeq}{\isamath{\simeq}}
   4.266 +\newcommand{\isasymapprox}{\isamath{\approx}}
   4.267 +\newcommand{\isasymasymp}{\isamath{\asymp}}
   4.268 +\newcommand{\isasymcong}{\isamath{\cong}}
   4.269 +\newcommand{\isasymsmile}{\isamath{\smile}}
   4.270 +\newcommand{\isasymequiv}{\isamath{\equiv}}
   4.271 +\newcommand{\isasymfrown}{\isamath{\frown}}
   4.272 +\newcommand{\isasymJoin}{\isamath{\Join}}  %requires amssymb
   4.273 +\newcommand{\isasymbowtie}{\isamath{\bowtie}}
   4.274 +\newcommand{\isasymprec}{\isamath{\prec}}
   4.275 +\newcommand{\isasymsucc}{\isamath{\succ}}
   4.276 +\newcommand{\isasympreceq}{\isamath{\preceq}}
   4.277 +\newcommand{\isasymsucceq}{\isamath{\succeq}}
   4.278 +\newcommand{\isasymparallel}{\isamath{\parallel}}
   4.279 +\newcommand{\isasymbar}{\isamath{\mid}}
   4.280 +\newcommand{\isasymplusminus}{\isamath{\pm}}
   4.281 +\newcommand{\isasymminusplus}{\isamath{\mp}}
   4.282 +\newcommand{\isasymtimes}{\isamath{\times}}
   4.283 +\newcommand{\isasymdiv}{\isamath{\div}}
   4.284 +\newcommand{\isasymcdot}{\isamath{\cdot}}
   4.285 +\newcommand{\isasymstar}{\isamath{\star}}
   4.286 +\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
   4.287 +\newcommand{\isasymcirc}{\isamath{\circ}}
   4.288 +\newcommand{\isasymdagger}{\isamath{\dagger}}
   4.289 +\newcommand{\isasymddagger}{\isamath{\ddagger}}
   4.290 +\newcommand{\isasymlhd}{\isamath{\lhd}}  %requires amssymb
   4.291 +\newcommand{\isasymrhd}{\isamath{\rhd}}  %requires amssymb
   4.292 +\newcommand{\isasymunlhd}{\isamath{\unlhd}}  %requires amssymb
   4.293 +\newcommand{\isasymunrhd}{\isamath{\unrhd}}  %requires amssymb
   4.294 +\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
   4.295 +\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
   4.296 +\newcommand{\isasymtriangle}{\isamath{\triangle}}
   4.297 +\newcommand{\isasymtriangleq}{\isamath{\triangleq}}  %requires amssymb
   4.298 +\newcommand{\isasymoplus}{\isamath{\oplus}}
   4.299 +\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}
   4.300 +\newcommand{\isasymotimes}{\isamath{\otimes}}
   4.301 +\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}
   4.302 +\newcommand{\isasymodot}{\isamath{\odot}}
   4.303 +\newcommand{\isasymOdot}{\isamath{\bigodot\,}}
   4.304 +\newcommand{\isasymominus}{\isamath{\ominus}}
   4.305 +\newcommand{\isasymoslash}{\isamath{\oslash}}
   4.306 +\newcommand{\isasymdots}{\isamath{\dots}}
   4.307 +\newcommand{\isasymcdots}{\isamath{\cdots}}
   4.308 +\newcommand{\isasymSum}{\isamath{\sum\,}}
   4.309 +\newcommand{\isasymProd}{\isamath{\prod\,}}
   4.310 +\newcommand{\isasymCoprod}{\isamath{\coprod\,}}
   4.311 +\newcommand{\isasyminfinity}{\isamath{\infty}}
   4.312 +\newcommand{\isasymintegral}{\isamath{\int\,}}
   4.313 +\newcommand{\isasymointegral}{\isamath{\oint\,}}
   4.314 +\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
   4.315 +\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
   4.316 +\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
   4.317 +\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
   4.318 +\newcommand{\isasymaleph}{\isamath{\aleph}}
   4.319 +\newcommand{\isasymemptyset}{\isamath{\emptyset}}
   4.320 +\newcommand{\isasymnabla}{\isamath{\nabla}}
   4.321 +\newcommand{\isasympartial}{\isamath{\partial}}
   4.322 +\newcommand{\isasymRe}{\isamath{\Re}}
   4.323 +\newcommand{\isasymIm}{\isamath{\Im}}
   4.324 +\newcommand{\isasymflat}{\isamath{\flat}}
   4.325 +\newcommand{\isasymnatural}{\isamath{\natural}}
   4.326 +\newcommand{\isasymsharp}{\isamath{\sharp}}
   4.327 +\newcommand{\isasymangle}{\isamath{\angle}}
   4.328 +\newcommand{\isasymcopyright}{\isatext{\rm\copyright}}
   4.329 +\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
   4.330 +\newcommand{\isasymhyphen}{\isatext{\rm-}}
   4.331 +\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
   4.332 +\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}}  %requires latin1
   4.333 +\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}}  %requires latin1
   4.334 +\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}}  %requires latin1
   4.335 +\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}}  %requires latin1
   4.336 +\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}}  %requires latin1
   4.337 +\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}}  %requires latin1
   4.338 +\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
   4.339 +\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
   4.340 +\newcommand{\isasymsection}{\isatext{\rm\S}}
   4.341 +\newcommand{\isasymparagraph}{\isatext{\rm\P}}
   4.342 +\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
   4.343 +\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
   4.344 +\newcommand{\isasymeuro}{\isatext{\textgreek{\euro}}}  %requires greek babel
   4.345 +\newcommand{\isasympounds}{\isamath{\pounds}}
   4.346 +\newcommand{\isasymyen}{\isatext{\yen}}  %requires amssymb
   4.347 +\newcommand{\isasymcent}{\isatext{\textcent}}  %requires textcomp
   4.348 +\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
   4.349 +\newcommand{\isasymdegree}{\isatext{\rm\textdegree}}  %requires latin1
   4.350 +\newcommand{\isasymamalg}{\isamath{\amalg}}
   4.351 +\newcommand{\isasymmho}{\isamath{\mho}}  %requires amssymb
   4.352 +\newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssymb
   4.353 +\newcommand{\isasymwp}{\isamath{\wp}}
   4.354 +\newcommand{\isasymwrong}{\isamath{\wr}}
   4.355 +\newcommand{\isasymstruct}{\isamath{\diamond}}
   4.356 +\newcommand{\isasymacute}{\isatext{\'\relax}}
   4.357 +\newcommand{\isasymindex}{\isatext{\i}}
   4.358 +\newcommand{\isasymdieresis}{\isatext{\"\relax}}
   4.359 +\newcommand{\isasymcedilla}{\isatext{\c\relax}}
   4.360 +\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
   4.361 +\newcommand{\isasymspacespace}{\isamath{~~}}
   4.362 +\newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}
   4.363 +\newcommand{\isasymsome}{\isamath{\epsilon\,}}

     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/doc-src/IsarRef/Thy/document/pdfsetup.sty	Tue Apr 22 13:35:26 2008 +0200
     5.3 @@ -0,0 +1,25 @@
     5.4 +%%
     5.5 +%% 
     5.6 +%%
     5.7 +%% smart url or hyperref setup
     5.8 +%%
     5.9 +
    5.10 +\newif\ifpdfoutput
    5.11 +\ifx\pdfoutput\undefined
    5.12 +\else
    5.13 +  \ifx\pdfoutput\relax
    5.14 +  \else
    5.15 +    \ifcase\pdfoutput
    5.16 +    \else\pdfoutputtrue\fi
    5.17 +  \fi
    5.18 +\fi
    5.19 +
    5.20 +\ifpdfoutput
    5.21 +  \message{PDF output}
    5.22 +  \usepackage{color}\definecolor{darkblue}{rgb}{0,0,0.5}
    5.23 +  \usepackage[pdftex,a4paper,colorlinks=true,linkcolor=darkblue,citecolor=darkblue,filecolor=darkblue,pagecolor=darkblue,urlcolor=darkblue]{hyperref}
    5.24 +  \IfFileExists{thumbpdf.sty}{\usepackage{thumbpdf}}{}
    5.25 +\else
    5.26 +  \message{No PDF output}
    5.27 +  \usepackage{url}
    5.28 +\fi

     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/doc-src/IsarRef/Thy/document/session.tex	Tue Apr 22 13:35:26 2008 +0200
     6.3 @@ -0,0 +1,4 @@
     6.4 +%%% Local Variables:
     6.5 +%%% mode: latex
     6.6 +%%% TeX-master: "root"
     6.7 +%%% End:

     7.1 --- a/doc-src/IsarRef/isar-ref.tex	Tue Apr 22 10:31:15 2008 +0200
     7.2 +++ b/doc-src/IsarRef/isar-ref.tex	Tue Apr 22 13:35:26 2008 +0200
     7.3 @@ -2,24 +2,18 @@
     7.4  %% $Id$
     7.5  
     7.6  \documentclass[12pt,a4paper,fleqn]{report}
     7.7 -\usepackage{latexsym,graphicx,../iman,../extra,../ttbox,../proof,../rail,../railsetup,../isar,../pdfsetup}
     7.8 +\usepackage{latexsym,graphicx}
     7.9 +\usepackage{../iman,../extra,../isar,../proof}
    7.10 +\usepackage{Thy/document/isabelle,Thy/document/isabellesym}
    7.11 +\usepackage{../ttbox,,../rail,../railsetup}
    7.12 +\usepackage{style}
    7.13 +\usepackage{../pdfsetup}
    7.14  
    7.15  \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
    7.16  \author{\emph{Markus Wenzel} \\ TU M\"unchen}
    7.17  
    7.18  \makeindex
    7.19  
    7.20 -\newcommand{\isastyle}{\small\tt\slshape}
    7.21 -\newcommand{\isa}[1]{\emph{\isastyle #1}}
    7.22 -\newcommand{\isamath}[1]{\emph{$#1$}}
    7.23 -\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
    7.24 -\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
    7.25 -\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
    7.26 -\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
    7.27 -\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
    7.28 -\newcommand{\isasymequiv}{\isamath{\equiv}}
    7.29 -\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
    7.30 -
    7.31  \railterm{percent,ppercent,underscore,lbrace,rbrace,atsign}
    7.32  \railterm{ident,longident,symident,var,textvar,typefree,typevar,nat,string,verbatim,keyword}
    7.33  \railterm{name,nameref,text,type,term,prop,atom}
    7.34 @@ -61,8 +55,6 @@
    7.35  
    7.36  \renewcommand{\phi}{\varphi}
    7.37  
    7.38 -%\includeonly{}
    7.39 -
    7.40  
    7.41  \begin{document}
    7.42  

     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/doc-src/IsarRef/style.sty	Tue Apr 22 13:35:26 2008 +0200
     8.3 @@ -0,0 +1,49 @@
     8.4 +
     8.5 +%% $Id$
     8.6 +
     8.7 +%% toc
     8.8 +\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
     8.9 +\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
    8.10 +
    8.11 +%% references
    8.12 +\newcommand{\secref}[1]{\S\ref{#1}}
    8.13 +\newcommand{\chref}[1]{chapter~\ref{#1}}
    8.14 +\newcommand{\figref}[1]{figure~\ref{#1}}
    8.15 +
    8.16 +%% index
    8.17 +%FIXME
    8.18 +
    8.19 +%% math
    8.20 +\newcommand{\text}[1]{\mbox{#1}}
    8.21 +\newcommand{\isasymvartheta}{\isamath{\theta}}
    8.22 +\newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
    8.23 +
    8.24 +\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
    8.25 +
    8.26 +\pagestyle{headings}
    8.27 +\sloppy
    8.28 +\binperiod
    8.29 +\underscoreon
    8.30 +
    8.31 +\renewcommand{\isadigit}[1]{\isamath{#1}}
    8.32 +
    8.33 +\newcommand{\minorcmd}[1]{{\sf #1}}
    8.34 +
    8.35 +\newcommand{\isasymGUESS}{\isakeyword{guess}}
    8.36 +\newcommand{\isasymOBTAIN}{\isakeyword{obtain}}
    8.37 +\newcommand{\isasymTHEORY}{\isakeyword{theory}}
    8.38 +\newcommand{\isasymIMPORTS}{\isakeyword{imports}}
    8.39 +\newcommand{\isasymUSES}{\isakeyword{uses}}
    8.40 +\newcommand{\isasymBEGIN}{\isakeyword{begin}}
    8.41 +\newcommand{\isasymEND}{\isakeyword{end}}
    8.42 +\newcommand{\isasymCONSTS}{\isakeyword{consts}}
    8.43 +\newcommand{\isasymDEFS}{\isakeyword{defs}}
    8.44 +\newcommand{\isasymTHEOREM}{\isakeyword{theorem}}
    8.45 +\newcommand{\isasymDEFINITION}{\isakeyword{definition}}
    8.46 +
    8.47 +\isabellestyle{it}
    8.48 +
    8.49 +%%% Local Variables: 
    8.50 +%%% mode: latex
    8.51 +%%% TeX-master: "implementation"
    8.52 +%%% End: