equal
deleted
inserted
replaced
192 |
192 |
193 \begin{itemize} |
193 \begin{itemize} |
194 \item @{text t}, @{text u}, @{text trm} for (raw) terms; ML-type: @{ML_type term} |
194 \item @{text t}, @{text u}, @{text trm} for (raw) terms; ML-type: @{ML_type term} |
195 \item @{text ct}, @{text cu} for certified terms; ML-type: @{ML_type cterm} |
195 \item @{text ct}, @{text cu} for certified terms; ML-type: @{ML_type cterm} |
196 \item @{text "ty"}, @{text T}, @{text U} for (raw) types; ML-type: @{ML_type typ} |
196 \item @{text "ty"}, @{text T}, @{text U} for (raw) types; ML-type: @{ML_type typ} |
|
197 \item @{text "S"} for sorts; ML-type: @{ML_type sort} |
197 \item @{text th}, @{text thm} for theorems; ML-type: @{ML_type thm} |
198 \item @{text th}, @{text thm} for theorems; ML-type: @{ML_type thm} |
198 \item @{text "foo_tac"} for tactics; ML-type: @{ML_type tactic} |
199 \item @{text "foo_tac"} for tactics; ML-type: @{ML_type tactic} |
199 \item @{text thy} for theories; ML-type: @{ML_type theory} |
200 \item @{text thy} for theories; ML-type: @{ML_type theory} |
200 \item @{text ctxt} for proof contexts; ML-type: @{ML_type Proof.context} |
201 \item @{text ctxt} for proof contexts; ML-type: @{ML_type Proof.context} |
201 \item @{text lthy} for local theories; ML-type: @{ML_type local_theory} |
202 \item @{text lthy} for local theories; ML-type: @{ML_type local_theory} |
224 \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, |
225 \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, |
225 \ref{rec:external} and \ref{rec:oracle}. He also wrote section \ref{sec:conversion} |
226 \ref{rec:external} and \ref{rec:oracle}. He also wrote section \ref{sec:conversion} |
226 and helped with recipe \ref{rec:timing}. Parts of section \ref{sec:storing} |
227 and helped with recipe \ref{rec:timing}. Parts of section \ref{sec:storing} |
227 are by him. |
228 are by him. |
228 |
229 |
|
230 \item {\bf Lukas Bulwahn} made me aware of the problems with recursive |
|
231 parsers. |
|
232 |
229 \item {\bf Jeremy Dawson} wrote the first version of the chapter |
233 \item {\bf Jeremy Dawson} wrote the first version of the chapter |
230 about parsing. |
234 about parsing. |
231 |
235 |
232 \item {\bf Armin Heller} helped with recipe \ref{rec:sat}. |
236 \item {\bf Armin Heller} helped with recipe \ref{rec:sat}. |
233 |
237 |
253 This document (version \input{tip}\hspace{-0.5ex}) was compiled with:\\ |
257 This document (version \input{tip}\hspace{-0.5ex}) was compiled with:\\ |
254 \input{version}\\ |
258 \input{version}\\ |
255 \input{pversion} |
259 \input{pversion} |
256 *} |
260 *} |
257 |
261 |
258 |
|
259 |
|
260 end |
262 end |