--- a/doc-src/Intro/intro.bbl Wed May 05 18:24:57 1999 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,106 +0,0 @@
-\begin{thebibliography}{10}
-
-\bibitem{galton90}
-Antony Galton.
-\newblock {\em Logic for Information Technology}.
-\newblock Wiley, 1990.
-
-\bibitem{mgordon-hol}
-M.~J.~C. Gordon and T.~F. Melham.
-\newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher
- Order Logic}.
-\newblock Cambridge University Press, 1993.
-
-\bibitem{mgordon79}
-Michael J.~C. Gordon, Robin Milner, and Christopher~P. Wadsworth.
-\newblock {\em Edinburgh {LCF}: A Mechanised Logic of Computation}.
-\newblock LNCS 78. Springer, 1979.
-
-\bibitem{haskell-tutorial}
-Paul Hudak and Joseph~H. Fasel.
-\newblock A gentle introduction to {Haskell}.
-\newblock {\em {SIGPLAN} Notices}, 27(5), May 1992.
-
-\bibitem{haskell-report}
-Paul Hudak, Simon~Peyton Jones, and Philip Wadler.
-\newblock Report on the programming language {Haskell}: A non-strict, purely
- functional language.
-\newblock {\em {SIGPLAN} Notices}, 27(5), May 1992.
-\newblock Version 1.2.
-
-\bibitem{huet75}
-G.~P. Huet.
-\newblock A unification algorithm for typed $\lambda$-calculus.
-\newblock {\em Theoretical Computer Science}, 1:27--57, 1975.
-
-\bibitem{miller-mixed}
-Dale Miller.
-\newblock Unification under a mixed prefix.
-\newblock {\em Journal of Symbolic Computation}, 14(4):321--358, 1992.
-
-\bibitem{nipkow-prehofer}
-Tobias Nipkow and Christian Prehofer.
-\newblock Type reconstruction for type classes.
-\newblock {\em Journal of Functional Programming}, 5(2):201--224, 1995.
-
-\bibitem{nordstrom90}
-Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith.
-\newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}.
-\newblock Oxford University Press, 1990.
-
-\bibitem{paulson-natural}
-Lawrence~C. Paulson.
-\newblock Natural deduction as higher-order resolution.
-\newblock {\em Journal of Logic Programming}, 3:237--258, 1986.
-
-\bibitem{paulson87}
-Lawrence~C. Paulson.
-\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}.
-\newblock Cambridge University Press, 1987.
-
-\bibitem{paulson-found}
-Lawrence~C. Paulson.
-\newblock The foundation of a generic theorem prover.
-\newblock {\em Journal of Automated Reasoning}, 5(3):363--397, 1989.
-
-\bibitem{paulson700}
-Lawrence~C. Paulson.
-\newblock {Isabelle}: The next 700 theorem provers.
-\newblock In P.~Odifreddi, editor, {\em Logic and Computer Science}, pages
- 361--386. Academic Press, 1990.
-
-\bibitem{paulson-handbook}
-Lawrence~C. Paulson.
-\newblock Designing a theorem prover.
-\newblock In S.~Abramsky, D.~M. Gabbay, and T.~S.~E. Maibaum, editors, {\em
- Handbook of Logic in Computer Science}, volume~2, pages 415--475. Oxford
- University Press, 1992.
-
-\bibitem{paulson-ml2}
-Lawrence~C. Paulson.
-\newblock {\em {ML} for the Working Programmer}.
-\newblock Cambridge University Press, 2nd edition, 1996.
-
-\bibitem{pelletier86}
-F.~J. Pelletier.
-\newblock Seventy-five problems for testing automatic theorem provers.
-\newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.
-\newblock Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135.
-
-\bibitem{reeves90}
-Steve Reeves and Michael Clarke.
-\newblock {\em Logic for Computer Science}.
-\newblock Addison-Wesley, 1990.
-
-\bibitem{suppes72}
-Patrick Suppes.
-\newblock {\em Axiomatic Set Theory}.
-\newblock Dover, 1972.
-
-\bibitem{wos-bledsoe}
-Larry Wos.
-\newblock Automated reasoning and {Bledsoe's} dream for the field.
-\newblock In Robert~S. Boyer, editor, {\em Automated Reasoning: Essays in Honor
- of {Woody Bledsoe}}, pages 297--342. Kluwer Academic Publishers, 1991.
-
-\end{thebibliography}
--- a/doc-src/Intro/intro.ind Wed May 05 18:24:57 1999 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,267 +0,0 @@
-\begin{theindex}
-
- \item {\tt !!} symbol, 26
- \item {\tt\%} symbol, 25
- \item {\tt ::} symbol, 25
- \item {\tt ==} symbol, 26
- \item {\tt ==>} symbol, 26
- \item {\tt =>} symbol, 25
- \item {\tt =?=} symbol, 26
- \item {\tt [} symbol, 25
- \item {\tt [|} symbol, 26
- \item {\tt ]} symbol, 25
- \item {\tt\ttlbrace} symbol, 25
- \item {\tt\ttrbrace} symbol, 25
- \item {\tt |]} symbol, 26
-
- \indexspace
-
- \item {\tt allI} theorem, 38
- \item arities
- \subitem declaring, 4, \bold{48}
- \item {\tt Asm_simp_tac}, 59
- \item {\tt assume_tac}, 30, 32, 38
- \item assumptions
- \subitem deleting, 20
- \subitem discharge of, 7
- \subitem lifting over, 14
- \subitem of main goal, 41
- \subitem use of, 16, 28
- \item axioms
- \subitem Peano, 54
-
- \indexspace
-
- \item {\tt ba}, 31
- \item {\tt back}, 58, 62
- \item backtracking
- \subitem Prolog style, 61
- \item {\tt bd}, 31
- \item {\tt be}, 31
- \item {\tt Blast_tac}, 39, 40
- \item {\tt br}, 31
- \item {\tt by}, 31
-
- \indexspace
-
- \item {\tt choplev}, 37, 38, 64
- \item classes, 3
- \subitem built-in, \bold{25}
- \item classical reasoner, 39
- \item {\tt conjunct1} theorem, 28
- \item constants, 3
- \subitem clashes with variables, 9
- \subitem declaring, \bold{47}
- \subitem overloaded, 53
- \subitem polymorphic, 3
- \item {\tt CPure} theory, 46
-
- \indexspace
-
- \item definitions, 6, \bold{47}
- \subitem and derived rules, 43--45
- \item {\tt DEPTH_FIRST}, 63
- \item destruct-resolution, 22, 30
- \item {\tt disjE} theorem, 31
- \item {\tt dres_inst_tac}, 56
- \item {\tt dresolve_tac}, 30, 33, 39
-
- \indexspace
-
- \item eigenvariables, \see{parameters}{8}
- \item elim-resolution, \bold{20}, 30
- \item equality
- \subitem polymorphic, 3
- \item {\tt eres_inst_tac}, 56
- \item {\tt eresolve_tac}, 30, 33, 39
- \item examples
- \subitem of deriving rules, 41
- \subitem of induction, 56, 57
- \subitem of simplification, 59
- \subitem of tacticals, 37
- \subitem of theories, 47, 49--53, 55, 60
- \subitem propositional, 17, 31, 33
- \subitem with quantifiers, 18, 34, 36, 38
- \item {\tt exE} theorem, 38
-
- \indexspace
-
- \item {\tt FalseE} theorem, 45
- \item first-order logic, 1
- \item flex-flex constraints, 6, 26, \bold{29}
- \item {\tt flexflex_rule}, 29
- \item forward proof, 21, 24--30
- \item {\tt fun} type, 1, 4
- \item function applications, 1, 8
-
- \indexspace
-
- \item {\tt Goal}, 30, 41
- \item {\tt Goalw}, 44
-
- \indexspace
-
- \item {\tt has_fewer_prems}, 63
- \item higher-order logic, 4
-
- \indexspace
-
- \item identifiers, 24
- \item {\tt impI} theorem, 31, 44
- \item infixes, 51
- \item instantiation, 56--59
- \item Isabelle
- \subitem object-logics supported, i
- \subitem overview, i
- \subitem release history, i
-
- \indexspace
-
- \item $\lambda$-abstractions, 1, 8, 25
- \item $\lambda$-calculus, 1
- \item LCF, i
- \item LCF system, 15, 27
- \item level of a proof, 31
- \item lifting, \bold{14}
- \item {\tt logic} class, 3, 6, 25
-
- \indexspace
-
- \item major premise, \bold{21}
- \item {\tt Match} exception, 42
- \item meta-assumptions
- \subitem syntax of, 22
- \item meta-equality, \bold{5}, 26
- \item meta-implication, \bold{5}, 7, 26
- \item meta-quantifiers, \bold{5}, 8, 26
- \item meta-rewriting, 43
- \item mixfix declarations, 51, 52, 55
- \item ML, i
- \item {\tt ML} section, 46
- \item {\tt mp} theorem, 27, 28
-
- \indexspace
-
- \item {\tt Nat} theory, 55
- \item {\tt nat} type, 3
- \item {\tt not_def} theorem, 44
- \item {\tt notE} theorem, 57
- \item {\tt notI} theorem, \bold{44}, 57
-
- \indexspace
-
- \item {\tt o} type, 3, 4
- \item {\tt ORELSE}, 38
- \item overloading, \bold{4}, 52
-
- \indexspace
-
- \item parameters, \bold{8}, 34
- \subitem lifting over, 15
- \item {\tt Prolog} theory, 60
- \item Prolog interpreter, \bold{60}
- \item proof state, 16
- \item proofs
- \subitem commands for, 30
- \item {\tt PROP} symbol, 26
- \item {\textit {prop}} type, 25, 26
- \item {\tt prop} type, 6
- \item {\tt prth}, 27
- \item {\tt prthq}, 27, 29
- \item {\tt prths}, 27
- \item {\tt Pure} theory, 46
-
- \indexspace
-
- \item {\tt qed}, 31, 43
- \item quantifiers, 5, 8, 34
-
- \indexspace
-
- \item {\tt read_instantiate}, 29
- \item {\tt refl} theorem, 29
- \item {\tt REPEAT}, 34, 38, 61, 63
- \item {\tt res_inst_tac}, 56, 59
- \item reserved words, 24
- \item resolution, 10, \bold{12}
- \subitem in backward proof, 15
- \subitem with instantiation, 56
- \item {\tt resolve_tac}, 30, 31, 57
- \item {\tt result}, 31
- \item {\tt rewrite_goals_tac}, 44, 45
- \item {\tt rewrite_rule}, 45
- \item {\tt RL}, 29
- \item {\tt RLN}, 29
- \item {\tt RS}, 27, 29
- \item {\tt RSN}, 27, 29
- \item rules
- \subitem declaring, 47
- \subitem derived, 13, \bold{22}, 41, 43
- \subitem destruction, 21
- \subitem elimination, 21
- \subitem propositional, 6
- \subitem quantifier, 8
-
- \indexspace
-
- \item search
- \subitem depth-first, 62
- \item signatures, \bold{9}
- \item {\tt Simp_tac}, 59
- \item simplification, 59
- \item simplification sets, 59
- \item sort constraints, 25
- \item sorts, \bold{5}
- \item {\tt spec} theorem, 28, 36, 38
- \item {\tt standard}, 27
- \item substitution, \bold{8}
- \item {\tt Suc_inject}, 57
- \item {\tt Suc_neq_0}, 57
- \item syntax
- \subitem of types and terms, 25
-
- \indexspace
-
- \item tacticals, \bold{19}, 37
- \item tactics, \bold{19}
- \subitem assumption, 30
- \subitem resolution, 30
- \item {\tt term} class, 3
- \item terms
- \subitem syntax of, 1, \bold{25}
- \item theorems
- \subitem basic operations on, \bold{27}
- \subitem printing of, 27
- \item theories, \bold{9}
- \subitem defining, 46--56
- \item {\tt thm} ML type, 27
- \item {\tt topthm}, 43
- \item {\tt Trueprop} constant, 6, 7, 26
- \item type constraints, 25
- \item type constructors, 1
- \item type identifiers, 25
- \item type synonyms, \bold{50}
- \item types
- \subitem declaring, \bold{48}
- \subitem function, 1
- \subitem higher, \bold{5}
- \subitem polymorphic, \bold{3}
- \subitem simple, \bold{1}
- \subitem syntax of, 1, \bold{25}
-
- \indexspace
-
- \item {\tt undo}, 31
- \item unification
- \subitem higher-order, \bold{11}, 57
- \subitem incompleteness of, 11
- \item unknowns, 10, 25, 34
- \subitem function, \bold{11}, 29, 34
- \item {\tt use_thy}, \bold{46, 47}
-
- \indexspace
-
- \item variables
- \subitem bound, 8
-
-\end{theindex}