automatic updates

--- 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

--- 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}).

--- 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.,