final Springer version
authorlcp
Tue May 03 18:38:28 1994 +0200 (1994-05-03)
changeset 359b5a2e9503a7a
parent 358 df8f0fbf7dbd
child 360 2b74eebdbdb8
final Springer version
doc-src/Intro/intro.bbl
doc-src/Intro/intro.ind
doc-src/Intro/intro.toc
doc-src/Logics/CTT-eg.txt
doc-src/Logics/logics.bbl
doc-src/Logics/logics.toc
doc-src/Ref/ref.bbl
doc-src/Ref/ref.toc
doc-src/Ref/simplifier-eg.txt
     1.1 --- a/doc-src/Intro/intro.bbl	Tue May 03 18:36:18 1994 +0200
     1.2 +++ b/doc-src/Intro/intro.bbl	Tue May 03 18:38:28 1994 +0200
     1.3 @@ -5,28 +5,28 @@
     1.4  \newblock {\em Logic for Information Technology}.
     1.5  \newblock Wiley, 1990.
     1.6  
     1.7 -\bibitem{gordon88a}
     1.8 -Michael J.~C. Gordon.
     1.9 -\newblock {HOL}: A proof generating system for higher-order logic.
    1.10 -\newblock In Graham Birtwistle and P.~A. Subrahmanyam, editors, {\em {VLSI}
    1.11 -  Specification, Verification and Synthesis}, pages 73--128. Kluwer Academic
    1.12 -  Publishers, 1988.
    1.13 +\bibitem{mgordon-hol}
    1.14 +M.~J.~C. Gordon and T.~F. Melham.
    1.15 +\newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher
    1.16 +  Order Logic}.
    1.17 +\newblock Cambridge University Press, 1993.
    1.18  
    1.19 -\bibitem{gordon79}
    1.20 +\bibitem{mgordon79}
    1.21  Michael J.~C. Gordon, Robin Milner, and Christopher~P. Wadsworth.
    1.22  \newblock {\em Edinburgh {LCF}: A Mechanised Logic of Computation}.
    1.23 -\newblock Springer LNCS 78, 1979.
    1.24 +\newblock Springer, 1979.
    1.25 +\newblock LNCS 78.
    1.26  
    1.27  \bibitem{haskell-tutorial}
    1.28  Paul Hudak and Joseph~H. Fasel.
    1.29  \newblock A gentle introduction to {Haskell}.
    1.30 -\newblock {\em {ACM} {SIGPLAN} Notices}, 27(5), May 1992.
    1.31 +\newblock {\em {SIGPLAN} Notices}, 27(5), May 1992.
    1.32  
    1.33  \bibitem{haskell-report}
    1.34  Paul Hudak, Simon~Peyton Jones, and Philip Wadler.
    1.35  \newblock Report on the programming language {Haskell}: A non-strict, purely
    1.36    functional language.
    1.37 -\newblock {\em {ACM} {SIGPLAN} Notices}, 27(5), May 1992.
    1.38 +\newblock {\em {SIGPLAN} Notices}, 27(5), May 1992.
    1.39  \newblock Version 1.2.
    1.40  
    1.41  \bibitem{huet75}
    1.42 @@ -34,7 +34,7 @@
    1.43  \newblock A unification algorithm for typed $\lambda$-calculus.
    1.44  \newblock {\em Theoretical Computer Science}, 1:27--57, 1975.
    1.45  
    1.46 -\bibitem{miller-jsc}
    1.47 +\bibitem{miller-mixed}
    1.48  Dale Miller.
    1.49  \newblock Unification under a mixed prefix.
    1.50  \newblock {\em Journal of Symbolic Computation}, 14(4):321--358, 1992.
    1.51 @@ -42,13 +42,15 @@
    1.52  \bibitem{nipkow-prehofer}
    1.53  Tobias Nipkow and Christian Prehofer.
    1.54  \newblock Type checking type classes.
    1.55 -\newblock In {\em 20th ACM Symp.\ Principles of Programming Languages}, 1993.
    1.56 -\newblock To appear.
    1.57 +\newblock In {\em 20th Principles of Programming Languages}, pages 409--418.
    1.58 +  ACM Press, 1993.
    1.59 +\newblock Revised version to appear in \bgroup\em Journal of Functional
    1.60 +  Programming\egroup.
    1.61  
    1.62  \bibitem{nordstrom90}
    1.63  Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith.
    1.64  \newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}.
    1.65 -\newblock Oxford, 1990.
    1.66 +\newblock Oxford University Press, 1990.
    1.67  
    1.68  \bibitem{paulson86}
    1.69  Lawrence~C. Paulson.
    1.70 @@ -63,7 +65,7 @@
    1.71  \bibitem{paulson89}
    1.72  Lawrence~C. Paulson.
    1.73  \newblock The foundation of a generic theorem prover.
    1.74 -\newblock {\em Journal of Automated Reasoning}, 5:363--397, 1989.
    1.75 +\newblock {\em Journal of Automated Reasoning}, 5(3):363--397, 1989.
    1.76  
    1.77  \bibitem{paulson700}
    1.78  Lawrence~C. Paulson.
     2.1 --- a/doc-src/Intro/intro.ind	Tue May 03 18:36:18 1994 +0200
     2.2 +++ b/doc-src/Intro/intro.ind	Tue May 03 18:38:28 1994 +0200
     2.3 @@ -1,251 +1,265 @@
     2.4  \begin{theindex}
     2.5  
     2.6 -  \item $\Forall$, \bold{5}, 7
     2.7 -  \item $\Imp$, \bold{5}
     2.8 -  \item $\To$, \bold{1}, \bold{3}
     2.9 -  \item $\equiv$, \bold{5}
    2.10 -
    2.11 -  \indexspace
    2.12 -
    2.13 -  \item {\tt allI}, 35
    2.14 -  \item arities
    2.15 -    \subitem declaring, 3, \bold{46}
    2.16 -  \item {\tt asm_simp_tac}, 55
    2.17 -  \item associativity of addition, 54
    2.18 -  \item {\tt assume_tac}, \bold{27}, 29, 30, 35, 43, 44
    2.19 -  \item assumptions, 6
    2.20 +  \item {\ptt !!} symbol, 24
    2.21 +    \subitem in main goal, 44
    2.22 +  \item {\tt\%} symbol, 24
    2.23 +  \item {\ptt ::} symbol, 24
    2.24 +  \item {\ptt ==} symbol, 24
    2.25 +  \item {\ptt ==>} symbol, 24
    2.26 +  \item {\ptt =>} symbol, 24
    2.27 +  \item {\ptt =?=} symbol, 24
    2.28 +  \item {\ptt [} symbol, 24
    2.29 +  \item {\ptt [|} symbol, 24
    2.30 +  \item {\ptt ]} symbol, 24
    2.31 +  \item {\tt\ttlbrace} symbol, 24
    2.32 +  \item {\tt\ttrbrace} symbol, 24
    2.33 +  \item {\ptt |]} symbol, 24
    2.34  
    2.35    \indexspace
    2.36  
    2.37 -  \item {\tt ba}, \bold{28}
    2.38 -  \item {\tt back}, 54, 57
    2.39 -  \item backtracking, 57
    2.40 -  \item {\tt bd}, \bold{28}
    2.41 -  \item {\tt be}, \bold{28}
    2.42 -  \item {\tt br}, \bold{28}
    2.43 -  \item {\tt by}, \bold{28}
    2.44 +  \item {\ptt allI} theorem, 35
    2.45 +  \item arities
    2.46 +    \subitem declaring, 4, \bold{46}
    2.47 +  \item {\ptt asm_simp_tac}, 56
    2.48 +  \item {\ptt assume_tac}, 28, 30, 35, 44
    2.49 +  \item assumptions
    2.50 +    \subitem deleting, 19
    2.51 +    \subitem discharge of, 7
    2.52 +    \subitem lifting over, 13
    2.53 +    \subitem of main goal, 39
    2.54 +    \subitem use of, 16, 27
    2.55 +  \item axioms
    2.56 +    \subitem Peano, 51
    2.57  
    2.58    \indexspace
    2.59  
    2.60 -  \item {\tt choplev}, 34, 35, 59
    2.61 -  \item classes, \bold{3}
    2.62 -    \subitem built-in, \bold{23}
    2.63 -  \item classical reasoning package, 36
    2.64 -  \item classical sets, \bold{36}
    2.65 -  \item {\tt conjunct1}, 25
    2.66 -  \item constants
    2.67 -    \subitem declaring, \bold{45}
    2.68 +  \item {\ptt ba}, 29
    2.69 +  \item {\ptt back}, 54, 55, 58
    2.70 +  \item backtracking
    2.71 +    \subitem Prolog style, 58
    2.72 +  \item {\ptt bd}, 29
    2.73 +  \item {\ptt be}, 29
    2.74 +  \item {\ptt br}, 29
    2.75 +  \item {\ptt by}, 29
    2.76  
    2.77    \indexspace
    2.78  
    2.79 -  \item definitions, \bold{5}
    2.80 -    \subitem reasoning about, \bold{40}
    2.81 -  \item {\tt DEPTH_FIRST}, 59
    2.82 -  \item destruct-resolution, \bold{20}
    2.83 -  \item destruction rules, \bold{20}
    2.84 -  \item {\tt disjE}, 29
    2.85 -  \item {\tt dres_inst_tac}, \bold{52}
    2.86 -  \item {\tt dresolve_tac}, \bold{28}, 30, 33, 36
    2.87 +  \item {\ptt choplev}, 34, 35, 60
    2.88 +  \item classes, 3
    2.89 +    \subitem built-in, \bold{24}
    2.90 +  \item classical reasoner, 37
    2.91 +  \item {\ptt conjunct1} theorem, 26
    2.92 +  \item constants, 1
    2.93 +    \subitem clashes with variables, 9
    2.94 +    \subitem declaring, \bold{46}
    2.95 +    \subitem overloaded, 50
    2.96 +    \subitem polymorphic, 3
    2.97 +
    2.98 +  \indexspace
    2.99 +
   2.100 +  \item definitions, 5, \bold{46}
   2.101 +    \subitem and derived rules, 41--44
   2.102 +  \item {\ptt DEPTH_FIRST}, 59
   2.103 +  \item destruct-resolution, 21, 29
   2.104 +  \item {\ptt disjE} theorem, 30
   2.105 +  \item {\ptt dres_inst_tac}, 53
   2.106 +  \item {\ptt dresolve_tac}, 29, 31, 36
   2.107  
   2.108    \indexspace
   2.109  
   2.110    \item eigenvariables, \see{parameters}{7}
   2.111 -  \item elim-resolution, \bold{18}
   2.112 +  \item elim-resolution, \bold{19}, 28
   2.113    \item equality
   2.114 -    \subitem meta-level, \bold{5}
   2.115 -  \item {\tt eres_inst_tac}, \bold{52}
   2.116 -  \item {\tt eresolve_tac}, \bold{27}, 30, 36, 43, 44
   2.117 +    \subitem polymorphic, 3
   2.118 +  \item {\ptt eres_inst_tac}, 53
   2.119 +  \item {\ptt eresolve_tac}, 28, 31, 36, 44
   2.120    \item examples
   2.121 -    \subitem of deriving rules, 38
   2.122 -    \subitem of induction, 52, 53
   2.123 -    \subitem of rewriting, 54
   2.124 +    \subitem of deriving rules, 39
   2.125 +    \subitem of induction, 53, 54
   2.126 +    \subitem of simplification, 55
   2.127      \subitem of tacticals, 35
   2.128 -    \subitem of theories, 45--51, 56
   2.129 -    \subitem propositional, 16, 28, 30
   2.130 -    \subitem with quantifiers, 17, 31, 33, 35
   2.131 -  \item {\tt exE}, 35
   2.132 +    \subitem of theories, 46--52, 57
   2.133 +    \subitem propositional, 16, 29, 31
   2.134 +    \subitem with quantifiers, 17, 32, 33, 36
   2.135 +  \item {\ptt exE} theorem, 36
   2.136  
   2.137    \indexspace
   2.138  
   2.139 -  \item {\tt FalseE}, 42
   2.140 -  \item {\tt fast_tac}, 36, 37
   2.141 -  \item flex-flex equations, \bold{5}, 23, \bold{26}
   2.142 -  \item {\tt flexflex_rule}, 26
   2.143 -  \item {\tt FOL}, 56
   2.144 -  \item {\tt FOL.thy}, 28
   2.145 -  \item folding, \bold{40}
   2.146 -
   2.147 -  \indexspace
   2.148 -
   2.149 -  \item {\tt goal}, \bold{28}, 38, 39, 41--43
   2.150 -  \item {\tt goalw}, 42, 43
   2.151 +  \item {\ptt FalseE} theorem, 43
   2.152 +  \item {\ptt fast_tac}, 37
   2.153 +  \item first-order logic, 1
   2.154 +  \item flex-flex constraints, 5, 24, \bold{27}
   2.155 +  \item {\ptt flexflex_rule}, 27
   2.156 +  \item forward proof, 20, 23--29
   2.157 +  \item {\ptt fun} type, 1, 4
   2.158 +  \item function applications, 1, 7
   2.159  
   2.160    \indexspace
   2.161  
   2.162 -  \item {\tt has_fewer_prems}, 59
   2.163 +  \item {\ptt goal}, 29, 39, 44
   2.164 +  \item {\ptt goalw}, 42--44
   2.165 +
   2.166 +  \indexspace
   2.167 +
   2.168 +  \item {\ptt has_fewer_prems}, 60
   2.169 +  \item higher-order logic, 4
   2.170  
   2.171    \indexspace
   2.172  
   2.173 -  \item identifiers, \bold{22}
   2.174 -  \item imitation, \bold{10}
   2.175 -  \item {\tt impI}, 29, 41
   2.176 -  \item implication
   2.177 -    \subitem meta-level, \bold{5}
   2.178 -  \item infix operators, \bold{47}
   2.179 -  \item instantiation
   2.180 -    \subitem explicit, \bold{52}
   2.181 +  \item identifiers, 23
   2.182 +  \item {\ptt impI} theorem, 30, 42
   2.183 +  \item infixes, 48
   2.184 +  \item instantiation, 53--56
   2.185    \item Isabelle
   2.186 -    \subitem definitions in, 40
   2.187 -    \subitem formalizing rules, \bold{5}
   2.188 -    \subitem formalizing syntax, \bold{1}
   2.189 -    \subitem getting started, 22
   2.190      \subitem object-logics supported, i
   2.191      \subitem overview, i
   2.192 -    \subitem proof construction in, \bold{9}
   2.193      \subitem release history, i
   2.194 -    \subitem syntax of, 23
   2.195  
   2.196    \indexspace
   2.197  
   2.198 -  \item LCF, i, 14, 24
   2.199 -  \item level, \bold{29}
   2.200 +  \item $\lambda$-abstractions, 1, 7, 24
   2.201 +  \item $\lambda$-calculus, 1
   2.202 +  \item LCF, i
   2.203 +  \item LCF system, 15, 25
   2.204 +  \item level of a proof, 29
   2.205    \item lifting, \bold{13}
   2.206 -    \subitem over assumptions, \bold{13}
   2.207 -    \subitem over parameters, \bold{13}
   2.208 -  \item {\tt logic}, 23
   2.209 +  \item {\ptt logic} class, 3, 6, 24
   2.210  
   2.211    \indexspace
   2.212  
   2.213 -  \item main goal, \bold{14}
   2.214 -  \item major premise, \bold{19}
   2.215 -  \item {\tt Match}, 39
   2.216 -  \item meta-formulae
   2.217 -    \subitem syntax, \bold{23}
   2.218 -  \item meta-logic, \bold{5}
   2.219 -  \item mixfix operators, \bold{47}
   2.220 -  \item ML, i, 22, 25
   2.221 -  \item {\tt mp}, 25
   2.222 +  \item major premise, \bold{20}
   2.223 +  \item {\ptt Match} exception, 40
   2.224 +  \item meta-assumptions
   2.225 +    \subitem syntax of, 21
   2.226 +  \item meta-equality, \bold{5}, 24
   2.227 +  \item meta-implication, \bold{5}, 6, 24
   2.228 +  \item meta-quantifiers, \bold{5}, 7, 24
   2.229 +  \item meta-rewriting, 41
   2.230 +  \item mixfix declarations, 49, 52
   2.231 +  \item ML, i
   2.232 +  \item {\ptt ML} section, 45
   2.233 +  \item {\ptt mp} theorem, 26
   2.234  
   2.235    \indexspace
   2.236  
   2.237 -  \item {\tt Nat}, \bold{51}
   2.238 -  \item {\tt Nat.thy}, 53
   2.239 -  \item {\tt not_def}, 41
   2.240 -  \item {\tt notE}, \bold{43}, 53
   2.241 -  \item {\tt notI}, \bold{41}, 53
   2.242 +  \item {\ptt Nat} theory, 52
   2.243 +  \item {\ptt nat} type, 1, 3
   2.244 +  \item {\ptt not_def} theorem, 42
   2.245 +  \item {\ptt notE} theorem, \bold{43}, 54
   2.246 +  \item {\ptt notI} theorem, \bold{42}, 54
   2.247  
   2.248    \indexspace
   2.249  
   2.250 -  \item {\tt ORELSE}, 35
   2.251 -  \item overloading, \bold{4}, 48
   2.252 +  \item {\ptt o} type, 1, 4
   2.253 +  \item {\ptt ORELSE}, 35
   2.254 +  \item overloading, \bold{4}, 50
   2.255  
   2.256    \indexspace
   2.257  
   2.258 -  \item parameters, \bold{7}, 31
   2.259 -  \item printing commands, \bold{25}
   2.260 -  \item projection, \bold{10}
   2.261 -  \item {\tt Prolog}, 56
   2.262 -  \item Prolog interpreter, \bold{55}
   2.263 -  \item proof
   2.264 -    \subitem backward, \bold{14}
   2.265 -    \subitem by assumption, \bold{15}
   2.266 -    \subitem by induction, 52
   2.267 -    \subitem commands for, \bold{28}
   2.268 -    \subitem forward, 20
   2.269 -  \item proof state, \bold{14}
   2.270 -  \item {\tt PROP}, 24
   2.271 -  \item {\tt prop}, 23, 24
   2.272 -  \item {\tt prth}, \bold{25}
   2.273 -  \item {\tt prthq}, \bold{25}, 26
   2.274 -  \item {\tt prths}, \bold{25}
   2.275 -  \item {\tt Pure}, \bold{44}
   2.276 +  \item parameters, \bold{7}, 32
   2.277 +    \subitem lifting over, 14
   2.278 +  \item {\ptt Prolog} theory, 57
   2.279 +  \item Prolog interpreter, \bold{56}
   2.280 +  \item proof state, 15
   2.281 +  \item proofs
   2.282 +    \subitem commands for, 29
   2.283 +  \item {\ptt PROP} symbol, 25
   2.284 +  \item {\ptt prop} type, 6, 24
   2.285 +  \item {\ptt prth}, 26
   2.286 +  \item {\ptt prthq}, 26, 27
   2.287 +  \item {\ptt prths}, 26
   2.288 +  \item {\ptt Pure} theory, 45
   2.289 +
   2.290 +  \indexspace
   2.291 +
   2.292 +  \item quantifiers, 5, 7, 32
   2.293  
   2.294    \indexspace
   2.295  
   2.296 -  \item quantifiers
   2.297 -    \subitem meta-level, \bold{5}
   2.298 -    \subitem reasoning about, 31
   2.299 -
   2.300 -  \indexspace
   2.301 -
   2.302 -  \item {\tt read_instantiate}, 27
   2.303 -  \item refinement, \bold{15}
   2.304 -    \subitem with instantiation, \bold{52}
   2.305 -  \item {\tt refl}, 27
   2.306 -  \item {\tt REPEAT}, 30, 35, 57, 59
   2.307 -  \item {\tt res_inst_tac}, \bold{52}, 54, 55
   2.308 -  \item reserved words, \bold{22}
   2.309 -  \item resolution, \bold{11}
   2.310 -    \subitem in backward proof, 14
   2.311 -  \item {\tt resolve_tac}, \bold{27}, 29, 43, 53
   2.312 -  \item {\tt result}, \bold{28}, 29, 38, 39, 44
   2.313 -  \item {\tt rewrite_goals_tac}, 41, 42
   2.314 -  \item {\tt rewrite_rule}, 42, 43
   2.315 -  \item rewriting
   2.316 -    \subitem meta-level, 40, \bold{40}
   2.317 -    \subitem object-level, 54
   2.318 -  \item {\tt RL}, 27
   2.319 -  \item {\tt RLN}, 27
   2.320 -  \item {\tt RS}, \bold{25}, 27, 43
   2.321 -  \item {\tt RSN}, \bold{25}, 27
   2.322 +  \item {\ptt read_instantiate}, 28
   2.323 +  \item {\ptt refl} theorem, 28
   2.324 +  \item {\ptt REPEAT}, 31, 36, 58, 59
   2.325 +  \item {\ptt res_inst_tac}, 53, 55
   2.326 +  \item reserved words, 23
   2.327 +  \item resolution, 10, \bold{11}
   2.328 +    \subitem in backward proof, 15
   2.329 +    \subitem with instantiation, 53
   2.330 +  \item {\ptt resolve_tac}, 28, 30, 43, 54
   2.331 +  \item {\ptt result}, 29, 40, 44
   2.332 +  \item {\ptt rewrite_goals_tac}, 42
   2.333 +  \item {\ptt rewrite_rule}, 43
   2.334 +  \item {\ptt RL}, 27, 28
   2.335 +  \item {\ptt RLN}, 27
   2.336 +  \item {\ptt RS}, 26, 27, 44
   2.337 +  \item {\ptt RSN}, 26, 27
   2.338    \item rules
   2.339 -    \subitem declaring, \bold{45}
   2.340 -    \subitem derived, 12, \bold{20}, 38, 40
   2.341 -    \subitem propositional, \bold{6}
   2.342 -    \subitem quantifier, \bold{7}
   2.343 +    \subitem declaring, 46
   2.344 +    \subitem derived, 12, \bold{21}, 39, 41
   2.345 +    \subitem destruction, 20
   2.346 +    \subitem elimination, 20
   2.347 +    \subitem propositional, 6
   2.348 +    \subitem quantifier, 7
   2.349  
   2.350    \indexspace
   2.351  
   2.352    \item search
   2.353 -    \subitem depth-first, 58
   2.354 +    \subitem depth-first, 59
   2.355    \item signatures, \bold{8}
   2.356 -  \item {\tt simp_tac}, 55
   2.357 -  \item simplification set, \bold{54}
   2.358 +  \item {\ptt simp_tac}, 56
   2.359 +  \item simplification, 55
   2.360 +  \item simplification sets, 55
   2.361 +  \item sort constraints, 24
   2.362    \item sorts, \bold{4}
   2.363 -  \item {\tt spec}, 26, 33, 35
   2.364 -  \item {\tt standard}, \bold{25}
   2.365 -  \item subgoals, \bold{14}
   2.366 +  \item {\ptt spec} theorem, 26, 34, 35
   2.367 +  \item {\ptt standard}, 26
   2.368    \item substitution, \bold{7}
   2.369 -  \item {\tt Suc_inject}, 53
   2.370 -  \item {\tt Suc_neq_0}, 53
   2.371 +  \item {\ptt Suc_inject}, 54
   2.372 +  \item {\ptt Suc_neq_0}, 54
   2.373 +  \item syntax
   2.374 +    \subitem of types and terms, 24
   2.375  
   2.376    \indexspace
   2.377  
   2.378 -  \item tacticals, \bold{14}, \bold{17}, 35
   2.379 -  \item Tactics, \bold{14}
   2.380 -  \item tactics, \bold{17}
   2.381 -    \subitem basic, \bold{27}
   2.382 +  \item tacticals, \bold{18}, 35
   2.383 +  \item tactics, \bold{18}
   2.384 +    \subitem assumption, 28
   2.385 +    \subitem resolution, 28
   2.386 +  \item {\ptt term} class, 3
   2.387    \item terms
   2.388 -    \subitem syntax, \bold{23}
   2.389 +    \subitem syntax of, 1, \bold{24}
   2.390    \item theorems
   2.391 -    \subitem basic operations on, \bold{24}
   2.392 +    \subitem basic operations on, \bold{25}
   2.393 +    \subitem printing of, 25
   2.394    \item theories, \bold{8}
   2.395 -    \subitem defining, 44--52
   2.396 -  \item {\tt thm}, 24
   2.397 -  \item {\tt topthm}, 39
   2.398 -  \item {$Trueprop$}, 6, 7, 9, 23
   2.399 -  \item type constructors
   2.400 +    \subitem defining, 44--53
   2.401 +  \item {\ptt thm} ML type, 25
   2.402 +  \item {\ptt topthm}, 40
   2.403 +  \item {\ptt Trueprop} constant, 6, 24
   2.404 +  \item type constraints, 24
   2.405 +  \item type constructors, 1
   2.406 +  \item type identifiers, 23
   2.407 +  \item type synonyms, \bold{48}
   2.408 +  \item types
   2.409      \subitem declaring, \bold{46}
   2.410 -  \item types, 1
   2.411 -    \subitem higher, \bold{4}
   2.412 +    \subitem function, 1
   2.413 +    \subitem higher, \bold{5}
   2.414      \subitem polymorphic, \bold{3}
   2.415      \subitem simple, \bold{1}
   2.416 -    \subitem syntax, \bold{23}
   2.417 +    \subitem syntax of, 1, \bold{24}
   2.418  
   2.419    \indexspace
   2.420  
   2.421 -  \item {\tt undo}, \bold{28}
   2.422 -  \item unfolding, \bold{40}
   2.423 +  \item {\ptt undo}, 29
   2.424    \item unification
   2.425 -    \subitem higher-order, \bold{10}, 53
   2.426 -  \item unknowns, \bold{9}, 31
   2.427 -    \subitem of function type, \bold{11}, 26
   2.428 -  \item {\tt use_thy}, \bold{44, 45}
   2.429 +    \subitem higher-order, \bold{10}, 54
   2.430 +    \subitem incompleteness of, 11
   2.431 +  \item unknowns, 9, 23, 32
   2.432 +    \subitem function, \bold{11}, 27, 32
   2.433 +  \item {\ptt use_thy}, \bold{45}
   2.434  
   2.435    \indexspace
   2.436  
   2.437    \item variables
   2.438      \subitem bound, 7
   2.439 -    \subitem schematic, \see{unknowns}{9}
   2.440  
   2.441  \end{theindex}
     3.1 --- a/doc-src/Intro/intro.toc	Tue May 03 18:36:18 1994 +0200
     3.2 +++ b/doc-src/Intro/intro.toc	Tue May 03 18:38:28 1994 +0200
     3.3 @@ -2,7 +2,7 @@
     3.4  \contentsline {section}{\numberline {1}Formalizing logical syntax in Isabelle}{1}
     3.5  \contentsline {subsection}{\numberline {1.1}Simple types and constants}{1}
     3.6  \contentsline {subsection}{\numberline {1.2}Polymorphic types and constants}{3}
     3.7 -\contentsline {subsection}{\numberline {1.3}Higher types and quantifiers}{4}
     3.8 +\contentsline {subsection}{\numberline {1.3}Higher types and quantifiers}{5}
     3.9  \contentsline {section}{\numberline {2}Formalizing logical rules in Isabelle}{5}
    3.10  \contentsline {subsection}{\numberline {2.1}Expressing propositional rules}{6}
    3.11  \contentsline {subsection}{\numberline {2.2}Quantifier rules and substitution}{7}
    3.12 @@ -10,58 +10,61 @@
    3.13  \contentsline {section}{\numberline {3}Proof construction in Isabelle}{9}
    3.14  \contentsline {subsection}{\numberline {3.1}Higher-order unification}{10}
    3.15  \contentsline {subsection}{\numberline {3.2}Joining rules by resolution}{11}
    3.16 -\contentsline {subsection}{\numberline {3.3}Lifting a rule into a context}{13}
    3.17 -\contentsline {subsubsection}{Lifting over assumptions}{13}
    3.18 -\contentsline {subsubsection}{Lifting over parameters}{13}
    3.19 -\contentsline {section}{\numberline {4}Backward proof by resolution}{14}
    3.20 -\contentsline {subsection}{\numberline {4.1}Refinement by resolution}{15}
    3.21 -\contentsline {subsection}{\numberline {4.2}Proof by assumption}{15}
    3.22 -\contentsline {subsection}{\numberline {4.3}A propositional proof}{16}
    3.23 -\contentsline {subsection}{\numberline {4.4}A quantifier proof}{17}
    3.24 -\contentsline {subsection}{\numberline {4.5}Tactics and tacticals}{17}
    3.25 -\contentsline {section}{\numberline {5}Variations on resolution}{18}
    3.26 -\contentsline {subsection}{\numberline {5.1}Elim-resolution}{18}
    3.27 -\contentsline {subsection}{\numberline {5.2}Destruction rules}{20}
    3.28 -\contentsline {subsection}{\numberline {5.3}Deriving rules by resolution}{20}
    3.29 -\contentsline {part}{\uppercase {ii}\phspace {1em}Getting started with Isabelle}{22}
    3.30 -\contentsline {section}{\numberline {6}Forward proof}{22}
    3.31 -\contentsline {subsection}{\numberline {6.1}Lexical matters}{22}
    3.32 -\contentsline {subsection}{\numberline {6.2}Syntax of types and terms}{23}
    3.33 -\contentsline {subsection}{\numberline {6.3}Basic operations on theorems}{24}
    3.34 -\contentsline {subsection}{\numberline {6.4}Flex-flex equations}{26}
    3.35 -\contentsline {section}{\numberline {7}Backward proof}{27}
    3.36 -\contentsline {subsection}{\numberline {7.1}The basic tactics}{27}
    3.37 -\contentsline {subsection}{\numberline {7.2}Commands for backward proof}{28}
    3.38 -\contentsline {subsection}{\numberline {7.3}A trivial example in propositional logic}{28}
    3.39 -\contentsline {subsection}{\numberline {7.4}Proving a distributive law}{30}
    3.40 -\contentsline {section}{\numberline {8}Quantifier reasoning}{31}
    3.41 -\contentsline {subsection}{\numberline {8.1}Two quantifier proofs, successful and not}{31}
    3.42 -\contentsline {subsubsection}{The successful proof}{31}
    3.43 -\contentsline {subsubsection}{The unsuccessful proof}{32}
    3.44 -\contentsline {subsection}{\numberline {8.2}Nested quantifiers}{33}
    3.45 -\contentsline {subsubsection}{The wrong approach}{33}
    3.46 -\contentsline {subsubsection}{The right approach}{34}
    3.47 -\contentsline {subsubsection}{A one-step proof using tacticals}{35}
    3.48 -\contentsline {subsection}{\numberline {8.3}A realistic quantifier proof}{35}
    3.49 -\contentsline {subsection}{\numberline {8.4}The classical reasoning package}{36}
    3.50 -\contentsline {part}{\uppercase {iii}\phspace {1em}Advanced methods}{38}
    3.51 -\contentsline {section}{\numberline {9}Deriving rules in Isabelle}{38}
    3.52 -\contentsline {subsection}{\numberline {9.1}Deriving a rule using tactics}{38}
    3.53 -\contentsline {subsection}{\numberline {9.2}Definitions and derived rules}{40}
    3.54 -\contentsline {subsubsection}{Deriving the introduction rule}{41}
    3.55 -\contentsline {subsubsection}{Deriving the elimination rule}{42}
    3.56 -\contentsline {section}{\numberline {10}Defining theories}{44}
    3.57 -\contentsline {subsection}{\numberline {10.1}Declaring constants and rules}{45}
    3.58 -\contentsline {subsection}{\numberline {10.2}Declaring type constructors}{46}
    3.59 -\contentsline {subsection}{\numberline {10.3}Infixes and Mixfixes}{47}
    3.60 -\contentsline {subsection}{\numberline {10.4}Overloading}{48}
    3.61 -\contentsline {subsection}{\numberline {10.5}Extending first-order logic with the natural numbers}{50}
    3.62 -\contentsline {subsection}{\numberline {10.6}Declaring the theory to Isabelle}{51}
    3.63 -\contentsline {section}{\numberline {11}Refinement with explicit instantiation}{52}
    3.64 -\contentsline {subsection}{\numberline {11.1}A simple proof by induction}{52}
    3.65 -\contentsline {subsection}{\numberline {11.2}An example of ambiguity in {\ptt resolve_tac}}{53}
    3.66 -\contentsline {subsection}{\numberline {11.3}Proving that addition is associative}{54}
    3.67 -\contentsline {section}{\numberline {12}A {\psc Prolog} interpreter}{55}
    3.68 -\contentsline {subsection}{\numberline {12.1}Simple executions}{56}
    3.69 -\contentsline {subsection}{\numberline {12.2}Backtracking}{57}
    3.70 -\contentsline {subsection}{\numberline {12.3}Depth-first search}{58}
    3.71 +\contentsline {section}{\numberline {4}Lifting a rule into a context}{13}
    3.72 +\contentsline {subsection}{\numberline {4.1}Lifting over assumptions}{13}
    3.73 +\contentsline {subsection}{\numberline {4.2}Lifting over parameters}{14}
    3.74 +\contentsline {section}{\numberline {5}Backward proof by resolution}{15}
    3.75 +\contentsline {subsection}{\numberline {5.1}Refinement by resolution}{15}
    3.76 +\contentsline {subsection}{\numberline {5.2}Proof by assumption}{16}
    3.77 +\contentsline {subsection}{\numberline {5.3}A propositional proof}{16}
    3.78 +\contentsline {subsection}{\numberline {5.4}A quantifier proof}{17}
    3.79 +\contentsline {subsection}{\numberline {5.5}Tactics and tacticals}{18}
    3.80 +\contentsline {section}{\numberline {6}Variations on resolution}{18}
    3.81 +\contentsline {subsection}{\numberline {6.1}Elim-resolution}{19}
    3.82 +\contentsline {subsection}{\numberline {6.2}Destruction rules}{20}
    3.83 +\contentsline {subsection}{\numberline {6.3}Deriving rules by resolution}{21}
    3.84 +\contentsline {part}{\uppercase {ii}\phspace {1em}Getting Started with Isabelle}{23}
    3.85 +\contentsline {section}{\numberline {7}Forward proof}{23}
    3.86 +\contentsline {subsection}{\numberline {7.1}Lexical matters}{23}
    3.87 +\contentsline {subsection}{\numberline {7.2}Syntax of types and terms}{24}
    3.88 +\contentsline {subsection}{\numberline {7.3}Basic operations on theorems}{25}
    3.89 +\contentsline {subsection}{\numberline {7.4}*Flex-flex constraints}{27}
    3.90 +\contentsline {section}{\numberline {8}Backward proof}{28}
    3.91 +\contentsline {subsection}{\numberline {8.1}The basic tactics}{28}
    3.92 +\contentsline {subsection}{\numberline {8.2}Commands for backward proof}{29}
    3.93 +\contentsline {subsection}{\numberline {8.3}A trivial example in propositional logic}{29}
    3.94 +\contentsline {subsection}{\numberline {8.4}Part of a distributive law}{31}
    3.95 +\contentsline {section}{\numberline {9}Quantifier reasoning}{32}
    3.96 +\contentsline {subsection}{\numberline {9.1}Two quantifier proofs: a success and a failure}{32}
    3.97 +\contentsline {paragraph}{The successful proof.}{32}
    3.98 +\contentsline {paragraph}{The unsuccessful proof.}{33}
    3.99 +\contentsline {subsection}{\numberline {9.2}Nested quantifiers}{33}
   3.100 +\contentsline {paragraph}{The wrong approach.}{34}
   3.101 +\contentsline {paragraph}{The right approach.}{34}
   3.102 +\contentsline {paragraph}{A one-step proof using tacticals.}{35}
   3.103 +\contentsline {subsection}{\numberline {9.3}A realistic quantifier proof}{36}
   3.104 +\contentsline {subsection}{\numberline {9.4}The classical reasoner}{37}
   3.105 +\contentsline {part}{\uppercase {iii}\phspace {1em}Advanced Methods}{39}
   3.106 +\contentsline {section}{\numberline {10}Deriving rules in Isabelle}{39}
   3.107 +\contentsline {subsection}{\numberline {10.1}Deriving a rule using tactics and meta-level assumptions}{39}
   3.108 +\contentsline {subsection}{\numberline {10.2}Definitions and derived rules}{41}
   3.109 +\contentsline {subsection}{\numberline {10.3}Deriving the $\neg $ introduction rule}{41}
   3.110 +\contentsline {subsection}{\numberline {10.4}Deriving the $\neg $ elimination rule}{42}
   3.111 +\contentsline {section}{\numberline {11}Defining theories}{44}
   3.112 +\contentsline {subsection}{\numberline {11.1}Declaring constants and rules}{46}
   3.113 +\contentsline {subsection}{\numberline {11.2}Declaring type constructors}{46}
   3.114 +\contentsline {subsection}{\numberline {11.3}Type synonyms}{48}
   3.115 +\contentsline {subsection}{\numberline {11.4}Infix and mixfix operators}{48}
   3.116 +\contentsline {subsection}{\numberline {11.5}Overloading}{50}
   3.117 +\contentsline {section}{\numberline {12}Theory example: the natural numbers}{51}
   3.118 +\contentsline {subsection}{\numberline {12.1}Extending first-order logic with the natural numbers}{51}
   3.119 +\contentsline {subsection}{\numberline {12.2}Declaring the theory to Isabelle}{52}
   3.120 +\contentsline {subsection}{\numberline {12.3}Proving some recursion equations}{52}
   3.121 +\contentsline {section}{\numberline {13}Refinement with explicit instantiation}{53}
   3.122 +\contentsline {subsection}{\numberline {13.1}A simple proof by induction}{53}
   3.123 +\contentsline {subsection}{\numberline {13.2}An example of ambiguity in {\ptt resolve_tac}}{54}
   3.124 +\contentsline {subsection}{\numberline {13.3}Proving that addition is associative}{55}
   3.125 +\contentsline {section}{\numberline {14}A Prolog interpreter}{56}
   3.126 +\contentsline {subsection}{\numberline {14.1}Simple executions}{57}
   3.127 +\contentsline {subsection}{\numberline {14.2}Backtracking}{58}
   3.128 +\contentsline {subsection}{\numberline {14.3}Depth-first search}{59}
     4.1 --- a/doc-src/Logics/CTT-eg.txt	Tue May 03 18:36:18 1994 +0200
     4.2 +++ b/doc-src/Logics/CTT-eg.txt	Tue May 03 18:38:28 1994 +0200
     4.3 @@ -36,10 +36,10 @@
     4.4  (*** Currying, from CTT/ex/elim.ML ***)
     4.5  
     4.6  val prems = goal CTT.thy
     4.7 -    "[| A type; !!x. x:A ==> B(x) type; \
     4.8 -\               !!z. z: (SUM x:A. B(x)) ==> C(z) type |] \
     4.9 -\    ==> ?a : (PROD z : (SUM x:A . B(x)) . C(z)) \
    4.10 -\         --> (PROD x:A . PROD y:B(x) . C(<x,y>))";
    4.11 +    "[| A type; !!x. x:A ==> B(x) type; 			\
    4.12 +\               !!z. z: (SUM x:A. B(x)) ==> C(z) type 		\
    4.13 +\    |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).	\
    4.14 +\                     (PROD x:A . PROD y:B(x) . C(<x,y>))";
    4.15  by (intr_tac prems);
    4.16  by (eresolve_tac [ProdE] 1);
    4.17  by (intr_tac prems);
    4.18 @@ -50,8 +50,8 @@
    4.19  val prems = goal CTT.thy   
    4.20      "[| A type;  !!x. x:A ==> B(x) type;  \
    4.21  \       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type  \
    4.22 -\    |] ==> ?a :    (PROD x:A. SUM y:B(x). C(x,y))    \
    4.23 -\               --> (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
    4.24 +\    |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).    \
    4.25 +\                        (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
    4.26  by (intr_tac prems);
    4.27  by (eresolve_tac [ProdE RS SumE_fst] 1);
    4.28  by (assume_tac 1);
     5.1 --- a/doc-src/Logics/logics.bbl	Tue May 03 18:36:18 1994 +0200
     5.2 +++ b/doc-src/Logics/logics.bbl	Tue May 03 18:38:28 1994 +0200
     5.3 @@ -10,25 +10,46 @@
     5.4  David Basin and Matt Kaufmann.
     5.5  \newblock The {Boyer-Moore} prover and {Nuprl}: An experimental comparison.
     5.6  \newblock In {G\'erard} Huet and Gordon Plotkin, editors, {\em Logical
     5.7 -  Frameworks}, pages 89--119. Cambridge University Press, 1991.
     5.8 +  Frameworks}, pages 89--119. 1991.
     5.9  
    5.10  \bibitem{boyer86}
    5.11  Robert Boyer, Ewing Lusk, William McCune, Ross Overbeek, Mark Stickel, and
    5.12    Lawrence Wos.
    5.13  \newblock Set theory in first-order logic: Clauses for {G\"odel's} axioms.
    5.14 -\newblock {\em Journal of Automated Reasoning}, 2(3):287--327, 1986.
    5.15 +\newblock 2(3):287--327, 1986.
    5.16  
    5.17  \bibitem{camilleri92}
    5.18  J.~Camilleri and T.~F. Melham.
    5.19  \newblock Reasoning with inductively defined relations in the {HOL} theorem
    5.20    prover.
    5.21 -\newblock Technical Report 265, University of Cambridge Computer Laboratory,
    5.22 -  August 1992.
    5.23 +\newblock Technical Report 265, August 1992.
    5.24  
    5.25  \bibitem{church40}
    5.26  Alonzo Church.
    5.27  \newblock A formulation of the simple theory of types.
    5.28 -\newblock {\em Journal of Symbolic Logic}, 5:56--68, 1940.
    5.29 +\newblock 5:56--68, 1940.
    5.30 +
    5.31 +\bibitem{coen92}
    5.32 +Martin~D. Coen.
    5.33 +\newblock {\em Interactive Program Derivation}.
    5.34 +\newblock PhD thesis, University of Cambridge, 1992.
    5.35 +\newblock Computer Laboratory Technical Report 272.
    5.36 +
    5.37 +\bibitem{constable86}
    5.38 +R.~L. {Constable et al.}
    5.39 +\newblock {\em Implementing Mathematics with the Nuprl Proof Development
    5.40 +  System}.
    5.41 +\newblock 1986.
    5.42 +
    5.43 +\bibitem{davey&priestley}
    5.44 +B.~A. Davey and H.~A. Priestley.
    5.45 +\newblock {\em Introduction to Lattices and Order}.
    5.46 +\newblock 1990.
    5.47 +
    5.48 +\bibitem{devlin79}
    5.49 +Keith~J. Devlin.
    5.50 +\newblock {\em Fundamentals of Contemporary Set Theory}.
    5.51 +\newblock Springer, 1979.
    5.52  
    5.53  \bibitem{dummett}
    5.54  Michael Dummett.
    5.55 @@ -38,7 +59,7 @@
    5.56  \bibitem{dyckhoff}
    5.57  Roy Dyckhoff.
    5.58  \newblock Contraction-free sequent calculi for intuitionistic logic.
    5.59 -\newblock {\em Journal of Symbolic Logic}, 57(3):795--807, 1992.
    5.60 +\newblock 57(3):795--807, 1992.
    5.61  
    5.62  \bibitem{felty91a}
    5.63  Amy Felty.
    5.64 @@ -51,14 +72,7 @@
    5.65  \bibitem{frost93}
    5.66  Jacob Frost.
    5.67  \newblock A case study of co-induction in {Isabelle HOL}.
    5.68 -\newblock Technical Report 308, University of Cambridge Computer Laboratory,
    5.69 -  August 1993.
    5.70 -
    5.71 -\bibitem{OBJ}
    5.72 -K.~Futatsugi, J.A. Goguen, Jean-Pierre Jouannaud, and J.~Meseguer.
    5.73 -\newblock Principles of {OBJ2}.
    5.74 -\newblock In {\em Symposium on Principles of Programming Languages}, pages
    5.75 -  52--66, 1985.
    5.76 +\newblock Technical Report 308, August 1993.
    5.77  
    5.78  \bibitem{gallier86}
    5.79  J.~H. Gallier.
    5.80 @@ -66,12 +80,11 @@
    5.81    Proving}.
    5.82  \newblock Harper \& Row, 1986.
    5.83  
    5.84 -\bibitem{mgordon88a}
    5.85 -Michael J.~C. Gordon.
    5.86 -\newblock {HOL}: A proof generating system for higher-order logic.
    5.87 -\newblock In Graham Birtwistle and P.~A. Subrahmanyam, editors, {\em {VLSI}
    5.88 -  Specification, Verification and Synthesis}, pages 73--128. Kluwer Academic
    5.89 -  Publishers, 1988.
    5.90 +\bibitem{mgordon-hol}
    5.91 +M.~J.~C. Gordon and T.~F. Melham.
    5.92 +\newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher
    5.93 +  Order Logic}.
    5.94 +\newblock 1993.
    5.95  
    5.96  \bibitem{halmos60}
    5.97  Paul~R. Halmos.
    5.98 @@ -84,6 +97,13 @@
    5.99    second-order patterns.
   5.100  \newblock {\em Acta Informatica}, 11:31--55, 1978.
   5.101  
   5.102 +\bibitem{alf}
   5.103 +Lena Magnusson and Bengt {Nordstr\"om}.
   5.104 +\newblock The {ALF} proof editor and its proof engine.
   5.105 +\newblock In {\em : International Workshop {TYPES '93}}, pages 213--237.
   5.106 +  Springer, published 1994.
   5.107 +\newblock LNCS 806.
   5.108 +
   5.109  \bibitem{mw81}
   5.110  Zohar Manna and Richard Waldinger.
   5.111  \newblock Deductive synthesis of the unification algorithm.
   5.112 @@ -94,6 +114,13 @@
   5.113  \newblock {\em Intuitionistic type theory}.
   5.114  \newblock Bibliopolis, 1984.
   5.115  
   5.116 +\bibitem{melham89}
   5.117 +Thomas~F. Melham.
   5.118 +\newblock Automating recursive type definitions in higher order logic.
   5.119 +\newblock In Graham Birtwistle and P.~A. Subrahmanyam, editors, {\em Current
   5.120 +  Trends in Hardware Verification and Automated Theorem Proving}, pages
   5.121 +  341--386. Springer, 1989.
   5.122 +
   5.123  \bibitem{milner-coind}
   5.124  Robin Milner and Mads Tofte.
   5.125  \newblock Co-induction in relational semantics.
   5.126 @@ -102,7 +129,7 @@
   5.127  \bibitem{noel}
   5.128  Philippe {No\"el}.
   5.129  \newblock Experimenting with {Isabelle} in {ZF} set theory.
   5.130 -\newblock {\em Journal of Automated Reasoning}, 10(1):15--58, 1993.
   5.131 +\newblock 10(1):15--58, 1993.
   5.132  
   5.133  \bibitem{nordstrom90}
   5.134  Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith.
   5.135 @@ -115,13 +142,6 @@
   5.136  \newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon,
   5.137    December 1992.
   5.138  
   5.139 -\bibitem{paulson-set-I}
   5.140 -Lawrence~C. Paulson.
   5.141 -\newblock Set theory for verification: {I}. {From} foundations to functions.
   5.142 -\newblock {\em Journal of Automated Reasoning}.
   5.143 -\newblock In press; draft available as Report 271, University of Cambridge
   5.144 -  Computer Laboratory.
   5.145 -
   5.146  \bibitem{paulson85}
   5.147  Lawrence~C. Paulson.
   5.148  \newblock Verifying the unification algorithm in {LCF}.
   5.149 @@ -130,7 +150,7 @@
   5.150  \bibitem{paulson87}
   5.151  Lawrence~C. Paulson.
   5.152  \newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}.
   5.153 -\newblock Cambridge University Press, 1987.
   5.154 +\newblock 1987.
   5.155  
   5.156  \bibitem{paulson-COLOG}
   5.157  Lawrence~C. Paulson.
   5.158 @@ -140,44 +160,46 @@
   5.159    of Sciences, Springer.
   5.160  \newblock LNCS 417.
   5.161  
   5.162 -\bibitem{paulson91}
   5.163 -Lawrence~C. Paulson.
   5.164 -\newblock {\em {ML} for the Working Programmer}.
   5.165 -\newblock Cambridge University Press, 1991.
   5.166 -
   5.167  \bibitem{paulson-coind}
   5.168  Lawrence~C. Paulson.
   5.169  \newblock Co-induction and co-recursion in higher-order logic.
   5.170 -\newblock Technical Report 304, University of Cambridge Computer Laboratory,
   5.171 -  July 1993.
   5.172 +\newblock Technical Report 304, July 1993.
   5.173  
   5.174  \bibitem{paulson-fixedpt}
   5.175  Lawrence~C. Paulson.
   5.176 -\newblock A fixedpoint approach to implementing (co-)inductive definitions.
   5.177 -\newblock Technical report, University of Cambridge Computer Laboratory, 1993.
   5.178 -\newblock Draft.
   5.179 +\newblock A fixedpoint approach to implementing (co)inductive definitions.
   5.180 +\newblock Technical Report 320, December 1993.
   5.181 +
   5.182 +\bibitem{paulson-set-I}
   5.183 +Lawrence~C. Paulson.
   5.184 +\newblock Set theory for verification: {I}. {From} foundations to functions.
   5.185 +\newblock 11(3):353--389, 1993.
   5.186  
   5.187  \bibitem{paulson-set-II}
   5.188  Lawrence~C. Paulson.
   5.189  \newblock Set theory for verification: {II}. {Induction} and recursion.
   5.190 -\newblock Technical Report 312, University of Cambridge Computer Laboratory,
   5.191 -  1993.
   5.192 +\newblock Technical Report 312, 1993.
   5.193 +
   5.194 +\bibitem{paulson-final}
   5.195 +Lawrence~C. Paulson.
   5.196 +\newblock A concrete final coalgebra theorem for {ZF} set theory.
   5.197 +\newblock Technical report, 1994.
   5.198  
   5.199  \bibitem{pelletier86}
   5.200  F.~J. Pelletier.
   5.201  \newblock Seventy-five problems for testing automatic theorem provers.
   5.202 -\newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.
   5.203 +\newblock 2:191--216, 1986.
   5.204  \newblock Errata, JAR 4 (1988), 235--236.
   5.205  
   5.206  \bibitem{plaisted90}
   5.207  David~A. Plaisted.
   5.208  \newblock A sequent-style model elimination strategy and a positive refinement.
   5.209 -\newblock {\em Journal of Automated Reasoning}, 6(4):389--402, 1990.
   5.210 +\newblock 6(4):389--402, 1990.
   5.211  
   5.212  \bibitem{quaife92}
   5.213  Art Quaife.
   5.214  \newblock Automated deduction in {von Neumann-Bernays-G\"odel} set theory.
   5.215 -\newblock {\em Journal of Automated Reasoning}, 8(1):91--147, 1992.
   5.216 +\newblock 8(1):91--147, 1992.
   5.217  
   5.218  \bibitem{suppes72}
   5.219  Patrick Suppes.
   5.220 @@ -197,7 +219,7 @@
   5.221  \bibitem{principia}
   5.222  A.~N. Whitehead and B.~Russell.
   5.223  \newblock {\em Principia Mathematica}.
   5.224 -\newblock Cambridge University Press, 1962.
   5.225 +\newblock 1962.
   5.226  \newblock Paperback edition to *56, abridged from the 2nd edition (1927).
   5.227  
   5.228  \end{thebibliography}
     6.1 --- a/doc-src/Logics/logics.toc	Tue May 03 18:36:18 1994 +0200
     6.2 +++ b/doc-src/Logics/logics.toc	Tue May 03 18:38:28 1994 +0200
     6.3 @@ -1,7 +1,7 @@
     6.4 -\contentsline {chapter}{\numberline {1}Introduction}{1}
     6.5 -\contentsline {section}{\numberline {1.1}Syntax definitions}{1}
     6.6 +\contentsline {chapter}{\numberline {1}Basic Concepts}{1}
     6.7 +\contentsline {section}{\numberline {1.1}Syntax definitions}{2}
     6.8  \contentsline {section}{\numberline {1.2}Proof procedures}{3}
     6.9 -\contentsline {chapter}{\numberline {2}First-order logic}{4}
    6.10 +\contentsline {chapter}{\numberline {2}First-Order Logic}{4}
    6.11  \contentsline {section}{\numberline {2.1}Syntax and rules of inference}{4}
    6.12  \contentsline {section}{\numberline {2.2}Generic packages}{8}
    6.13  \contentsline {section}{\numberline {2.3}Intuitionistic proof procedures}{8}
    6.14 @@ -9,92 +9,67 @@
    6.15  \contentsline {section}{\numberline {2.5}An intuitionistic example}{11}
    6.16  \contentsline {section}{\numberline {2.6}An example of intuitionistic negation}{12}
    6.17  \contentsline {section}{\numberline {2.7}A classical example}{14}
    6.18 -\contentsline {section}{\numberline {2.8}Derived rules and the classical tactics}{16}
    6.19 -\contentsline {subsection}{Deriving the introduction rule}{17}
    6.20 +\contentsline {section}{\numberline {2.8}Derived rules and the classical tactics}{15}
    6.21 +\contentsline {subsection}{Deriving the introduction rule}{16}
    6.22  \contentsline {subsection}{Deriving the elimination rule}{17}
    6.23 -\contentsline {subsection}{Using the derived rules}{18}
    6.24 -\contentsline {subsection}{Derived rules versus definitions}{20}
    6.25 -\contentsline {chapter}{\numberline {3}Zermelo-Fraenkel set theory}{23}
    6.26 -\contentsline {section}{\numberline {3.1}Which version of axiomatic set theory?}{23}
    6.27 -\contentsline {section}{\numberline {3.2}The syntax of set theory}{24}
    6.28 -\contentsline {section}{\numberline {3.3}Binding operators}{26}
    6.29 -\contentsline {section}{\numberline {3.4}The Zermelo-Fraenkel axioms}{28}
    6.30 -\contentsline {section}{\numberline {3.5}From basic lemmas to function spaces}{33}
    6.31 -\contentsline {subsection}{Fundamental lemmas}{34}
    6.32 -\contentsline {subsection}{Unordered pairs and finite sets}{34}
    6.33 -\contentsline {subsection}{Subset and lattice properties}{37}
    6.34 -\contentsline {subsection}{Ordered pairs}{37}
    6.35 -\contentsline {subsection}{Relations}{37}
    6.36 -\contentsline {subsection}{Functions}{38}
    6.37 -\contentsline {section}{\numberline {3.6}Further developments}{41}
    6.38 -\contentsline {section}{\numberline {3.7}Simplification rules}{49}
    6.39 -\contentsline {section}{\numberline {3.8}The examples directory}{49}
    6.40 -\contentsline {section}{\numberline {3.9}A proof about powersets}{52}
    6.41 -\contentsline {section}{\numberline {3.10}Monotonicity of the union operator}{54}
    6.42 -\contentsline {section}{\numberline {3.11}Low-level reasoning about functions}{55}
    6.43 -\contentsline {chapter}{\numberline {4}Higher-order logic}{58}
    6.44 -\contentsline {section}{\numberline {4.1}Syntax}{58}
    6.45 -\contentsline {subsection}{Types}{58}
    6.46 -\contentsline {subsection}{Binders}{61}
    6.47 -\contentsline {section}{\numberline {4.2}Rules of inference}{61}
    6.48 -\contentsline {section}{\numberline {4.3}Generic packages}{65}
    6.49 -\contentsline {section}{\numberline {4.4}A formulation of set theory}{66}
    6.50 -\contentsline {subsection}{Syntax of set theory}{66}
    6.51 -\contentsline {subsection}{Axioms and rules of set theory}{72}
    6.52 -\contentsline {subsection}{Derived rules for sets}{72}
    6.53 -\contentsline {section}{\numberline {4.5}Types}{72}
    6.54 -\contentsline {subsection}{Product and sum types}{77}
    6.55 -\contentsline {subsection}{The type of natural numbers, $nat$}{77}
    6.56 -\contentsline {subsection}{The type constructor for lists, $\alpha \pcomma list$}{77}
    6.57 -\contentsline {subsection}{The type constructor for lazy lists, $\alpha \pcomma llist$}{81}
    6.58 -\contentsline {section}{\numberline {4.6}Classical proof procedures}{81}
    6.59 -\contentsline {section}{\numberline {4.7}The examples directories}{81}
    6.60 -\contentsline {section}{\numberline {4.8}Example: deriving the conjunction rules}{82}
    6.61 -\contentsline {subsection}{The introduction rule}{82}
    6.62 -\contentsline {subsection}{The elimination rule}{83}
    6.63 -\contentsline {section}{\numberline {4.9}Example: Cantor's Theorem}{84}
    6.64 -\contentsline {chapter}{\numberline {5}First-order sequent calculus}{87}
    6.65 -\contentsline {section}{\numberline {5.1}Unification for lists}{87}
    6.66 -\contentsline {section}{\numberline {5.2}Syntax and rules of inference}{88}
    6.67 -\contentsline {section}{\numberline {5.3}Tactics for the cut rule}{88}
    6.68 -\contentsline {section}{\numberline {5.4}Tactics for sequents}{93}
    6.69 -\contentsline {section}{\numberline {5.5}Packaging sequent rules}{93}
    6.70 -\contentsline {section}{\numberline {5.6}Proof procedures}{94}
    6.71 -\contentsline {subsection}{Method A}{95}
    6.72 -\contentsline {subsection}{Method B}{95}
    6.73 -\contentsline {section}{\numberline {5.7}A simple example of classical reasoning}{95}
    6.74 -\contentsline {section}{\numberline {5.8}A more complex proof}{97}
    6.75 -\contentsline {chapter}{\numberline {6}Constructive Type Theory}{99}
    6.76 -\contentsline {section}{\numberline {6.1}Syntax}{100}
    6.77 -\contentsline {section}{\numberline {6.2}Rules of inference}{100}
    6.78 -\contentsline {section}{\numberline {6.3}Rule lists}{105}
    6.79 -\contentsline {section}{\numberline {6.4}Tactics for subgoal reordering}{108}
    6.80 -\contentsline {section}{\numberline {6.5}Rewriting tactics}{109}
    6.81 -\contentsline {section}{\numberline {6.6}Tactics for logical reasoning}{109}
    6.82 -\contentsline {section}{\numberline {6.7}A theory of arithmetic}{110}
    6.83 -\contentsline {section}{\numberline {6.8}The examples directory}{110}
    6.84 -\contentsline {section}{\numberline {6.9}Example: type inference}{112}
    6.85 -\contentsline {section}{\numberline {6.10}An example of logical reasoning}{113}
    6.86 -\contentsline {section}{\numberline {6.11}Example: deriving a currying functional}{116}
    6.87 -\contentsline {section}{\numberline {6.12}Example: proving the Axiom of Choice}{117}
    6.88 -\contentsline {chapter}{\numberline {7}Defining Logics}{121}
    6.89 -\contentsline {section}{\numberline {7.1}Precedence grammars}{121}
    6.90 -\contentsline {section}{\numberline {7.2}Basic syntax}{122}
    6.91 -\contentsline {subsection}{Logical types and default syntax}{123}
    6.92 -\contentsline {subsection}{Lexical matters *}{124}
    6.93 -\contentsline {subsection}{Inspecting syntax *}{124}
    6.94 -\contentsline {section}{\numberline {7.3}Abstract syntax trees}{126}
    6.95 -\contentsline {subsection}{Parse trees to asts}{128}
    6.96 -\contentsline {subsection}{Asts to terms *}{129}
    6.97 -\contentsline {subsection}{Printing of terms *}{129}
    6.98 -\contentsline {section}{\numberline {7.4}Mixfix declarations}{130}
    6.99 -\contentsline {subsection}{Infixes}{133}
   6.100 -\contentsline {subsection}{Binders}{133}
   6.101 -\contentsline {section}{\numberline {7.5}Syntactic translations (macros)}{134}
   6.102 -\contentsline {subsection}{Specifying macros}{135}
   6.103 -\contentsline {subsection}{Applying rules}{136}
   6.104 -\contentsline {subsection}{Rewriting strategy}{138}
   6.105 -\contentsline {subsection}{More examples}{138}
   6.106 -\contentsline {section}{\numberline {7.6}Translation functions *}{141}
   6.107 -\contentsline {subsection}{A simple example *}{142}
   6.108 -\contentsline {section}{\numberline {7.7}Example: some minimal logics}{143}
   6.109 +\contentsline {subsection}{Using the derived rules}{17}
   6.110 +\contentsline {subsection}{Derived rules versus definitions}{19}
   6.111 +\contentsline {chapter}{\numberline {3}Zermelo-Fraenkel Set Theory}{22}
   6.112 +\contentsline {section}{\numberline {3.1}Which version of axiomatic set theory?}{22}
   6.113 +\contentsline {section}{\numberline {3.2}The syntax of set theory}{23}
   6.114 +\contentsline {section}{\numberline {3.3}Binding operators}{25}
   6.115 +\contentsline {section}{\numberline {3.4}The Zermelo-Fraenkel axioms}{27}
   6.116 +\contentsline {section}{\numberline {3.5}From basic lemmas to function spaces}{30}
   6.117 +\contentsline {subsection}{Fundamental lemmas}{30}
   6.118 +\contentsline {subsection}{Unordered pairs and finite sets}{32}
   6.119 +\contentsline {subsection}{Subset and lattice properties}{32}
   6.120 +\contentsline {subsection}{Ordered pairs}{36}
   6.121 +\contentsline {subsection}{Relations}{36}
   6.122 +\contentsline {subsection}{Functions}{37}
   6.123 +\contentsline {section}{\numberline {3.6}Further developments}{38}
   6.124 +\contentsline {section}{\numberline {3.7}Simplification rules}{47}
   6.125 +\contentsline {section}{\numberline {3.8}The examples directory}{47}
   6.126 +\contentsline {section}{\numberline {3.9}A proof about powersets}{48}
   6.127 +\contentsline {section}{\numberline {3.10}Monotonicity of the union operator}{51}
   6.128 +\contentsline {section}{\numberline {3.11}Low-level reasoning about functions}{52}
   6.129 +\contentsline {chapter}{\numberline {4}Higher-Order Logic}{55}
   6.130 +\contentsline {section}{\numberline {4.1}Syntax}{55}
   6.131 +\contentsline {subsection}{Types}{57}
   6.132 +\contentsline {subsection}{Binders}{58}
   6.133 +\contentsline {subsection}{The {\ptt let} and {\ptt case} constructions}{58}
   6.134 +\contentsline {section}{\numberline {4.2}Rules of inference}{58}
   6.135 +\contentsline {section}{\numberline {4.3}A formulation of set theory}{60}
   6.136 +\contentsline {subsection}{Syntax of set theory}{65}
   6.137 +\contentsline {subsection}{Axioms and rules of set theory}{69}
   6.138 +\contentsline {section}{\numberline {4.4}Generic packages and classical reasoning}{71}
   6.139 +\contentsline {section}{\numberline {4.5}Types}{73}
   6.140 +\contentsline {subsection}{Product and sum types}{73}
   6.141 +\contentsline {subsection}{The type of natural numbers, {\ptt nat}}{73}
   6.142 +\contentsline {subsection}{The type constructor for lists, {\ptt list}}{76}
   6.143 +\contentsline {subsection}{The type constructor for lazy lists, {\ptt llist}}{76}
   6.144 +\contentsline {section}{\numberline {4.6}The examples directories}{79}
   6.145 +\contentsline {section}{\numberline {4.7}Example: Cantor's Theorem}{80}
   6.146 +\contentsline {chapter}{\numberline {5}First-Order Sequent Calculus}{82}
   6.147 +\contentsline {section}{\numberline {5.1}Unification for lists}{82}
   6.148 +\contentsline {section}{\numberline {5.2}Syntax and rules of inference}{84}
   6.149 +\contentsline {section}{\numberline {5.3}Tactics for the cut rule}{86}
   6.150 +\contentsline {section}{\numberline {5.4}Tactics for sequents}{87}
   6.151 +\contentsline {section}{\numberline {5.5}Packaging sequent rules}{88}
   6.152 +\contentsline {section}{\numberline {5.6}Proof procedures}{88}
   6.153 +\contentsline {subsection}{Method A}{89}
   6.154 +\contentsline {subsection}{Method B}{89}
   6.155 +\contentsline {section}{\numberline {5.7}A simple example of classical reasoning}{90}
   6.156 +\contentsline {section}{\numberline {5.8}A more complex proof}{91}
   6.157 +\contentsline {chapter}{\numberline {6}Constructive Type Theory}{93}
   6.158 +\contentsline {section}{\numberline {6.1}Syntax}{95}
   6.159 +\contentsline {section}{\numberline {6.2}Rules of inference}{95}
   6.160 +\contentsline {section}{\numberline {6.3}Rule lists}{101}
   6.161 +\contentsline {section}{\numberline {6.4}Tactics for subgoal reordering}{101}
   6.162 +\contentsline {section}{\numberline {6.5}Rewriting tactics}{102}
   6.163 +\contentsline {section}{\numberline {6.6}Tactics for logical reasoning}{103}
   6.164 +\contentsline {section}{\numberline {6.7}A theory of arithmetic}{105}
   6.165 +\contentsline {section}{\numberline {6.8}The examples directory}{105}
   6.166 +\contentsline {section}{\numberline {6.9}Example: type inference}{105}
   6.167 +\contentsline {section}{\numberline {6.10}An example of logical reasoning}{107}
   6.168 +\contentsline {section}{\numberline {6.11}Example: deriving a currying functional}{110}
   6.169 +\contentsline {section}{\numberline {6.12}Example: proving the Axiom of Choice}{111}
     7.1 --- a/doc-src/Ref/ref.bbl	Tue May 03 18:36:18 1994 +0200
     7.2 +++ b/doc-src/Ref/ref.bbl	Tue May 03 18:38:28 1994 +0200
     7.3 @@ -1,5 +1,10 @@
     7.4  \begin{thebibliography}{1}
     7.5  
     7.6 +\bibitem{bm88book}
     7.7 +Robert~S. Boyer and J~Strother Moore.
     7.8 +\newblock {\em A Computational Logic Handbook}.
     7.9 +\newblock Academic Press, 1988.
    7.10 +
    7.11  \bibitem{charniak80}
    7.12  E.~Charniak, C.~K. Riesbeck, and D.~V. McDermott.
    7.13  \newblock {\em Artificial Intelligence Programming}.
    7.14 @@ -11,11 +16,30 @@
    7.15    formula manipulation, with application to the {Church-Rosser Theorem}.
    7.16  \newblock {\em Indagationes Mathematicae}, 34:381--392, 1972.
    7.17  
    7.18 +\bibitem{OBJ}
    7.19 +K.~Futatsugi, J.A. Goguen, Jean-Pierre Jouannaud, and J.~Meseguer.
    7.20 +\newblock Principles of {OBJ2}.
    7.21 +\newblock In {\em Principles of Programming Languages}, pages 52--66, 1985.
    7.22 +
    7.23 +\bibitem{martin-nipkow}
    7.24 +Ursula Martin and Tobias Nipkow.
    7.25 +\newblock Ordered rewriting and confluence.
    7.26 +\newblock In M.~E. Stickel, editor, {\em 10th International Conference on
    7.27 +  Automated Deduction}, pages 366--380. Springer, 1990.
    7.28 +\newblock LNCS 449.
    7.29 +
    7.30  \bibitem{nipkow-prehofer}
    7.31  Tobias Nipkow and Christian Prehofer.
    7.32  \newblock Type checking type classes.
    7.33 -\newblock In {\em 20th ACM Symp.\ Principles of Programming Languages}, 1993.
    7.34 -\newblock To appear.
    7.35 +\newblock In {\em 20th Principles of Programming Languages}, pages 409--418.
    7.36 +  ACM Press, 1993.
    7.37 +\newblock Revised version to appear in \bgroup\em Journal of Functional
    7.38 +  Programming\egroup.
    7.39 +
    7.40 +\bibitem{nordstrom90}
    7.41 +Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith.
    7.42 +\newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}.
    7.43 +\newblock Oxford University Press, 1990.
    7.44  
    7.45  \bibitem{paulson91}
    7.46  Lawrence~C. Paulson.
     8.1 --- a/doc-src/Ref/ref.toc	Tue May 03 18:36:18 1994 +0200
     8.2 +++ b/doc-src/Ref/ref.toc	Tue May 03 18:38:28 1994 +0200
     8.3 @@ -1,151 +1,180 @@
     8.4 -\contentsline {chapter}{\numberline {1}Introduction}{1}
     8.5 +\contentsline {chapter}{\numberline {1}Basic Use of Isabelle}{1}
     8.6  \contentsline {section}{\numberline {1.1}Basic interaction with Isabelle}{1}
     8.7  \contentsline {section}{\numberline {1.2}Ending a session}{2}
     8.8 -\contentsline {section}{\numberline {1.3}Reading files of proofs and theories}{2}
     8.9 -\contentsline {section}{\numberline {1.4}Printing of terms and theorems}{3}
    8.10 -\contentsline {subsection}{Printing limits}{3}
    8.11 -\contentsline {subsection}{Printing of meta-level hypotheses}{3}
    8.12 -\contentsline {subsection}{Printing of types and sorts}{3}
    8.13 -\contentsline {subsection}{$\eta $-contraction before printing}{4}
    8.14 -\contentsline {section}{\numberline {1.5}Displaying exceptions as error messages}{4}
    8.15 -\contentsline {section}{\numberline {1.6}Shell scripts}{5}
    8.16 -\contentsline {chapter}{\numberline {2}Proof Management: The Subgoal Module}{6}
    8.17 -\contentsline {section}{\numberline {2.1}Basic commands}{6}
    8.18 -\contentsline {subsection}{Starting a backward proof}{6}
    8.19 -\contentsline {subsection}{Applying a tactic}{7}
    8.20 -\contentsline {subsection}{Extracting the proved theorem}{8}
    8.21 -\contentsline {subsection}{Undoing and backtracking}{8}
    8.22 -\contentsline {subsection}{Printing the proof state}{9}
    8.23 -\contentsline {subsection}{Timing}{9}
    8.24 -\contentsline {section}{\numberline {2.2}Shortcuts for applying tactics}{9}
    8.25 -\contentsline {subsection}{Refining a given subgoal}{9}
    8.26 -\contentsline {subsubsection}{Resolution with a list of theorems}{9}
    8.27 -\contentsline {subsection}{Scanning shortcuts}{10}
    8.28 -\contentsline {subsubsection}{Proof by assumption and resolution}{10}
    8.29 -\contentsline {subsubsection}{Resolution with a list of theorems}{10}
    8.30 -\contentsline {subsection}{Other shortcuts}{10}
    8.31 -\contentsline {section}{\numberline {2.3}Advanced features}{11}
    8.32 -\contentsline {subsection}{Executing batch proofs}{11}
    8.33 -\contentsline {subsection}{Managing multiple proofs}{11}
    8.34 -\contentsline {subsubsection}{The stack of proof states}{12}
    8.35 -\contentsline {subsubsection}{Saving and restoring proof states}{12}
    8.36 -\contentsline {subsection}{Debugging and inspecting}{12}
    8.37 -\contentsline {subsubsection}{Reading and printing terms}{13}
    8.38 -\contentsline {subsubsection}{Inspecting the proof state}{13}
    8.39 -\contentsline {subsubsection}{Filtering lists of rules}{13}
    8.40 -\contentsline {chapter}{\numberline {3}Tactics}{14}
    8.41 -\contentsline {section}{\numberline {3.1}Resolution and assumption tactics}{14}
    8.42 -\contentsline {subsection}{Resolution tactics}{14}
    8.43 -\contentsline {subsection}{Assumption tactics}{15}
    8.44 -\contentsline {subsection}{Matching tactics}{15}
    8.45 -\contentsline {subsection}{Resolution with instantiation}{15}
    8.46 -\contentsline {section}{\numberline {3.2}Other basic tactics}{16}
    8.47 -\contentsline {subsection}{Definitions and meta-level rewriting}{16}
    8.48 -\contentsline {subsection}{Tactic shortcuts}{17}
    8.49 -\contentsline {subsection}{Inserting premises and facts}{17}
    8.50 -\contentsline {subsection}{Theorems useful with tactics}{18}
    8.51 -\contentsline {section}{\numberline {3.3}Obscure tactics}{18}
    8.52 -\contentsline {subsection}{Tidying the proof state}{18}
    8.53 -\contentsline {subsection}{Renaming parameters in a goal}{18}
    8.54 -\contentsline {subsection}{Composition: resolution without lifting}{19}
    8.55 -\contentsline {section}{\numberline {3.4}Managing lots of rules}{19}
    8.56 -\contentsline {subsection}{Combined resolution and elim-resolution}{20}
    8.57 -\contentsline {subsection}{Discrimination nets for fast resolution}{20}
    8.58 -\contentsline {section}{\numberline {3.5}Programming tools for proof strategies}{21}
    8.59 -\contentsline {subsection}{Operations on type {\ptt tactic}}{22}
    8.60 -\contentsline {subsection}{Tracing}{22}
    8.61 -\contentsline {subsection}{Sequences}{23}
    8.62 -\contentsline {subsubsection}{Basic operations on sequences}{23}
    8.63 -\contentsline {subsubsection}{Converting between sequences and lists}{23}
    8.64 -\contentsline {subsubsection}{Combining sequences}{23}
    8.65 -\contentsline {chapter}{\numberline {4}Tacticals}{25}
    8.66 -\contentsline {section}{\numberline {4.1}The basic tacticals}{25}
    8.67 -\contentsline {subsection}{Joining two tactics}{25}
    8.68 -\contentsline {subsection}{Joining a list of tactics}{25}
    8.69 -\contentsline {subsection}{Repetition tacticals}{26}
    8.70 -\contentsline {subsection}{Identities for tacticals}{26}
    8.71 -\contentsline {section}{\numberline {4.2}Control and search tacticals}{27}
    8.72 -\contentsline {subsection}{Filtering a tactic's results}{27}
    8.73 -\contentsline {subsection}{Depth-first search}{28}
    8.74 -\contentsline {subsection}{Other search strategies}{28}
    8.75 -\contentsline {subsection}{Auxiliary tacticals for searching}{29}
    8.76 -\contentsline {subsection}{Predicates and functions useful for searching}{29}
    8.77 -\contentsline {section}{\numberline {4.3}Tacticals for subgoal numbering}{29}
    8.78 -\contentsline {subsection}{Restricting a tactic to one subgoal}{30}
    8.79 -\contentsline {subsection}{Scanning for a subgoal by number}{31}
    8.80 -\contentsline {subsection}{Joining tactic functions}{32}
    8.81 -\contentsline {subsection}{Applying a list of tactics to 1}{32}
    8.82 -\contentsline {chapter}{\numberline {5}Theorems and Forward Proof}{33}
    8.83 -\contentsline {section}{\numberline {5.1}Basic operations on theorems}{33}
    8.84 -\contentsline {subsection}{Pretty-printing a theorem}{33}
    8.85 -\contentsline {subsubsection}{Top-level commands}{33}
    8.86 -\contentsline {subsubsection}{Operations for programming}{34}
    8.87 -\contentsline {subsection}{Forwards proof: joining rules by resolution}{34}
    8.88 -\contentsline {subsection}{Expanding definitions in theorems}{35}
    8.89 -\contentsline {subsection}{Instantiating a theorem}{35}
    8.90 -\contentsline {subsection}{Miscellaneous forward rules}{35}
    8.91 -\contentsline {subsection}{Taking a theorem apart}{36}
    8.92 -\contentsline {subsection}{Tracing flags for unification}{36}
    8.93 -\contentsline {section}{\numberline {5.2}Primitive meta-level inference rules}{37}
    8.94 -\contentsline {subsection}{Propositional rules}{38}
    8.95 -\contentsline {subsubsection}{Assumption}{38}
    8.96 -\contentsline {subsubsection}{Implication}{38}
    8.97 -\contentsline {subsubsection}{Logical equivalence (equality)}{39}
    8.98 -\contentsline {subsection}{Equality rules}{39}
    8.99 -\contentsline {subsection}{The $\lambda $-conversion rules}{39}
   8.100 -\contentsline {subsection}{Universal quantifier rules}{40}
   8.101 -\contentsline {subsubsection}{Forall introduction}{40}
   8.102 -\contentsline {subsubsection}{Forall elimination}{40}
   8.103 -\contentsline {subsubsection}{Instantiation of unknowns}{41}
   8.104 -\contentsline {subsection}{Freezing/thawing type variables}{41}
   8.105 -\contentsline {section}{\numberline {5.3}Derived rules for goal-directed proof}{41}
   8.106 -\contentsline {subsection}{Proof by assumption}{41}
   8.107 -\contentsline {subsection}{Resolution}{41}
   8.108 -\contentsline {subsection}{Composition: resolution without lifting}{42}
   8.109 -\contentsline {subsection}{Other meta-rules}{42}
   8.110 -\contentsline {chapter}{\numberline {6}Theories, Terms and Types}{44}
   8.111 -\contentsline {section}{\numberline {6.1}Defining Theories}{44}
   8.112 -\contentsline {subsection}{Classes and types}{47}
   8.113 -\contentsline {section}{\numberline {6.2}Loading Theories}{47}
   8.114 -\contentsline {subsection}{Reading a new theory}{47}
   8.115 -\contentsline {subsection}{Filenames and paths}{48}
   8.116 -\contentsline {subsection}{Reloading a theory}{48}
   8.117 -\contentsline {subsection}{Pseudo theories}{48}
   8.118 -\contentsline {subsection}{Removing a theory}{49}
   8.119 -\contentsline {subsection}{Using Poly/{\psc ml}}{49}
   8.120 -\contentsline {section}{\numberline {6.3}Basic operations on theories}{49}
   8.121 -\contentsline {subsection}{Extracting an axiom from a theory}{49}
   8.122 -\contentsline {subsection}{Building a theory}{50}
   8.123 -\contentsline {subsection}{Inspecting a theory}{51}
   8.124 -\contentsline {section}{\numberline {6.4}Terms}{52}
   8.125 -\contentsline {section}{\numberline {6.5}Certified terms}{53}
   8.126 -\contentsline {subsection}{Printing terms}{53}
   8.127 -\contentsline {subsection}{Making and inspecting certified terms}{53}
   8.128 -\contentsline {section}{\numberline {6.6}Types}{54}
   8.129 -\contentsline {section}{\numberline {6.7}Certified types}{54}
   8.130 -\contentsline {subsection}{Printing types}{54}
   8.131 -\contentsline {subsection}{Making and inspecting certified types}{54}
   8.132 -\contentsline {chapter}{\numberline {7}Substitution Tactics}{56}
   8.133 -\contentsline {section}{\numberline {7.1}Simple substitution}{56}
   8.134 -\contentsline {section}{\numberline {7.2}Substitution in the hypotheses}{57}
   8.135 -\contentsline {section}{\numberline {7.3}Setting up {\ptt hyp_subst_tac}}{57}
   8.136 -\contentsline {chapter}{\numberline {8}Simplification}{60}
   8.137 -\contentsline {section}{\numberline {8.1}Simplification sets}{60}
   8.138 -\contentsline {subsection}{Rewrite rules}{60}
   8.139 -\contentsline {subsection}{Congruence rules}{61}
   8.140 -\contentsline {subsection}{The subgoaler}{61}
   8.141 -\contentsline {subsection}{The solver}{62}
   8.142 -\contentsline {subsection}{The looper}{62}
   8.143 -\contentsline {section}{\numberline {8.2}The simplification tactics}{62}
   8.144 -\contentsline {section}{\numberline {8.3}Example: using the simplifier}{63}
   8.145 -\contentsline {chapter}{\numberline {9}The classical theorem prover}{67}
   8.146 -\contentsline {section}{\numberline {9.1}The sequent calculus}{67}
   8.147 -\contentsline {section}{\numberline {9.2}Simulating sequents by natural deduction}{68}
   8.148 -\contentsline {section}{\numberline {9.3}Extra rules for the sequent calculus}{69}
   8.149 -\contentsline {section}{\numberline {9.4}Classical rule sets}{70}
   8.150 -\contentsline {section}{\numberline {9.5}The classical tactics}{71}
   8.151 -\contentsline {subsection}{Single-step tactics}{72}
   8.152 -\contentsline {subsection}{The automatic tactics}{72}
   8.153 -\contentsline {subsection}{Other useful tactics}{72}
   8.154 -\contentsline {subsection}{Creating swapped rules}{73}
   8.155 -\contentsline {section}{\numberline {9.6}Setting up the classical prover}{73}
   8.156 +\contentsline {section}{\numberline {1.3}Reading ML files}{2}
   8.157 +\contentsline {section}{\numberline {1.4}Printing of terms and theorems}{2}
   8.158 +\contentsline {subsection}{Printing limits}{2}
   8.159 +\contentsline {subsection}{Printing of hypotheses, types and sorts}{3}
   8.160 +\contentsline {subsection}{$\eta $-contraction before printing}{3}
   8.161 +\contentsline {section}{\numberline {1.5}Displaying exceptions as error messages}{3}
   8.162 +\contentsline {section}{\numberline {1.6}Shell scripts}{4}
   8.163 +\contentsline {chapter}{\numberline {2}Proof Management: The Subgoal Module}{5}
   8.164 +\contentsline {section}{\numberline {2.1}Basic commands}{5}
   8.165 +\contentsline {subsection}{Starting a backward proof}{5}
   8.166 +\contentsline {subsection}{Applying a tactic}{6}
   8.167 +\contentsline {subsection}{Extracting the proved theorem}{7}
   8.168 +\contentsline {subsection}{Undoing and backtracking}{7}
   8.169 +\contentsline {subsection}{Printing the proof state}{8}
   8.170 +\contentsline {subsection}{Timing}{8}
   8.171 +\contentsline {section}{\numberline {2.2}Shortcuts for applying tactics}{8}
   8.172 +\contentsline {subsection}{Refining a given subgoal}{8}
   8.173 +\contentsline {subsection}{Scanning shortcuts}{9}
   8.174 +\contentsline {subsection}{Other shortcuts}{9}
   8.175 +\contentsline {section}{\numberline {2.3}Executing batch proofs}{9}
   8.176 +\contentsline {section}{\numberline {2.4}Managing multiple proofs}{10}
   8.177 +\contentsline {subsection}{The stack of proof states}{11}
   8.178 +\contentsline {subsection}{Saving and restoring proof states}{11}
   8.179 +\contentsline {section}{\numberline {2.5}Debugging and inspecting}{11}
   8.180 +\contentsline {subsection}{Reading and printing terms}{11}
   8.181 +\contentsline {subsection}{Inspecting the proof state}{12}
   8.182 +\contentsline {subsection}{Filtering lists of rules}{12}
   8.183 +\contentsline {chapter}{\numberline {3}Tactics}{13}
   8.184 +\contentsline {section}{\numberline {3.1}Resolution and assumption tactics}{13}
   8.185 +\contentsline {subsection}{Resolution tactics}{13}
   8.186 +\contentsline {subsection}{Assumption tactics}{14}
   8.187 +\contentsline {subsection}{Matching tactics}{14}
   8.188 +\contentsline {subsection}{Resolution with instantiation}{14}
   8.189 +\contentsline {section}{\numberline {3.2}Other basic tactics}{15}
   8.190 +\contentsline {subsection}{Definitions and meta-level rewriting}{15}
   8.191 +\contentsline {subsection}{Tactic shortcuts}{16}
   8.192 +\contentsline {subsection}{Inserting premises and facts}{16}
   8.193 +\contentsline {subsection}{Theorems useful with tactics}{17}
   8.194 +\contentsline {section}{\numberline {3.3}Obscure tactics}{17}
   8.195 +\contentsline {subsection}{Tidying the proof state}{17}
   8.196 +\contentsline {subsection}{Renaming parameters in a goal}{17}
   8.197 +\contentsline {subsection}{Composition: resolution without lifting}{18}
   8.198 +\contentsline {section}{\numberline {3.4}Managing lots of rules}{18}
   8.199 +\contentsline {subsection}{Combined resolution and elim-resolution}{19}
   8.200 +\contentsline {subsection}{Discrimination nets for fast resolution}{19}
   8.201 +\contentsline {section}{\numberline {3.5}Programming tools for proof strategies}{20}
   8.202 +\contentsline {subsection}{Operations on type {\ptt tactic}}{21}
   8.203 +\contentsline {subsection}{Tracing}{21}
   8.204 +\contentsline {section}{\numberline {3.6}Sequences}{22}
   8.205 +\contentsline {subsection}{Basic operations on sequences}{22}
   8.206 +\contentsline {subsection}{Converting between sequences and lists}{22}
   8.207 +\contentsline {subsection}{Combining sequences}{22}
   8.208 +\contentsline {chapter}{\numberline {4}Tacticals}{24}
   8.209 +\contentsline {section}{\numberline {4.1}The basic tacticals}{24}
   8.210 +\contentsline {subsection}{Joining two tactics}{24}
   8.211 +\contentsline {subsection}{Joining a list of tactics}{24}
   8.212 +\contentsline {subsection}{Repetition tacticals}{25}
   8.213 +\contentsline {subsection}{Identities for tacticals}{25}
   8.214 +\contentsline {section}{\numberline {4.2}Control and search tacticals}{26}
   8.215 +\contentsline {subsection}{Filtering a tactic's results}{26}
   8.216 +\contentsline {subsection}{Depth-first search}{26}
   8.217 +\contentsline {subsection}{Other search strategies}{27}
   8.218 +\contentsline {subsection}{Auxiliary tacticals for searching}{27}
   8.219 +\contentsline {subsection}{Predicates and functions useful for searching}{28}
   8.220 +\contentsline {section}{\numberline {4.3}Tacticals for subgoal numbering}{28}
   8.221 +\contentsline {subsection}{Restricting a tactic to one subgoal}{28}
   8.222 +\contentsline {subsection}{Scanning for a subgoal by number}{29}
   8.223 +\contentsline {subsection}{Joining tactic functions}{30}
   8.224 +\contentsline {subsection}{Applying a list of tactics to 1}{31}
   8.225 +\contentsline {chapter}{\numberline {5}Theorems and Forward Proof}{32}
   8.226 +\contentsline {section}{\numberline {5.1}Basic operations on theorems}{32}
   8.227 +\contentsline {subsection}{Pretty-printing a theorem}{32}
   8.228 +\contentsline {subsection}{Forward proof: joining rules by resolution}{33}
   8.229 +\contentsline {subsection}{Expanding definitions in theorems}{33}
   8.230 +\contentsline {subsection}{Instantiating a theorem}{34}
   8.231 +\contentsline {subsection}{Miscellaneous forward rules}{34}
   8.232 +\contentsline {subsection}{Taking a theorem apart}{35}
   8.233 +\contentsline {subsection}{Tracing flags for unification}{35}
   8.234 +\contentsline {section}{\numberline {5.2}Primitive meta-level inference rules}{36}
   8.235 +\contentsline {subsection}{Assumption rule}{37}
   8.236 +\contentsline {subsection}{Implication rules}{37}
   8.237 +\contentsline {subsection}{Logical equivalence rules}{38}
   8.238 +\contentsline {subsection}{Equality rules}{38}
   8.239 +\contentsline {subsection}{The $\lambda $-conversion rules}{38}
   8.240 +\contentsline {subsection}{Forall introduction rules}{39}
   8.241 +\contentsline {subsection}{Forall elimination rules}{39}
   8.242 +\contentsline {subsection}{Instantiation of unknowns}{39}
   8.243 +\contentsline {subsection}{Freezing/thawing type unknowns}{40}
   8.244 +\contentsline {section}{\numberline {5.3}Derived rules for goal-directed proof}{40}
   8.245 +\contentsline {subsection}{Proof by assumption}{40}
   8.246 +\contentsline {subsection}{Resolution}{40}
   8.247 +\contentsline {subsection}{Composition: resolution without lifting}{40}
   8.248 +\contentsline {subsection}{Other meta-rules}{41}
   8.249 +\contentsline {chapter}{\numberline {6}Theories, Terms and Types}{42}
   8.250 +\contentsline {section}{\numberline {6.1}Defining theories}{42}
   8.251 +\contentsline {subsection}{*Classes and arities}{44}
   8.252 +\contentsline {section}{\numberline {6.2}Loading a new theory}{44}
   8.253 +\contentsline {section}{\numberline {6.3}Reloading modified theories}{45}
   8.254 +\contentsline {subsection}{Important note for Poly/ML users}{45}
   8.255 +\contentsline {subsection}{*Pseudo theories}{46}
   8.256 +\contentsline {section}{\numberline {6.4}Basic operations on theories}{47}
   8.257 +\contentsline {subsection}{Extracting an axiom from a theory}{47}
   8.258 +\contentsline {subsection}{Building a theory}{47}
   8.259 +\contentsline {subsection}{Inspecting a theory}{47}
   8.260 +\contentsline {section}{\numberline {6.5}Terms}{48}
   8.261 +\contentsline {section}{\numberline {6.6}Variable binding}{49}
   8.262 +\contentsline {section}{\numberline {6.7}Certified terms}{50}
   8.263 +\contentsline {subsection}{Printing terms}{50}
   8.264 +\contentsline {subsection}{Making and inspecting certified terms}{50}
   8.265 +\contentsline {section}{\numberline {6.8}Types}{50}
   8.266 +\contentsline {section}{\numberline {6.9}Certified types}{51}
   8.267 +\contentsline {subsection}{Printing types}{51}
   8.268 +\contentsline {subsection}{Making and inspecting certified types}{51}
   8.269 +\contentsline {chapter}{\numberline {7}Defining Logics}{52}
   8.270 +\contentsline {section}{\numberline {7.1}Priority grammars}{52}
   8.271 +\contentsline {section}{\numberline {7.2}The Pure syntax}{53}
   8.272 +\contentsline {subsection}{Logical types and default syntax}{55}
   8.273 +\contentsline {subsection}{Lexical matters}{55}
   8.274 +\contentsline {subsection}{*Inspecting the syntax}{56}
   8.275 +\contentsline {section}{\numberline {7.3}Mixfix declarations}{58}
   8.276 +\contentsline {subsection}{Grammar productions}{58}
   8.277 +\contentsline {subsection}{The general mixfix form}{59}
   8.278 +\contentsline {subsection}{Example: arithmetic expressions}{60}
   8.279 +\contentsline {subsection}{The mixfix template}{61}
   8.280 +\contentsline {subsection}{Infixes}{61}
   8.281 +\contentsline {subsection}{Binders}{62}
   8.282 +\contentsline {section}{\numberline {7.4}Example: some minimal logics}{62}
   8.283 +\contentsline {chapter}{\numberline {8}Syntax Transformations}{66}
   8.284 +\contentsline {section}{\numberline {8.1}Abstract syntax trees}{66}
   8.285 +\contentsline {section}{\numberline {8.2}Transforming parse trees to {\psc ast}{}s}{67}
   8.286 +\contentsline {section}{\numberline {8.3}Transforming {\psc ast}{}s to terms}{69}
   8.287 +\contentsline {section}{\numberline {8.4}Printing of terms}{69}
   8.288 +\contentsline {section}{\numberline {8.5}Macros: Syntactic rewriting}{71}
   8.289 +\contentsline {subsection}{Specifying macros}{72}
   8.290 +\contentsline {subsection}{Applying rules}{73}
   8.291 +\contentsline {subsection}{Example: the syntax of finite sets}{75}
   8.292 +\contentsline {subsection}{Example: a parse macro for dependent types}{76}
   8.293 +\contentsline {section}{\numberline {8.6}Translation functions}{76}
   8.294 +\contentsline {subsection}{Declaring translation functions}{77}
   8.295 +\contentsline {subsection}{The translation strategy}{77}
   8.296 +\contentsline {subsection}{Example: a print translation for dependent types}{78}
   8.297 +\contentsline {chapter}{\numberline {9}Substitution Tactics}{80}
   8.298 +\contentsline {section}{\numberline {9.1}Substitution rules}{80}
   8.299 +\contentsline {section}{\numberline {9.2}Substitution in the hypotheses}{81}
   8.300 +\contentsline {section}{\numberline {9.3}Setting up {\ptt hyp_subst_tac}}{82}
   8.301 +\contentsline {chapter}{\numberline {10}Simplification}{84}
   8.302 +\contentsline {section}{\numberline {10.1}Simplification sets}{84}
   8.303 +\contentsline {subsection}{Rewrite rules}{84}
   8.304 +\contentsline {subsection}{*Congruence rules}{85}
   8.305 +\contentsline {subsection}{*The subgoaler}{85}
   8.306 +\contentsline {subsection}{*The solver}{86}
   8.307 +\contentsline {subsection}{*The looper}{86}
   8.308 +\contentsline {section}{\numberline {10.2}The simplification tactics}{87}
   8.309 +\contentsline {section}{\numberline {10.3}Examples using the simplifier}{88}
   8.310 +\contentsline {subsection}{A trivial example}{88}
   8.311 +\contentsline {subsection}{An example of tracing}{89}
   8.312 +\contentsline {subsection}{Free variables and simplification}{90}
   8.313 +\contentsline {section}{\numberline {10.4}Permutative rewrite rules}{90}
   8.314 +\contentsline {subsection}{Example: sums of integers}{91}
   8.315 +\contentsline {subsection}{Re-orienting equalities}{93}
   8.316 +\contentsline {section}{\numberline {10.5}*Setting up the simplifier}{93}
   8.317 +\contentsline {subsection}{A collection of standard rewrite rules}{94}
   8.318 +\contentsline {subsection}{Functions for preprocessing the rewrite rules}{94}
   8.319 +\contentsline {subsection}{Making the initial simpset}{96}
   8.320 +\contentsline {subsection}{Case splitting}{97}
   8.321 +\contentsline {chapter}{\numberline {11}The Classical Reasoner}{98}
   8.322 +\contentsline {section}{\numberline {11.1}The sequent calculus}{98}
   8.323 +\contentsline {section}{\numberline {11.2}Simulating sequents by natural deduction}{99}
   8.324 +\contentsline {section}{\numberline {11.3}Extra rules for the sequent calculus}{100}
   8.325 +\contentsline {section}{\numberline {11.4}Classical rule sets}{101}
   8.326 +\contentsline {section}{\numberline {11.5}The classical tactics}{103}
   8.327 +\contentsline {subsection}{The automatic tactics}{103}
   8.328 +\contentsline {subsection}{Single-step tactics}{103}
   8.329 +\contentsline {subsection}{Other useful tactics}{104}
   8.330 +\contentsline {subsection}{Creating swapped rules}{104}
   8.331 +\contentsline {section}{\numberline {11.6}Setting up the classical reasoner}{104}
   8.332 +\contentsline {chapter}{\numberline {A}Syntax of Isabelle Theories}{107}
     9.1 --- a/doc-src/Ref/simplifier-eg.txt	Tue May 03 18:36:18 1994 +0200
     9.2 +++ b/doc-src/Ref/simplifier-eg.txt	Tue May 03 18:38:28 1994 +0200
     9.3 @@ -1,3 +1,5 @@
     9.4 +Pretty.setmargin 70;
     9.5 +
     9.6  > goal Nat.thy "m+0 = m";
     9.7  Level 0
     9.8  m + 0 = m
     9.9 @@ -71,3 +73,39 @@
    9.10  Level 3
    9.11  f(i + j) = i + f(j)
    9.12  No subgoals!
    9.13 +
    9.14 +
    9.15 +
    9.16 +> goal NatSum.thy "Suc(Suc(0))*sum(%i.i,Suc(n)) = n*Suc(n)";
    9.17 +Level 0
    9.18 +Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
    9.19 + 1. Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
    9.20 +
    9.21 +> by (simp_tac natsum_ss 1);
    9.22 +Level 1
    9.23 +Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
    9.24 + 1. n + (n + (sum(%i. i, n) + sum(%i. i, n))) = n + n * n
    9.25 +
    9.26 +> by (nat_ind_tac "n" 1);
    9.27 +Level 2
    9.28 +Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
    9.29 + 1. 0 + (0 + (sum(%i. i, 0) + sum(%i. i, 0))) = 0 + 0 * 0
    9.30 + 2. !!n1. n1 + (n1 + (sum(%i. i, n1) + sum(%i. i, n1))) =
    9.31 +          n1 + n1 * n1 ==>
    9.32 +          Suc(n1) +
    9.33 +          (Suc(n1) + (sum(%i. i, Suc(n1)) + sum(%i. i, Suc(n1)))) =
    9.34 +          Suc(n1) + Suc(n1) * Suc(n1)
    9.35 +
    9.36 +> by (simp_tac natsum_ss 1);
    9.37 +Level 3
    9.38 +Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
    9.39 + 1. !!n1. n1 + (n1 + (sum(%i. i, n1) + sum(%i. i, n1))) =
    9.40 +          n1 + n1 * n1 ==>
    9.41 +          Suc(n1) +
    9.42 +          (Suc(n1) + (sum(%i. i, Suc(n1)) + sum(%i. i, Suc(n1)))) =
    9.43 +          Suc(n1) + Suc(n1) * Suc(n1)
    9.44 +
    9.45 +> by (asm_simp_tac natsum_ss 1);
    9.46 +Level 4
    9.47 +Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
    9.48 +No subgoals!