# HG changeset patch
# User wenzelm
# Date 863448298 -7200
# Node ID 22ebe2bd5e455f328cb0c594e4c40b122e153405
# Parent  2bd87b6682bff4e57c9add5cadafa5899fda5cf8
SYNC;

diff -r 2bd87b6682bf -r 22ebe2bd5e45 doc-src/Logics/logics.ind
--- a/doc-src/Logics/logics.ind	Mon May 12 14:58:45 1997 +0200
+++ b/doc-src/Logics/logics.ind	Mon May 12 16:44:58 1997 +0200
@@ -118,7 +118,7 @@
   \item {\tt ccontr} theorem, 65
   \item {\tt classical} theorem, 65
   \item {\tt coinduct} theorem, 43
-  \item {\tt coinductive}, 91--94
+  \item {\tt coinductive}, 90--94
   \item {\tt Collect} constant, 24, 25, 28, 67, 69
   \item {\tt Collect_def} theorem, 29
   \item {\tt Collect_mem_eq} theorem, 69, 70
@@ -184,7 +184,7 @@
 
   \indexspace
 
-  \item {\tt datatype}, 84--91
+  \item {\tt datatype}, 84--90
   \item {\tt deepen_tac}, 15
   \item {\tt diff_0_eq_0} theorem, 122
   \item {\tt Diff_cancel} theorem, 40
@@ -401,8 +401,8 @@
   \item {\tt in} symbol, 26, 60
   \item {\tt ind} type, 78
   \item {\tt induct} theorem, 43
-  \item {\tt induct_tac}, 79, \bold{87}
-  \item {\tt inductive}, 91--94
+  \item {\tt induct_tac}, 79, \bold{85}
+  \item {\tt inductive}, 90--94
   \item {\tt Inf} constant, 24, 28
   \item {\tt infinity} theorem, 30
   \item {\tt inj} constant, 44, 74
@@ -507,7 +507,7 @@
   \item {\tt lfp_Tarski} theorem, 43
   \item {\tt List} theory, 79, 80
   \item {\tt list} constant, 48
-  \item {\tt list} type, 79, 95
+  \item {\tt list} type, 79, 94
   \item {\tt List.induct} theorem, 48
   \item {\tt list_case} constant, 48
   \item {\tt list_mono} theorem, 48
@@ -643,8 +643,8 @@
   \item {\tt Pow_mono} theorem, 51
   \item {\tt PowD} theorem, 32, 52, 72
   \item {\tt PowI} theorem, 32, 52, 72
-  \item primitive recursion, 89--91
-  \item {\tt primrec}, 89--91
+  \item primitive recursion, 89--90
+  \item {\tt primrec}, 89--90
   \item {\tt primrec} symbol, 78
   \item {\tt PrimReplace} constant, 24, 28
   \item priorities, 2
@@ -667,6 +667,7 @@
   \item {\tt qcase_def} theorem, 42
   \item {\tt qconverse} constant, 41
   \item {\tt qconverse_def} theorem, 42
+  \item {\tt qed_spec_mp}, 87
   \item {\tt qfsplit_def} theorem, 42
   \item {\tt QInl_def} theorem, 42
   \item {\tt QInr_def} theorem, 42