# HG changeset patch
# User paulson
# Date 909161240 -7200
# Node ID 4f0978bb8271d3edc331421a67a1235327607455
# Parent  a53ffabc6804bf78a4edc9c0ec01a8ba892e5bab
auto update

diff -r a53ffabc6804 -r 4f0978bb8271 doc-src/Logics/logics.ind
--- a/doc-src/Logics/logics.ind	Fri Oct 23 16:46:33 1998 +0200
+++ b/doc-src/Logics/logics.ind	Fri Oct 23 18:47:20 1998 +0200
@@ -121,16 +121,16 @@
   \item {\tt ccontr} theorem, 66
   \item {\tt classical} theorem, 66
   \item {\tt coinduct} theorem, 45
-  \item {\tt coinductive}, 101--104
+  \item {\tt coinductive}, 102--105
   \item {\tt Collect} constant, 26, 27, 30, 68, 70
   \item {\tt Collect_def} theorem, 31
   \item {\tt Collect_mem_eq} theorem, 70, 71
   \item {\tt Collect_subset} theorem, 37
-  \item {\tt CollectD} theorem, 72, 107
+  \item {\tt CollectD} theorem, 72, 108
   \item {\tt CollectD1} theorem, 33, 35
   \item {\tt CollectD2} theorem, 33, 35
   \item {\tt CollectE} theorem, 33, 35, 72
-  \item {\tt CollectI} theorem, 35, 72, 107
+  \item {\tt CollectI} theorem, 35, 72, 108
   \item {\tt comp_assoc} theorem, 46
   \item {\tt comp_bij} theorem, 46
   \item {\tt comp_def} theorem, 46
@@ -187,7 +187,7 @@
 
   \indexspace
 
-  \item {\tt datatype}, 87--94
+  \item {\tt datatype}, 87--95
   \item {\tt Delsplits}, \bold{76}
   \item {\tt delsplits}, \bold{76}
   \item {\tt diff_0_eq_0} theorem, 133
@@ -280,7 +280,7 @@
   \item {\tt exhaust_tac}, \bold{92}
   \item {\tt exI} theorem, 8, 66
   \item {\tt exL} theorem, 112
-  \item {\tt Exp} theory, 105
+  \item {\tt Exp} theory, 106
   \item {\tt exR} theorem, 112, 116, 117
   \item {\tt exR_thin} theorem, 113, 117, 118
   \item {\tt ext} theorem, 63, 64
@@ -405,7 +405,7 @@
   \item {\textit {ind}} type, 78
   \item {\tt induct} theorem, 45
   \item {\tt induct_tac}, 80, \bold{92}
-  \item {\tt inductive}, 101--104
+  \item {\tt inductive}, 102--105
   \item {\tt Inf} constant, 26, 30
   \item {\tt infinity} theorem, 32
   \item {\tt inj} constant, 46, 75
@@ -502,7 +502,7 @@
   \item {\tt Let} constant, 25, 26, 60, 63
   \item {\tt let} symbol, 28, 61, 63
   \item {\tt Let_def} theorem, 25, 31, 63, 64
-  \item {\tt LFilter} theory, 105
+  \item {\tt LFilter} theory, 106
   \item {\tt lfp_def} theorem, 45
   \item {\tt lfp_greatest} theorem, 45
   \item {\tt lfp_lowerbound} theorem, 45
@@ -522,7 +522,7 @@
   \item {\tt LK} theory, 1, 109, 113
   \item {\tt LK_dup_pack}, \bold{116}, 117
   \item {\tt LK_pack}, \bold{116}
-  \item {\tt LList} theory, 105
+  \item {\tt LList} theory, 106
   \item {\tt logic} class, 5
 
   \indexspace
@@ -648,7 +648,7 @@
   \item {\tt Pow_mono} theorem, 53
   \item {\tt PowD} theorem, 34, 54, 73
   \item {\tt PowI} theorem, 34, 54, 73
-  \item {\tt primrec}, 95--98
+  \item {\tt primrec}, 95--99
   \item {\tt primrec} symbol, 80
   \item {\tt PrimReplace} constant, 26, 30
   \item priorities, 2
@@ -686,7 +686,7 @@
 
   \indexspace
 
-  \item {\tt range} constant, 26, 68, 106
+  \item {\tt range} constant, 26, 68, 107
   \item {\tt range_def} theorem, 32, 71
   \item {\tt range_of_fun} theorem, 40, 41
   \item {\tt range_subset} theorem, 39
@@ -699,11 +699,11 @@
   \item {\tt rec_0} theorem, 48
   \item {\tt rec_def} theorem, 48
   \item {\tt rec_succ} theorem, 48
-  \item {\tt recdef}, 98--101
+  \item {\tt recdef}, 99--102
   \item recursion
-    \subitem general, 98--101
-    \subitem primitive, 95--98
-  \item recursive functions, \see{recursion}{94}
+    \subitem general, 99--102
+    \subitem primitive, 95--99
+  \item recursive functions, \see{recursion}{95}
   \item {\tt red_if_equal} theorem, 125
   \item {\tt Reduce} constant, 122, 125, 131
   \item {\tt refl} theorem, 8, 63, 112