1.1 --- a/doc-src/IsarImplementation/Thy/ML.thy Tue Jan 03 11:57:33 2006 +0100
1.2 +++ b/doc-src/IsarImplementation/Thy/ML.thy Tue Jan 03 13:59:55 2006 +0100
1.3 @@ -5,7 +5,10 @@
1.4
1.5 chapter {* Aesthetics of ML programming *}
1.6
1.7 -text {* FIXME style guide *}
1.8 +text {* FIXME style guide, see also
1.9 +\url{http://caml.inria.fr/resources/doc/guides/guidelines.en.html} and
1.10 +\url{http://www.cs.cornell.edu/Courses/cs312/2003sp/handouts/style.htm}
1.11 +*}
1.12
1.13
1.14 chapter {* Basic library functions *}
2.1 --- a/doc-src/IsarImplementation/Thy/document/ML.tex Tue Jan 03 11:57:33 2006 +0100
2.2 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex Tue Jan 03 13:59:55 2006 +0100
2.3 @@ -24,7 +24,9 @@
2.4 \isamarkuptrue%
2.5 %
2.6 \begin{isamarkuptext}%
2.7 -FIXME style guide%
2.8 +FIXME style guide, see also
2.9 +\url{http://caml.inria.fr/resources/doc/guides/guidelines.en.html} and
2.10 +\url{http://www.cs.cornell.edu/Courses/cs312/2003sp/handouts/style.htm}%
2.11 \end{isamarkuptext}%
2.12 \isamarkuptrue%
2.13 %
3.1 --- a/doc-src/IsarImplementation/Thy/document/integration.tex Tue Jan 03 11:57:33 2006 +0100
3.2 +++ b/doc-src/IsarImplementation/Thy/document/integration.tex Tue Jan 03 13:59:55 2006 +0100
3.3 @@ -394,7 +394,7 @@
3.4 been concluded, in order to support legacy proof {\ML} proof
3.5 scripts.
3.6
3.7 - The basic internal actions of the theory database are \isa{update}\indexbold{\isa{update} theory}, \isa{outdate}\indexbold{\isa{outdate} theory}, and \isa{remove}\indexbold{\isa{remove} theory}:
3.8 + The basic internal actions of the theory database are \isa{update}, \isa{outdate}, and \isa{remove}:
3.9
3.10 \begin{itemize}
3.11
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/doc-src/IsarImplementation/Thy/document/isabelle.sty Tue Jan 03 13:59:55 2006 +0100
4.3 @@ -0,0 +1,203 @@
4.4 +%%
4.5 +%%
4.6 +%%
4.7 +%% macros for Isabelle generated LaTeX output
4.8 +%%
4.9 +
4.10 +%%% Simple document preparation (based on theory token language and symbols)
4.11 +
4.12 +% isabelle environments
4.13 +
4.14 +\newcommand{\isabellecontext}{UNKNOWN}
4.15 +
4.16 +\newcommand{\isastyle}{\small\tt\slshape}
4.17 +\newcommand{\isastyleminor}{\small\tt\slshape}
4.18 +\newcommand{\isastylescript}{\footnotesize\tt\slshape}
4.19 +\newcommand{\isastyletext}{\normalsize\rm}
4.20 +\newcommand{\isastyletxt}{\rm}
4.21 +\newcommand{\isastylecmt}{\rm}
4.22 +
4.23 +%symbol markup -- \emph achieves decent spacing via italic corrections
4.24 +\newcommand{\isamath}[1]{\emph{$#1$}}
4.25 +\newcommand{\isatext}[1]{\emph{#1}}
4.26 +\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
4.27 +\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
4.28 +\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
4.29 +\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
4.30 +\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
4.31 +\newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}
4.32 +\newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup}
4.33 +\newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript}
4.34 +\newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}
4.35 +\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
4.36 +\newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}}
4.37 +
4.38 +
4.39 +\newdimen\isa@parindent\newdimen\isa@parskip
4.40 +
4.41 +\newenvironment{isabellebody}{%
4.42 +\isamarkuptrue\par%
4.43 +\isa@parindent\parindent\parindent0pt%
4.44 +\isa@parskip\parskip\parskip0pt%
4.45 +\isastyle}{\par}
4.46 +
4.47 +\newenvironment{isabelle}
4.48 +{\begin{trivlist}\begin{isabellebody}\item\relax}
4.49 +{\end{isabellebody}\end{trivlist}}
4.50 +
4.51 +\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
4.52 +
4.53 +\newcommand{\isaindent}[1]{\hphantom{#1}}
4.54 +\newcommand{\isanewline}{\mbox{}\par\mbox{}}
4.55 +\newcommand{\isasep}{}
4.56 +\newcommand{\isadigit}[1]{#1}
4.57 +
4.58 +\chardef\isacharbang=`\!
4.59 +\chardef\isachardoublequote=`\"
4.60 +\chardef\isachardoublequoteopen=`\"
4.61 +\chardef\isachardoublequoteclose=`\"
4.62 +\chardef\isacharhash=`\#
4.63 +\chardef\isachardollar=`\$
4.64 +\chardef\isacharpercent=`\%
4.65 +\chardef\isacharampersand=`\&
4.66 +\chardef\isacharprime=`\'
4.67 +\chardef\isacharparenleft=`\(
4.68 +\chardef\isacharparenright=`\)
4.69 +\chardef\isacharasterisk=`\*
4.70 +\chardef\isacharplus=`\+
4.71 +\chardef\isacharcomma=`\,
4.72 +\chardef\isacharminus=`\-
4.73 +\chardef\isachardot=`\.
4.74 +\chardef\isacharslash=`\/
4.75 +\chardef\isacharcolon=`\:
4.76 +\chardef\isacharsemicolon=`\;
4.77 +\chardef\isacharless=`\<
4.78 +\chardef\isacharequal=`\=
4.79 +\chardef\isachargreater=`\>
4.80 +\chardef\isacharquery=`\?
4.81 +\chardef\isacharat=`\@
4.82 +\chardef\isacharbrackleft=`\[
4.83 +\chardef\isacharbackslash=`\\
4.84 +\chardef\isacharbrackright=`\]
4.85 +\chardef\isacharcircum=`\^
4.86 +\chardef\isacharunderscore=`\_
4.87 +\chardef\isacharbackquote=`\`
4.88 +\chardef\isacharbackquoteopen=`\`
4.89 +\chardef\isacharbackquoteclose=`\`
4.90 +\chardef\isacharbraceleft=`\{
4.91 +\chardef\isacharbar=`\|
4.92 +\chardef\isacharbraceright=`\}
4.93 +\chardef\isachartilde=`\~
4.94 +\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}
4.95 +\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}
4.96 +
4.97 +
4.98 +% keyword and section markup
4.99 +
4.100 +\newcommand{\isakeywordcharunderscore}{\_}
4.101 +\newcommand{\isakeyword}[1]
4.102 +{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isakeywordcharunderscore}%
4.103 +\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
4.104 +\newcommand{\isacommand}[1]{\isakeyword{#1}}
4.105 +
4.106 +\newcommand{\isamarkupheader}[1]{\section{#1}}
4.107 +\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
4.108 +\newcommand{\isamarkupsection}[1]{\section{#1}}
4.109 +\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
4.110 +\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
4.111 +\newcommand{\isamarkupsect}[1]{\section{#1}}
4.112 +\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
4.113 +\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
4.114 +
4.115 +\newif\ifisamarkup
4.116 +\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
4.117 +\newcommand{\isaendpar}{\par\medskip}
4.118 +\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
4.119 +\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
4.120 +\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
4.121 +\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
4.122 +
4.123 +
4.124 +% alternative styles
4.125 +
4.126 +\newcommand{\isabellestyle}{}
4.127 +\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
4.128 +
4.129 +\newcommand{\isabellestylett}{%
4.130 +\renewcommand{\isastyle}{\small\tt}%
4.131 +\renewcommand{\isastyleminor}{\small\tt}%
4.132 +\renewcommand{\isastylescript}{\footnotesize\tt}%
4.133 +}
4.134 +\newcommand{\isabellestyleit}{%
4.135 +\renewcommand{\isastyle}{\small\it}%
4.136 +\renewcommand{\isastyleminor}{\it}%
4.137 +\renewcommand{\isastylescript}{\footnotesize\it}%
4.138 +\renewcommand{\isakeywordcharunderscore}{\mbox{-}}%
4.139 +\renewcommand{\isacharbang}{\isamath{!}}%
4.140 +\renewcommand{\isachardoublequote}{}%
4.141 +\renewcommand{\isachardoublequoteopen}{}%
4.142 +\renewcommand{\isachardoublequoteclose}{}%
4.143 +\renewcommand{\isacharhash}{\isamath{\#}}%
4.144 +\renewcommand{\isachardollar}{\isamath{\$}}%
4.145 +\renewcommand{\isacharpercent}{\isamath{\%}}%
4.146 +\renewcommand{\isacharampersand}{\isamath{\&}}%
4.147 +\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
4.148 +\renewcommand{\isacharparenleft}{\isamath{(}}%
4.149 +\renewcommand{\isacharparenright}{\isamath{)}}%
4.150 +\renewcommand{\isacharasterisk}{\isamath{*}}%
4.151 +\renewcommand{\isacharplus}{\isamath{+}}%
4.152 +\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
4.153 +\renewcommand{\isacharminus}{\isamath{-}}%
4.154 +\renewcommand{\isachardot}{\isamath{\mathord.}}%
4.155 +\renewcommand{\isacharslash}{\isamath{/}}%
4.156 +\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
4.157 +\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
4.158 +\renewcommand{\isacharless}{\isamath{<}}%
4.159 +\renewcommand{\isacharequal}{\isamath{=}}%
4.160 +\renewcommand{\isachargreater}{\isamath{>}}%
4.161 +\renewcommand{\isacharat}{\isamath{@}}%
4.162 +\renewcommand{\isacharbrackleft}{\isamath{[}}%
4.163 +\renewcommand{\isacharbackslash}{\isamath{\backslash}}%
4.164 +\renewcommand{\isacharbrackright}{\isamath{]}}%
4.165 +\renewcommand{\isacharunderscore}{\mbox{-}}%
4.166 +\renewcommand{\isacharbraceleft}{\isamath{\{}}%
4.167 +\renewcommand{\isacharbar}{\isamath{\mid}}%
4.168 +\renewcommand{\isacharbraceright}{\isamath{\}}}%
4.169 +\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
4.170 +\renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
4.171 +\renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
4.172 +\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}%
4.173 +\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}%
4.174 +}
4.175 +
4.176 +\newcommand{\isabellestylesl}{%
4.177 +\isabellestyleit%
4.178 +\renewcommand{\isastyle}{\small\sl}%
4.179 +\renewcommand{\isastyleminor}{\sl}%
4.180 +\renewcommand{\isastylescript}{\footnotesize\sl}%
4.181 +}
4.182 +
4.183 +
4.184 +% tagged regions
4.185 +
4.186 +%plain TeX version of comment package -- much faster!
4.187 +\let\isafmtname\fmtname\def\fmtname{plain}
4.188 +\usepackage{comment}
4.189 +\let\fmtname\isafmtname
4.190 +
4.191 +\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
4.192 +
4.193 +\newcommand{\isakeeptag}[1]%
4.194 +{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
4.195 +\newcommand{\isadroptag}[1]%
4.196 +{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
4.197 +\newcommand{\isafoldtag}[1]%
4.198 +{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
4.199 +
4.200 +\isakeeptag{theory}
4.201 +\isakeeptag{proof}
4.202 +\isakeeptag{ML}
4.203 +\isakeeptag{visible}
4.204 +\isadroptag{invisible}
4.205 +
4.206 +\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/doc-src/IsarImplementation/Thy/document/isabellesym.sty Tue Jan 03 13:59:55 2006 +0100
5.3 @@ -0,0 +1,359 @@
5.4 +%%
5.5 +%%
5.6 +%%
5.7 +%% definitions of standard Isabelle symbols
5.8 +%%
5.9 +
5.10 +\newcommand{\isasymzero}{\isamath{\mathbf{0}}} %requires amssymb
5.11 +\newcommand{\isasymone}{\isamath{\mathbf{1}}} %requires amssymb
5.12 +\newcommand{\isasymtwo}{\isamath{\mathbf{2}}} %requires amssymb
5.13 +\newcommand{\isasymthree}{\isamath{\mathbf{3}}} %requires amssymb
5.14 +\newcommand{\isasymfour}{\isamath{\mathbf{4}}} %requires amssymb
5.15 +\newcommand{\isasymfive}{\isamath{\mathbf{5}}} %requires amssymb
5.16 +\newcommand{\isasymsix}{\isamath{\mathbf{6}}} %requires amssymb
5.17 +\newcommand{\isasymseven}{\isamath{\mathbf{7}}} %requires amssymb
5.18 +\newcommand{\isasymeight}{\isamath{\mathbf{8}}} %requires amssymb
5.19 +\newcommand{\isasymnine}{\isamath{\mathbf{9}}} %requires amssymb
5.20 +\newcommand{\isasymA}{\isamath{\mathcal{A}}}
5.21 +\newcommand{\isasymB}{\isamath{\mathcal{B}}}
5.22 +\newcommand{\isasymC}{\isamath{\mathcal{C}}}
5.23 +\newcommand{\isasymD}{\isamath{\mathcal{D}}}
5.24 +\newcommand{\isasymE}{\isamath{\mathcal{E}}}
5.25 +\newcommand{\isasymF}{\isamath{\mathcal{F}}}
5.26 +\newcommand{\isasymG}{\isamath{\mathcal{G}}}
5.27 +\newcommand{\isasymH}{\isamath{\mathcal{H}}}
5.28 +\newcommand{\isasymI}{\isamath{\mathcal{I}}}
5.29 +\newcommand{\isasymJ}{\isamath{\mathcal{J}}}
5.30 +\newcommand{\isasymK}{\isamath{\mathcal{K}}}
5.31 +\newcommand{\isasymL}{\isamath{\mathcal{L}}}
5.32 +\newcommand{\isasymM}{\isamath{\mathcal{M}}}
5.33 +\newcommand{\isasymN}{\isamath{\mathcal{N}}}
5.34 +\newcommand{\isasymO}{\isamath{\mathcal{O}}}
5.35 +\newcommand{\isasymP}{\isamath{\mathcal{P}}}
5.36 +\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}
5.37 +\newcommand{\isasymR}{\isamath{\mathcal{R}}}
5.38 +\newcommand{\isasymS}{\isamath{\mathcal{S}}}
5.39 +\newcommand{\isasymT}{\isamath{\mathcal{T}}}
5.40 +\newcommand{\isasymU}{\isamath{\mathcal{U}}}
5.41 +\newcommand{\isasymV}{\isamath{\mathcal{V}}}
5.42 +\newcommand{\isasymW}{\isamath{\mathcal{W}}}
5.43 +\newcommand{\isasymX}{\isamath{\mathcal{X}}}
5.44 +\newcommand{\isasymY}{\isamath{\mathcal{Y}}}
5.45 +\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
5.46 +\newcommand{\isasyma}{\isamath{\mathrm{a}}}
5.47 +\newcommand{\isasymb}{\isamath{\mathrm{b}}}
5.48 +\newcommand{\isasymc}{\isamath{\mathrm{c}}}
5.49 +\newcommand{\isasymd}{\isamath{\mathrm{d}}}
5.50 +\newcommand{\isasyme}{\isamath{\mathrm{e}}}
5.51 +\newcommand{\isasymf}{\isamath{\mathrm{f}}}
5.52 +\newcommand{\isasymg}{\isamath{\mathrm{g}}}
5.53 +\newcommand{\isasymh}{\isamath{\mathrm{h}}}
5.54 +\newcommand{\isasymi}{\isamath{\mathrm{i}}}
5.55 +\newcommand{\isasymj}{\isamath{\mathrm{j}}}
5.56 +\newcommand{\isasymk}{\isamath{\mathrm{k}}}
5.57 +\newcommand{\isasyml}{\isamath{\mathrm{l}}}
5.58 +\newcommand{\isasymm}{\isamath{\mathrm{m}}}
5.59 +\newcommand{\isasymn}{\isamath{\mathrm{n}}}
5.60 +\newcommand{\isasymo}{\isamath{\mathrm{o}}}
5.61 +\newcommand{\isasymp}{\isamath{\mathrm{p}}}
5.62 +\newcommand{\isasymq}{\isamath{\mathrm{q}}}
5.63 +\newcommand{\isasymr}{\isamath{\mathrm{r}}}
5.64 +\newcommand{\isasyms}{\isamath{\mathrm{s}}}
5.65 +\newcommand{\isasymt}{\isamath{\mathrm{t}}}
5.66 +\newcommand{\isasymu}{\isamath{\mathrm{u}}}
5.67 +\newcommand{\isasymv}{\isamath{\mathrm{v}}}
5.68 +\newcommand{\isasymw}{\isamath{\mathrm{w}}}
5.69 +\newcommand{\isasymx}{\isamath{\mathrm{x}}}
5.70 +\newcommand{\isasymy}{\isamath{\mathrm{y}}}
5.71 +\newcommand{\isasymz}{\isamath{\mathrm{z}}}
5.72 +\newcommand{\isasymAA}{\isamath{\mathfrak{A}}} %requires eufrak
5.73 +\newcommand{\isasymBB}{\isamath{\mathfrak{B}}} %requires eufrak
5.74 +\newcommand{\isasymCC}{\isamath{\mathfrak{C}}} %requires eufrak
5.75 +\newcommand{\isasymDD}{\isamath{\mathfrak{D}}} %requires eufrak
5.76 +\newcommand{\isasymEE}{\isamath{\mathfrak{E}}} %requires eufrak
5.77 +\newcommand{\isasymFF}{\isamath{\mathfrak{F}}} %requires eufrak
5.78 +\newcommand{\isasymGG}{\isamath{\mathfrak{G}}} %requires eufrak
5.79 +\newcommand{\isasymHH}{\isamath{\mathfrak{H}}} %requires eufrak
5.80 +\newcommand{\isasymII}{\isamath{\mathfrak{I}}} %requires eufrak
5.81 +\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}} %requires eufrak
5.82 +\newcommand{\isasymKK}{\isamath{\mathfrak{K}}} %requires eufrak
5.83 +\newcommand{\isasymLL}{\isamath{\mathfrak{L}}} %requires eufrak
5.84 +\newcommand{\isasymMM}{\isamath{\mathfrak{M}}} %requires eufrak
5.85 +\newcommand{\isasymNN}{\isamath{\mathfrak{N}}} %requires eufrak
5.86 +\newcommand{\isasymOO}{\isamath{\mathfrak{O}}} %requires eufrak
5.87 +\newcommand{\isasymPP}{\isamath{\mathfrak{P}}} %requires eufrak
5.88 +\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}} %requires eufrak
5.89 +\newcommand{\isasymRR}{\isamath{\mathfrak{R}}} %requires eufrak
5.90 +\newcommand{\isasymSS}{\isamath{\mathfrak{S}}} %requires eufrak
5.91 +\newcommand{\isasymTT}{\isamath{\mathfrak{T}}} %requires eufrak
5.92 +\newcommand{\isasymUU}{\isamath{\mathfrak{U}}} %requires eufrak
5.93 +\newcommand{\isasymVV}{\isamath{\mathfrak{V}}} %requires eufrak
5.94 +\newcommand{\isasymWW}{\isamath{\mathfrak{W}}} %requires eufrak
5.95 +\newcommand{\isasymXX}{\isamath{\mathfrak{X}}} %requires eufrak
5.96 +\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}} %requires eufrak
5.97 +\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}} %requires eufrak
5.98 +\newcommand{\isasymaa}{\isamath{\mathfrak{a}}} %requires eufrak
5.99 +\newcommand{\isasymbb}{\isamath{\mathfrak{b}}} %requires eufrak
5.100 +\newcommand{\isasymcc}{\isamath{\mathfrak{c}}} %requires eufrak
5.101 +\newcommand{\isasymdd}{\isamath{\mathfrak{d}}} %requires eufrak
5.102 +\newcommand{\isasymee}{\isamath{\mathfrak{e}}} %requires eufrak
5.103 +\newcommand{\isasymff}{\isamath{\mathfrak{f}}} %requires eufrak
5.104 +\newcommand{\isasymgg}{\isamath{\mathfrak{g}}} %requires eufrak
5.105 +\newcommand{\isasymhh}{\isamath{\mathfrak{h}}} %requires eufrak
5.106 +\newcommand{\isasymii}{\isamath{\mathfrak{i}}} %requires eufrak
5.107 +\newcommand{\isasymjj}{\isamath{\mathfrak{j}}} %requires eufrak
5.108 +\newcommand{\isasymkk}{\isamath{\mathfrak{k}}} %requires eufrak
5.109 +\newcommand{\isasymll}{\isamath{\mathfrak{l}}} %requires eufrak
5.110 +\newcommand{\isasymmm}{\isamath{\mathfrak{m}}} %requires eufrak
5.111 +\newcommand{\isasymnn}{\isamath{\mathfrak{n}}} %requires eufrak
5.112 +\newcommand{\isasymoo}{\isamath{\mathfrak{o}}} %requires eufrak
5.113 +\newcommand{\isasympp}{\isamath{\mathfrak{p}}} %requires eufrak
5.114 +\newcommand{\isasymqq}{\isamath{\mathfrak{q}}} %requires eufrak
5.115 +\newcommand{\isasymrr}{\isamath{\mathfrak{r}}} %requires eufrak
5.116 +\newcommand{\isasymss}{\isamath{\mathfrak{s}}} %requires eufrak
5.117 +\newcommand{\isasymtt}{\isamath{\mathfrak{t}}} %requires eufrak
5.118 +\newcommand{\isasymuu}{\isamath{\mathfrak{u}}} %requires eufrak
5.119 +\newcommand{\isasymvv}{\isamath{\mathfrak{v}}} %requires eufrak
5.120 +\newcommand{\isasymww}{\isamath{\mathfrak{w}}} %requires eufrak
5.121 +\newcommand{\isasymxx}{\isamath{\mathfrak{x}}} %requires eufrak
5.122 +\newcommand{\isasymyy}{\isamath{\mathfrak{y}}} %requires eufrak
5.123 +\newcommand{\isasymzz}{\isamath{\mathfrak{z}}} %requires eufrak
5.124 +\newcommand{\isasymalpha}{\isamath{\alpha}}
5.125 +\newcommand{\isasymbeta}{\isamath{\beta}}
5.126 +\newcommand{\isasymgamma}{\isamath{\gamma}}
5.127 +\newcommand{\isasymdelta}{\isamath{\delta}}
5.128 +\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
5.129 +\newcommand{\isasymzeta}{\isamath{\zeta}}
5.130 +\newcommand{\isasymeta}{\isamath{\eta}}
5.131 +\newcommand{\isasymtheta}{\isamath{\vartheta}}
5.132 +\newcommand{\isasymiota}{\isamath{\iota}}
5.133 +\newcommand{\isasymkappa}{\isamath{\kappa}}
5.134 +\newcommand{\isasymlambda}{\isamath{\lambda}}
5.135 +\newcommand{\isasymmu}{\isamath{\mu}}
5.136 +\newcommand{\isasymnu}{\isamath{\nu}}
5.137 +\newcommand{\isasymxi}{\isamath{\xi}}
5.138 +\newcommand{\isasympi}{\isamath{\pi}}
5.139 +\newcommand{\isasymrho}{\isamath{\varrho}}
5.140 +\newcommand{\isasymsigma}{\isamath{\sigma}}
5.141 +\newcommand{\isasymtau}{\isamath{\tau}}
5.142 +\newcommand{\isasymupsilon}{\isamath{\upsilon}}
5.143 +\newcommand{\isasymphi}{\isamath{\varphi}}
5.144 +\newcommand{\isasymchi}{\isamath{\chi}}
5.145 +\newcommand{\isasympsi}{\isamath{\psi}}
5.146 +\newcommand{\isasymomega}{\isamath{\omega}}
5.147 +\newcommand{\isasymGamma}{\isamath{\Gamma}}
5.148 +\newcommand{\isasymDelta}{\isamath{\Delta}}
5.149 +\newcommand{\isasymTheta}{\isamath{\Theta}}
5.150 +\newcommand{\isasymLambda}{\isamath{\Lambda}}
5.151 +\newcommand{\isasymXi}{\isamath{\Xi}}
5.152 +\newcommand{\isasymPi}{\isamath{\Pi}}
5.153 +\newcommand{\isasymSigma}{\isamath{\Sigma}}
5.154 +\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
5.155 +\newcommand{\isasymPhi}{\isamath{\Phi}}
5.156 +\newcommand{\isasymPsi}{\isamath{\Psi}}
5.157 +\newcommand{\isasymOmega}{\isamath{\Omega}}
5.158 +\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
5.159 +\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
5.160 +\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
5.161 +\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
5.162 +\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
5.163 +\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
5.164 +\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
5.165 +\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
5.166 +\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
5.167 +\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
5.168 +\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
5.169 +\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
5.170 +\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
5.171 +\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
5.172 +\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
5.173 +\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
5.174 +\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
5.175 +\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
5.176 +\newcommand{\isasymmapsto}{\isamath{\mapsto}}
5.177 +\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
5.178 +\newcommand{\isasymmidarrow}{\isamath{\relbar}}
5.179 +\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
5.180 +\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
5.181 +\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
5.182 +\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
5.183 +\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
5.184 +\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
5.185 +\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
5.186 +\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
5.187 +\newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}} %requires amssymb
5.188 +\newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}} %requires amssymb
5.189 +\newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}} %requires amssymb
5.190 +\newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}} %requires amssymb
5.191 +\newcommand{\isasymrestriction}{\isamath{\restriction}} %requires amssymb
5.192 +\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb
5.193 +\newcommand{\isasymup}{\isamath{\uparrow}}
5.194 +\newcommand{\isasymUp}{\isamath{\Uparrow}}
5.195 +\newcommand{\isasymdown}{\isamath{\downarrow}}
5.196 +\newcommand{\isasymDown}{\isamath{\Downarrow}}
5.197 +\newcommand{\isasymupdown}{\isamath{\updownarrow}}
5.198 +\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
5.199 +\newcommand{\isasymlangle}{\isamath{\langle}}
5.200 +\newcommand{\isasymrangle}{\isamath{\rangle}}
5.201 +\newcommand{\isasymlceil}{\isamath{\lceil}}
5.202 +\newcommand{\isasymrceil}{\isamath{\rceil}}
5.203 +\newcommand{\isasymlfloor}{\isamath{\lfloor}}
5.204 +\newcommand{\isasymrfloor}{\isamath{\rfloor}}
5.205 +\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
5.206 +\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}
5.207 +\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
5.208 +\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
5.209 +\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
5.210 +\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
5.211 +\newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel
5.212 +\newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel
5.213 +\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
5.214 +\newcommand{\isasymnot}{\isamath{\neg}}
5.215 +\newcommand{\isasymbottom}{\isamath{\bot}}
5.216 +\newcommand{\isasymtop}{\isamath{\top}}
5.217 +\newcommand{\isasymand}{\isamath{\wedge}}
5.218 +\newcommand{\isasymAnd}{\isamath{\bigwedge}}
5.219 +\newcommand{\isasymor}{\isamath{\vee}}
5.220 +\newcommand{\isasymOr}{\isamath{\bigvee}}
5.221 +\newcommand{\isasymforall}{\isamath{\forall\,}}
5.222 +\newcommand{\isasymexists}{\isamath{\exists\,}}
5.223 +\newcommand{\isasymnexists}{\isamath{\nexists\,}} %requires amssymb
5.224 +\newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb
5.225 +\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb
5.226 +\newcommand{\isasymturnstile}{\isamath{\vdash}}
5.227 +\newcommand{\isasymTurnstile}{\isamath{\models}}
5.228 +\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
5.229 +\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
5.230 +\newcommand{\isasymstileturn}{\isamath{\dashv}}
5.231 +\newcommand{\isasymsurd}{\isamath{\surd}}
5.232 +\newcommand{\isasymle}{\isamath{\le}}
5.233 +\newcommand{\isasymge}{\isamath{\ge}}
5.234 +\newcommand{\isasymlless}{\isamath{\ll}}
5.235 +\newcommand{\isasymggreater}{\isamath{\gg}}
5.236 +\newcommand{\isasymlesssim}{\isamath{\lesssim}} %requires amssymb
5.237 +\newcommand{\isasymgreatersim}{\isamath{\gtrsim}} %requires amssymb
5.238 +\newcommand{\isasymlessapprox}{\isamath{\lessapprox}} %requires amssymb
5.239 +\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}} %requires amssymb
5.240 +\newcommand{\isasymin}{\isamath{\in}}
5.241 +\newcommand{\isasymnotin}{\isamath{\notin}}
5.242 +\newcommand{\isasymsubset}{\isamath{\subset}}
5.243 +\newcommand{\isasymsupset}{\isamath{\supset}}
5.244 +\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
5.245 +\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
5.246 +\newcommand{\isasymsqsubset}{\isamath{\sqsubset}} %requires amssymb
5.247 +\newcommand{\isasymsqsupset}{\isamath{\sqsupset}} %requires amssymb
5.248 +\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
5.249 +\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
5.250 +\newcommand{\isasyminter}{\isamath{\cap}}
5.251 +\newcommand{\isasymInter}{\isamath{\bigcap\,}}
5.252 +\newcommand{\isasymunion}{\isamath{\cup}}
5.253 +\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
5.254 +\newcommand{\isasymsqunion}{\isamath{\sqcup}}
5.255 +\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
5.256 +\newcommand{\isasymsqinter}{\isamath{\sqcap}}
5.257 +\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires amsmath
5.258 +\newcommand{\isasymuplus}{\isamath{\uplus}}
5.259 +\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
5.260 +\newcommand{\isasymnoteq}{\isamath{\not=}}
5.261 +\newcommand{\isasymsim}{\isamath{\sim}}
5.262 +\newcommand{\isasymdoteq}{\isamath{\doteq}}
5.263 +\newcommand{\isasymsimeq}{\isamath{\simeq}}
5.264 +\newcommand{\isasymapprox}{\isamath{\approx}}
5.265 +\newcommand{\isasymasymp}{\isamath{\asymp}}
5.266 +\newcommand{\isasymcong}{\isamath{\cong}}
5.267 +\newcommand{\isasymsmile}{\isamath{\smile}}
5.268 +\newcommand{\isasymequiv}{\isamath{\equiv}}
5.269 +\newcommand{\isasymfrown}{\isamath{\frown}}
5.270 +\newcommand{\isasympropto}{\isamath{\propto}}
5.271 +\newcommand{\isasymsome}{\isamath{\epsilon\,}}
5.272 +\newcommand{\isasymJoin}{\isamath{\Join}} %requires amssymb
5.273 +\newcommand{\isasymbowtie}{\isamath{\bowtie}}
5.274 +\newcommand{\isasymprec}{\isamath{\prec}}
5.275 +\newcommand{\isasymsucc}{\isamath{\succ}}
5.276 +\newcommand{\isasympreceq}{\isamath{\preceq}}
5.277 +\newcommand{\isasymsucceq}{\isamath{\succeq}}
5.278 +\newcommand{\isasymparallel}{\isamath{\parallel}}
5.279 +\newcommand{\isasymbar}{\isamath{\mid}}
5.280 +\newcommand{\isasymplusminus}{\isamath{\pm}}
5.281 +\newcommand{\isasymminusplus}{\isamath{\mp}}
5.282 +\newcommand{\isasymtimes}{\isamath{\times}}
5.283 +\newcommand{\isasymdiv}{\isamath{\div}}
5.284 +\newcommand{\isasymcdot}{\isamath{\cdot}}
5.285 +\newcommand{\isasymstar}{\isamath{\star}}
5.286 +\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
5.287 +\newcommand{\isasymcirc}{\isamath{\circ}}
5.288 +\newcommand{\isasymdagger}{\isamath{\dagger}}
5.289 +\newcommand{\isasymddagger}{\isamath{\ddagger}}
5.290 +\newcommand{\isasymlhd}{\isamath{\lhd}} %requires amssymb
5.291 +\newcommand{\isasymrhd}{\isamath{\rhd}} %requires amssymb
5.292 +\newcommand{\isasymunlhd}{\isamath{\unlhd}} %requires amssymb
5.293 +\newcommand{\isasymunrhd}{\isamath{\unrhd}} %requires amssymb
5.294 +\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
5.295 +\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
5.296 +\newcommand{\isasymtriangle}{\isamath{\triangle}}
5.297 +\newcommand{\isasymtriangleq}{\isamath{\triangleq}} %requires amssymb
5.298 +\newcommand{\isasymoplus}{\isamath{\oplus}}
5.299 +\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}
5.300 +\newcommand{\isasymotimes}{\isamath{\otimes}}
5.301 +\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}
5.302 +\newcommand{\isasymodot}{\isamath{\odot}}
5.303 +\newcommand{\isasymOdot}{\isamath{\bigodot\,}}
5.304 +\newcommand{\isasymominus}{\isamath{\ominus}}
5.305 +\newcommand{\isasymoslash}{\isamath{\oslash}}
5.306 +\newcommand{\isasymdots}{\isamath{\dots}}
5.307 +\newcommand{\isasymcdots}{\isamath{\cdots}}
5.308 +\newcommand{\isasymSum}{\isamath{\sum\,}}
5.309 +\newcommand{\isasymProd}{\isamath{\prod\,}}
5.310 +\newcommand{\isasymCoprod}{\isamath{\coprod\,}}
5.311 +\newcommand{\isasyminfinity}{\isamath{\infty}}
5.312 +\newcommand{\isasymintegral}{\isamath{\int\,}}
5.313 +\newcommand{\isasymointegral}{\isamath{\oint\,}}
5.314 +\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
5.315 +\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
5.316 +\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
5.317 +\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
5.318 +\newcommand{\isasymaleph}{\isamath{\aleph}}
5.319 +\newcommand{\isasymemptyset}{\isamath{\emptyset}}
5.320 +\newcommand{\isasymnabla}{\isamath{\nabla}}
5.321 +\newcommand{\isasympartial}{\isamath{\partial}}
5.322 +\newcommand{\isasymRe}{\isamath{\Re}}
5.323 +\newcommand{\isasymIm}{\isamath{\Im}}
5.324 +\newcommand{\isasymflat}{\isamath{\flat}}
5.325 +\newcommand{\isasymnatural}{\isamath{\natural}}
5.326 +\newcommand{\isasymsharp}{\isamath{\sharp}}
5.327 +\newcommand{\isasymangle}{\isamath{\angle}}
5.328 +\newcommand{\isasymcopyright}{\isatext{\rm\copyright}}
5.329 +\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
5.330 +\newcommand{\isasymhyphen}{\isatext{\rm-}}
5.331 +\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
5.332 +\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}} %requires latin1
5.333 +\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}} %requires latin1
5.334 +\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}} %requires latin1
5.335 +\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}} %requires latin1
5.336 +\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}} %requires latin1
5.337 +\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}} %requires latin1
5.338 +\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
5.339 +\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
5.340 +\newcommand{\isasymsection}{\isatext{\rm\S}}
5.341 +\newcommand{\isasymparagraph}{\isatext{\rm\P}}
5.342 +\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
5.343 +\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
5.344 +\newcommand{\isasymeuro}{\isatext{\textgreek{\euro}}} %requires greek babel
5.345 +\newcommand{\isasympounds}{\isamath{\pounds}}
5.346 +\newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb
5.347 +\newcommand{\isasymcent}{\isatext{\textcent}} %requires textcomp
5.348 +\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
5.349 +\newcommand{\isasymdegree}{\isatext{\rm\textdegree}} %requires latin1
5.350 +\newcommand{\isasymamalg}{\isamath{\amalg}}
5.351 +\newcommand{\isasymmho}{\isamath{\mho}} %requires amssymb
5.352 +\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssymb
5.353 +\newcommand{\isasymwp}{\isamath{\wp}}
5.354 +\newcommand{\isasymwrong}{\isamath{\wr}}
5.355 +\newcommand{\isasymstruct}{\isamath{\diamond}}
5.356 +\newcommand{\isasymacute}{\isatext{\'\relax}}
5.357 +\newcommand{\isasymindex}{\isatext{\i}}
5.358 +\newcommand{\isasymdieresis}{\isatext{\"\relax}}
5.359 +\newcommand{\isasymcedilla}{\isatext{\c\relax}}
5.360 +\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
5.361 +\newcommand{\isasymspacespace}{\isamath{~~}}
5.362 +\newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}
6.1 --- a/doc-src/IsarImplementation/Thy/document/prelim.tex Tue Jan 03 11:57:33 2006 +0100
6.2 +++ b/doc-src/IsarImplementation/Thy/document/prelim.tex Tue Jan 03 13:59:55 2006 +0100
6.3 @@ -261,23 +261,20 @@
6.4 like wood or stone.
6.5
6.6 Isabelle/Isar distinguishes two key notions of context: \emph{theory
6.7 - context}\indexbold{theory context} and \emph{proof context}.\indexbold{proof
6.8 - context} To motivate this fundamental division consider the very idea of
6.9 -logical reasoning which is about judgments $\Gamma \Drv{\Theta} \phi$, where
6.10 -$\Theta$ is the background theory with declarations of operators and axioms
6.11 -stating their properties, and $\Gamma$ a collection of hypotheses emerging
6.12 -temporarily during proof. For example, the rule of implication-introduction
6.13 -\[
6.14 -\infer{\Gamma \Drv{\Theta} A \Imp B}{\Gamma, A \Drv{\Theta} B}
6.15 -\]
6.16 -can be read as ``to show $A \Imp B$ we may assume $A$ as hypothesis and need
6.17 -to show $B$''. It is characteristic that $\Theta$ is unchanged and $\Gamma$
6.18 -is only modified according to some general patterns of ``assuming'' and
6.19 -``discharging'' hypotheses. This admits the following abbreviated notation,
6.20 -where the fixed $\Theta$ and locally changed $\Gamma$ are left implicit:
6.21 -\[
6.22 -\infer{A \Imp B}{\infer*{B}{[A]}}
6.23 -\]
6.24 +context} and \emph{proof context}. To motivate this fundamental
6.25 +division consider the very idea of logical reasoning which is about
6.26 +judgments $\Gamma \Drv{\Theta} \phi$, where $\Theta$ is the background
6.27 +theory with declarations of operators and axioms stating their
6.28 +properties, and $\Gamma$ a collection of hypotheses emerging
6.29 +temporarily during proof. For example, the rule of
6.30 +implication-introduction \[ \infer{\Gamma \Drv{\Theta} A \Imp
6.31 +B}{\Gamma, A \Drv{\Theta} B} \] can be read as ``to show $A \Imp B$ we
6.32 +may assume $A$ as hypothesis and need to show $B$''. It is
6.33 +characteristic that $\Theta$ is unchanged and $\Gamma$ is only
6.34 +modified according to some general patterns of ``assuming'' and
6.35 +``discharging'' hypotheses. This admits the following abbreviated
6.36 +notation, where the fixed $\Theta$ and locally changed $\Gamma$ are
6.37 +left implicit: \[ \infer{A \Imp B}{\infer*{B}{[A]}} \]
6.38
6.39 In some logical traditions (e.g.\ Type Theory) there is a tendency to
6.40 unify all kinds of declarations within a single notion of context.
7.1 --- a/doc-src/IsarImplementation/Thy/integration.thy Tue Jan 03 11:57:33 2006 +0100
7.2 +++ b/doc-src/IsarImplementation/Thy/integration.thy Tue Jan 03 13:59:55 2006 +0100
7.3 @@ -321,9 +321,7 @@
7.4 scripts.
7.5
7.6 The basic internal actions of the theory database are @{text
7.7 - "update"}\indexbold{@{text "update"} theory}, @{text
7.8 - "outdate"}\indexbold{@{text "outdate"} theory}, and @{text
7.9 - "remove"}\indexbold{@{text "remove"} theory}:
7.10 + "update"}, @{text "outdate"}, and @{text "remove"}:
7.11
7.12 \begin{itemize}
7.13
8.1 --- a/doc-src/IsarImplementation/Thy/prelim.thy Tue Jan 03 11:57:33 2006 +0100
8.2 +++ b/doc-src/IsarImplementation/Thy/prelim.thy Tue Jan 03 13:59:55 2006 +0100
8.3 @@ -189,23 +189,20 @@
8.4 like wood or stone.
8.5
8.6 Isabelle/Isar distinguishes two key notions of context: \emph{theory
8.7 - context}\indexbold{theory context} and \emph{proof context}.\indexbold{proof
8.8 - context} To motivate this fundamental division consider the very idea of
8.9 -logical reasoning which is about judgments $\Gamma \Drv{\Theta} \phi$, where
8.10 -$\Theta$ is the background theory with declarations of operators and axioms
8.11 -stating their properties, and $\Gamma$ a collection of hypotheses emerging
8.12 -temporarily during proof. For example, the rule of implication-introduction
8.13 -\[
8.14 -\infer{\Gamma \Drv{\Theta} A \Imp B}{\Gamma, A \Drv{\Theta} B}
8.15 -\]
8.16 -can be read as ``to show $A \Imp B$ we may assume $A$ as hypothesis and need
8.17 -to show $B$''. It is characteristic that $\Theta$ is unchanged and $\Gamma$
8.18 -is only modified according to some general patterns of ``assuming'' and
8.19 -``discharging'' hypotheses. This admits the following abbreviated notation,
8.20 -where the fixed $\Theta$ and locally changed $\Gamma$ are left implicit:
8.21 -\[
8.22 -\infer{A \Imp B}{\infer*{B}{[A]}}
8.23 -\]
8.24 +context} and \emph{proof context}. To motivate this fundamental
8.25 +division consider the very idea of logical reasoning which is about
8.26 +judgments $\Gamma \Drv{\Theta} \phi$, where $\Theta$ is the background
8.27 +theory with declarations of operators and axioms stating their
8.28 +properties, and $\Gamma$ a collection of hypotheses emerging
8.29 +temporarily during proof. For example, the rule of
8.30 +implication-introduction \[ \infer{\Gamma \Drv{\Theta} A \Imp
8.31 +B}{\Gamma, A \Drv{\Theta} B} \] can be read as ``to show $A \Imp B$ we
8.32 +may assume $A$ as hypothesis and need to show $B$''. It is
8.33 +characteristic that $\Theta$ is unchanged and $\Gamma$ is only
8.34 +modified according to some general patterns of ``assuming'' and
8.35 +``discharging'' hypotheses. This admits the following abbreviated
8.36 +notation, where the fixed $\Theta$ and locally changed $\Gamma$ are
8.37 +left implicit: \[ \infer{A \Imp B}{\infer*{B}{[A]}} \]
8.38
8.39 In some logical traditions (e.g.\ Type Theory) there is a tendency to
8.40 unify all kinds of declarations within a single notion of context.
9.1 --- a/doc-src/IsarImplementation/implementation.tex Tue Jan 03 11:57:33 2006 +0100
9.2 +++ b/doc-src/IsarImplementation/implementation.tex Tue Jan 03 13:59:55 2006 +0100
9.3 @@ -49,7 +49,13 @@
9.4 % formal specification. But university departments are not software houses. Programs like
9.5 % Isabelle are not products: when they have served their purpose, they are discarded.
9.6 %
9.7 -% L.C. Paulson, Isabelle: The Next 700 Theorem Provers
9.8 +% L.C. Paulson, ``Isabelle: The Next 700 Theorem Provers''
9.9 +
9.10 +% As I did 20 years ago, I still fervently believe that the only way to
9.11 +% make software secure, reliable, and fast is to make it small. Fight
9.12 +% Features.
9.13 +%
9.14 +% Andrew S. Tanenbaum
9.15
9.16 \appendix
9.17 \input{Thy/document/ML.tex}
10.1 --- a/doc-src/IsarImplementation/style.sty Tue Jan 03 11:57:33 2006 +0100
10.2 +++ b/doc-src/IsarImplementation/style.sty Tue Jan 03 13:59:55 2006 +0100
10.3 @@ -2,7 +2,8 @@
10.4 %% $Id$
10.5
10.6 %% toc
10.7 -\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}}
10.8 +\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
10.9 +\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
10.10
10.11 %% references
10.12 \newcommand{\secref}[1]{\S\ref{#1}}
10.13 @@ -11,10 +12,17 @@
10.14 %% glossary
10.15 \renewcommand{\glossary}[2]{\nomenclature{\bf #1}{#2}}
10.16 \newcommand{\seeglossary}[1]{\emph{#1}}
10.17 -\def\glossaryname{Glossary}
10.18 +\newcommand{\glossaryname}{Glossary}
10.19 \renewcommand{\nomname}{\glossaryname}
10.20 \renewcommand{\pagedeclaration}[1]{\nobreak\quad\dotfill~page~\bold{#1}}
10.21
10.22 +%% index
10.23 +\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
10.24 +\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
10.25 +\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
10.26 +\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
10.27 +
10.28 +
10.29 \newcommand{\drv}{\mathrel{\vdash}}
10.30 \newcommand{\edrv}{\mathop{\drv}\nolimits}
10.31 \newcommand{\Drv}[1]{\mathrel{\vdash_{#1}}}
10.32 @@ -37,11 +45,6 @@
10.33 \renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
10.34 \renewcommand{\endisatagmlref}{\endgroup}
10.35
10.36 -\newcommand{\indexml}[1]{\index{\emph{#1} ({\ML})|bold}}
10.37 -\newcommand{\indexmltype}[1]{\index{\emph{#1} ({\ML} type)|bold}}
10.38 -\newcommand{\indexmlstructure}[1]{\index{\emph{#1} ({\ML} structure)|bold}}
10.39 -\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} ({\ML} functor)|bold}}
10.40 -
10.41 \newcommand{\isasymTHEORY}{\isakeyword{theory}}
10.42 \newcommand{\isasymIMPORTS}{\isakeyword{imports}}
10.43 \newcommand{\isasymUSES}{\isakeyword{uses}}