# HG changeset patch # User paulson # Date 830425474 -7200 # Node ID dd1ced7f1ff1ae9e901581e01b7f026aa21d6f8f # Parent d9aaae4ff6c3177280ed9af05e472bcbd7dc3e22 automatic updates diff -r d9aaae4ff6c3 -r dd1ced7f1ff1 doc-src/Intro/intro.ind --- a/doc-src/Intro/intro.ind Wed Apr 24 13:01:13 1996 +0200 +++ b/doc-src/Intro/intro.ind Thu Apr 25 11:44:34 1996 +0200 @@ -20,7 +20,7 @@ \item {\ptt allI} theorem, 35 \item arities \subitem declaring, 4, \bold{47} - \item {\ptt asm_simp_tac}, 56 + \item {\ptt asm_simp_tac}, 57 \item {\ptt assume_tac}, 28, 30, 35, 44 \item assumptions \subitem deleting, 19 @@ -29,14 +29,14 @@ \subitem of main goal, 39 \subitem use of, 16, 27 \item axioms - \subitem Peano, 51 + \subitem Peano, 52 \indexspace \item {\ptt ba}, 29 - \item {\ptt back}, 55, 59 + \item {\ptt back}, 55, 56, 59 \item backtracking - \subitem Prolog style, 58 + \subitem Prolog style, 59 \item {\ptt bd}, 29 \item {\ptt be}, 29 \item {\ptt br}, 29 @@ -44,7 +44,7 @@ \indexspace - \item {\ptt choplev}, 34, 35, 60 + \item {\ptt choplev}, 34, 35, 61 \item classes, 3 \subitem built-in, \bold{24} \item classical reasoner, 37 @@ -52,7 +52,7 @@ \item constants, 1 \subitem clashes with variables, 9 \subitem declaring, \bold{46} - \subitem overloaded, 50 + \subitem overloaded, 51 \subitem polymorphic, 3 \indexspace @@ -78,7 +78,7 @@ \subitem of induction, 54, 55 \subitem of simplification, 56 \subitem of tacticals, 35 - \subitem of theories, 46--52, 57 + \subitem of theories, 46, 48--53, 58 \subitem propositional, 16, 29, 31 \subitem with quantifiers, 17, 32, 33, 36 \item {\ptt exE} theorem, 36 @@ -101,7 +101,7 @@ \indexspace - \item {\ptt has_fewer_prems}, 60 + \item {\ptt has_fewer_prems}, 61 \item higher-order logic, 4 \indexspace @@ -109,7 +109,7 @@ \item identifiers, 23 \item {\ptt impI} theorem, 30, 42 \item infixes, 49 - \item instantiation, 53--57 + \item instantiation, 54--57 \item Isabelle \subitem object-logics supported, i \subitem overview, i @@ -135,30 +135,30 @@ \item meta-implication, \bold{5}, 6, 24 \item meta-quantifiers, \bold{5}, 7, 24 \item meta-rewriting, 41 - \item mixfix declarations, 49, 50, 52 + \item mixfix declarations, 49, 50, 53 \item ML, i \item {\ptt ML} section, 45 \item {\ptt mp} theorem, 26 \indexspace - \item {\ptt Nat} theory, 52 + \item {\ptt Nat} theory, 53 \item {\ptt nat} type, 1, 3 \item {\ptt not_def} theorem, 42 - \item {\ptt notE} theorem, \bold{43}, 54 - \item {\ptt notI} theorem, \bold{42}, 54 + \item {\ptt notE} theorem, \bold{43}, 55 + \item {\ptt notI} theorem, \bold{42}, 55 \indexspace \item {\ptt o} type, 1, 4 \item {\ptt ORELSE}, 35 - \item overloading, \bold{4}, 50 + \item overloading, \bold{4}, 51 \indexspace \item parameters, \bold{7}, 32 \subitem lifting over, 14 - \item {\ptt Prolog} theory, 57 + \item {\ptt Prolog} theory, 58 \item Prolog interpreter, \bold{57} \item proof state, 15 \item proofs @@ -178,12 +178,12 @@ \item {\ptt read_instantiate}, 28 \item {\ptt refl} theorem, 28 - \item {\ptt REPEAT}, 31, 36, 58, 60 - \item {\ptt res_inst_tac}, 53, 56 + \item {\ptt REPEAT}, 31, 36, 59, 60 + \item {\ptt res_inst_tac}, 54, 56 \item reserved words, 23 \item resolution, 10, \bold{11} \subitem in backward proof, 15 - \subitem with instantiation, 53 + \subitem with instantiation, 54 \item {\ptt resolve_tac}, 28, 30, 43, 55 \item {\ptt result}, 29, 40, 44 \item {\ptt rewrite_goals_tac}, 42 @@ -203,9 +203,9 @@ \indexspace \item search - \subitem depth-first, 59 + \subitem depth-first, 60 \item signatures, \bold{8} - \item {\ptt simp_tac}, 56 + \item {\ptt simp_tac}, 57 \item simplification, 56 \item simplification sets, 56 \item sort constraints, 24 @@ -213,8 +213,8 @@ \item {\ptt spec} theorem, 26, 34, 35 \item {\ptt standard}, 26 \item substitution, \bold{7} - \item {\ptt Suc_inject}, 54 - \item {\ptt Suc_neq_0}, 54 + \item {\ptt Suc_inject}, 55 + \item {\ptt Suc_neq_0}, 55 \item syntax \subitem of types and terms, 24 @@ -231,14 +231,14 @@ \subitem basic operations on, \bold{25} \subitem printing of, 25 \item theories, \bold{8} - \subitem defining, 44--53 + \subitem defining, 44--54 \item {\ptt thm} ML type, 25 \item {\ptt topthm}, 40 \item {\ptt Trueprop} constant, 6, 24 \item type constraints, 24 \item type constructors, 1 \item type identifiers, 23 - \item type synonyms, \bold{48} + \item type synonyms, \bold{49} \item types \subitem declaring, \bold{47} \subitem function, 1 diff -r d9aaae4ff6c3 -r dd1ced7f1ff1 doc-src/Logics/logics.bbl --- a/doc-src/Logics/logics.bbl Wed Apr 24 13:01:13 1996 +0200 +++ b/doc-src/Logics/logics.bbl Thu Apr 25 11:44:34 1996 +0200 @@ -157,14 +157,6 @@ \newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}. \newblock Cambridge University Press, 1987. -\bibitem{paulson-coind} -Lawrence~C. Paulson. -\newblock Co-induction and co-recursion in higher-order logic. -\newblock Technical Report 304, Computer Laboratory, University of Cambridge, - July 1993. -\newblock To appear in the Festscrift for Alonzo Church, edited by A. Anderson - and M. Zeleny. - \bibitem{paulson-set-I} Lawrence~C. Paulson. \newblock Set theory for verification: {I}. {From} foundations to functions. @@ -182,6 +174,12 @@ \newblock Set theory for verification: {II}. {Induction} and recursion. \newblock {\em Journal of Automated Reasoning}, 15(2):167--215, 1995. +\bibitem{paulson-coind} +Lawrence~C. Paulson. +\newblock Mechanizing coinduction and corecursion in higher-order logic. +\newblock {\em Journal of Logic and Computation}, 1996. +\newblock In press. + \bibitem{paulson-COLOG} Lawrence~C. Paulson. \newblock A formulation of the simple theory of types (for {Isabelle}). diff -r d9aaae4ff6c3 -r dd1ced7f1ff1 doc-src/ind-defs.bbl --- a/doc-src/ind-defs.bbl Wed Apr 24 13:01:13 1996 +0200 +++ b/doc-src/ind-defs.bbl Thu Apr 25 11:44:34 1996 +0200 @@ -92,7 +92,9 @@ \bibitem{nipkow-CR} Nipkow, T., \newblock More {Church-Rosser} proofs (in {Isabelle/HOL}), -\newblock Tech. rep., T. U. Munich, 1996 +\newblock In {\em Automated Deduction --- {CADE}-13\/} (1996), M.~McRobbie, + J.~Slaney, Eds., LNAI, Springer, p.~?, +\newblock in press \bibitem{paulin92} Paulin-Mohring, C.,