# HG changeset patch
# User paulson
# Date 818425375 -3600
# Node ID 1f00494e37a5ac6cd3afa7086e06b2d24ae452af
# Parent  b8de98c2c29c54b1909e9ad8c4ea82eaa60a92eb
trivial, automatic changes

diff -r b8de98c2c29c -r 1f00494e37a5 doc-src/Intro/intro.ind
--- a/doc-src/Intro/intro.ind	Fri Dec 08 11:57:02 1995 +0100
+++ b/doc-src/Intro/intro.ind	Fri Dec 08 13:22:55 1995 +0100
@@ -19,7 +19,7 @@
 
   \item {\ptt allI} theorem, 35
   \item arities
-    \subitem declaring, 4, \bold{46}
+    \subitem declaring, 4, \bold{47}
   \item {\ptt asm_simp_tac}, 56
   \item {\ptt assume_tac}, 28, 30, 35, 44
   \item assumptions
@@ -34,7 +34,7 @@
   \indexspace
 
   \item {\ptt ba}, 29
-  \item {\ptt back}, 54, 55, 58
+  \item {\ptt back}, 55, 59
   \item backtracking
     \subitem Prolog style, 58
   \item {\ptt bd}, 29
@@ -59,10 +59,10 @@
 
   \item definitions, 5, \bold{46}
     \subitem and derived rules, 41--44
-  \item {\ptt DEPTH_FIRST}, 59
+  \item {\ptt DEPTH_FIRST}, 60
   \item destruct-resolution, 21, 29
   \item {\ptt disjE} theorem, 30
-  \item {\ptt dres_inst_tac}, 53
+  \item {\ptt dres_inst_tac}, 54
   \item {\ptt dresolve_tac}, 29, 31, 36
 
   \indexspace
@@ -71,12 +71,12 @@
   \item elim-resolution, \bold{19}, 28
   \item equality
     \subitem polymorphic, 3
-  \item {\ptt eres_inst_tac}, 53
+  \item {\ptt eres_inst_tac}, 54
   \item {\ptt eresolve_tac}, 28, 31, 36, 44
   \item examples
     \subitem of deriving rules, 39
-    \subitem of induction, 53, 54
-    \subitem of simplification, 55
+    \subitem of induction, 54, 55
+    \subitem of simplification, 56
     \subitem of tacticals, 35
     \subitem of theories, 46--52, 57
     \subitem propositional, 16, 29, 31
@@ -108,8 +108,8 @@
 
   \item identifiers, 23
   \item {\ptt impI} theorem, 30, 42
-  \item infixes, 48
-  \item instantiation, 53--56
+  \item infixes, 49
+  \item instantiation, 53--57
   \item Isabelle
     \subitem object-logics supported, i
     \subitem overview, i
@@ -135,7 +135,7 @@
   \item meta-implication, \bold{5}, 6, 24
   \item meta-quantifiers, \bold{5}, 7, 24
   \item meta-rewriting, 41
-  \item mixfix declarations, 49, 52
+  \item mixfix declarations, 49, 50, 52
   \item ML, i
   \item {\ptt ML} section, 45
   \item {\ptt mp} theorem, 26
@@ -159,7 +159,7 @@
   \item parameters, \bold{7}, 32
     \subitem lifting over, 14
   \item {\ptt Prolog} theory, 57
-  \item Prolog interpreter, \bold{56}
+  \item Prolog interpreter, \bold{57}
   \item proof state, 15
   \item proofs
     \subitem commands for, 29
@@ -178,13 +178,13 @@
 
   \item {\ptt read_instantiate}, 28
   \item {\ptt refl} theorem, 28
-  \item {\ptt REPEAT}, 31, 36, 58, 59
-  \item {\ptt res_inst_tac}, 53, 55
+  \item {\ptt REPEAT}, 31, 36, 58, 60
+  \item {\ptt res_inst_tac}, 53, 56
   \item reserved words, 23
   \item resolution, 10, \bold{11}
     \subitem in backward proof, 15
     \subitem with instantiation, 53
-  \item {\ptt resolve_tac}, 28, 30, 43, 54
+  \item {\ptt resolve_tac}, 28, 30, 43, 55
   \item {\ptt result}, 29, 40, 44
   \item {\ptt rewrite_goals_tac}, 42
   \item {\ptt rewrite_rule}, 43
@@ -206,8 +206,8 @@
     \subitem depth-first, 59
   \item signatures, \bold{8}
   \item {\ptt simp_tac}, 56
-  \item simplification, 55
-  \item simplification sets, 55
+  \item simplification, 56
+  \item simplification sets, 56
   \item sort constraints, 24
   \item sorts, \bold{4}
   \item {\ptt spec} theorem, 26, 34, 35
@@ -240,7 +240,7 @@
   \item type identifiers, 23
   \item type synonyms, \bold{48}
   \item types
-    \subitem declaring, \bold{46}
+    \subitem declaring, \bold{47}
     \subitem function, 1
     \subitem higher, \bold{5}
     \subitem polymorphic, \bold{3}
@@ -251,7 +251,7 @@
 
   \item {\ptt undo}, 29
   \item unification
-    \subitem higher-order, \bold{10}, 54
+    \subitem higher-order, \bold{10}, 55
     \subitem incompleteness of, 11
   \item unknowns, 9, 23, 32
     \subitem function, \bold{11}, 27, 32
diff -r b8de98c2c29c -r 1f00494e37a5 doc-src/Logics/logics.bbl
--- a/doc-src/Logics/logics.bbl	Fri Dec 08 11:57:02 1995 +0100
+++ b/doc-src/Logics/logics.bbl	Fri Dec 08 13:22:55 1995 +0100
@@ -73,8 +73,7 @@
 \newblock A logic program for transforming sequent proofs to natural deduction
   proofs.
 \newblock In Peter Schroeder-Heister, editor, {\em Extensions of Logic
-  Programming}, pages 157--178. Springer, 1991.
-\newblock LNAI 475.
+  Programming}, LNAI 475, pages 157--178. Springer, 1991.
 
 \bibitem{frost93}
 Jacob Frost.
@@ -114,8 +113,7 @@
 Lena Magnusson and Bengt {Nordstr\"om}.
 \newblock The {ALF} proof editor and its proof engine.
 \newblock In {\em Types for Proofs and Programs: International Workshop {TYPES
-  '93}}, pages 213--237. Springer, published 1994.
-\newblock LNCS 806.
+  '93}}, LNCS 806, pages 213--237. Springer, published 1994.
 
 \bibitem{mw81}
 Zohar Manna and Richard Waldinger.
@@ -170,39 +168,37 @@
 \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.
 \newblock {\em Journal of Automated Reasoning}, 11(3):353--389, 1993.
 
-\bibitem{paulson-set-II}
-Lawrence~C. Paulson.
-\newblock Set theory for verification: {II}. {Induction} and recursion.
-\newblock Technical Report 312, Computer Laboratory, University of Cambridge,
-  1993.
-\newblock To appear in Journal of Automated Reasoning.
-
-\bibitem{paulson-final}
-Lawrence~C. Paulson.
-\newblock A concrete final coalgebra theorem for {ZF} set theory.
-\newblock Technical Report 334, Computer Laboratory, University of Cambridge,
-  1994.
-
 \bibitem{paulson-CADE}
 Lawrence~C. Paulson.
 \newblock A fixedpoint approach to implementing (co)inductive definitions.
 \newblock In Alan Bundy, editor, {\em 12th International Conference on
-  Automated Deduction}, pages 148--161. Springer, 1994.
-\newblock LNAI 814.
+  Automated Deduction}, LNAI 814, pages 148--161. Springer, 1994.
+
+\bibitem{paulson-set-II}
+Lawrence~C. Paulson.
+\newblock Set theory for verification: {II}. {Induction} and recursion.
+\newblock {\em Journal of Automated Reasoning}, 15(2):167--215, 1995.
 
 \bibitem{paulson-COLOG}
 Lawrence~C. Paulson.
 \newblock A formulation of the simple theory of types (for {Isabelle}).
 \newblock In P.~Martin-L\"of and G.~Mints, editors, {\em COLOG-88:
-  International Conference on Computer Logic}, pages 246--274, Tallinn,
-  Published 1990. Estonian Academy of Sciences, Springer.
-\newblock LNCS 417.
+  International Conference on Computer Logic}, LNCS 417, pages 246--274,
+  Tallinn, Published 1990. Estonian Academy of Sciences, Springer.
+
+\bibitem{paulson-final}
+Lawrence~C. Paulson.
+\newblock A concrete final coalgebra theorem for {ZF} set theory.
+\newblock In {\em Types for Proofs and Programs: International Workshop {TYPES
+  '94}}, LNCS 996, pages 120--139. Springer, published 1995.
 
 \bibitem{pelletier86}
 F.~J. Pelletier.
diff -r b8de98c2c29c -r 1f00494e37a5 doc-src/Ref/ref.bbl
--- a/doc-src/Ref/ref.bbl	Fri Dec 08 11:57:02 1995 +0100
+++ b/doc-src/Ref/ref.bbl	Fri Dec 08 13:22:55 1995 +0100
@@ -26,8 +26,7 @@
 Ursula Martin and Tobias Nipkow.
 \newblock Ordered rewriting and confluence.
 \newblock In Mark~E. Stickel, editor, {\em 10th International Conference on
-  Automated Deduction}, pages 366--380. Springer, 1990.
-\newblock LNAI 449.
+  Automated Deduction}, LNAI 449, pages 366--380. Springer, 1990.
 
 \bibitem{Nipkow-LICS-93}
 Tobias Nipkow.