1.1 --- a/doc-src/Logics/logics.ind Thu May 22 10:49:33 1997 +0200
1.2 +++ b/doc-src/Logics/logics.ind Thu May 22 11:16:24 1997 +0200
1.3 @@ -118,7 +118,7 @@
1.4 \item {\tt ccontr} theorem, 66
1.5 \item {\tt classical} theorem, 66
1.6 \item {\tt coinduct} theorem, 44
1.7 - \item {\tt coinductive}, 91--95
1.8 + \item {\tt coinductive}, 92--95
1.9 \item {\tt Collect} constant, 25, 26, 29, 68, 70
1.10 \item {\tt Collect_def} theorem, 30
1.11 \item {\tt Collect_mem_eq} theorem, 70, 71
1.12 @@ -184,7 +184,7 @@
1.13
1.14 \indexspace
1.15
1.16 - \item {\tt datatype}, 85--91
1.17 + \item {\tt datatype}, 85--92
1.18 \item {\tt deepen_tac}, 16
1.19 \item {\tt diff_0_eq_0} theorem, 123
1.20 \item {\tt Diff_cancel} theorem, 41
1.21 @@ -272,6 +272,7 @@
1.22 \item {\tt exCI} theorem, 11, 15, 66
1.23 \item {\tt excluded_middle} theorem, 11, 66
1.24 \item {\tt exE} theorem, 8, 66
1.25 + \item {\tt exhaust_tac}, \bold{88}
1.26 \item {\tt exI} theorem, 8, 66
1.27 \item {\tt exL} theorem, 102
1.28 \item {\tt Exp} theory, 96
1.29 @@ -402,7 +403,7 @@
1.30 \item {\tt ind} type, 79
1.31 \item {\tt induct} theorem, 44
1.32 \item {\tt induct_tac}, 80, \bold{86}
1.33 - \item {\tt inductive}, 91--95
1.34 + \item {\tt inductive}, 92--95
1.35 \item {\tt Inf} constant, 25, 29
1.36 \item {\tt infinity} theorem, 31
1.37 \item {\tt inj} constant, 45, 75
1.38 @@ -507,7 +508,7 @@
1.39 \item {\tt lfp_Tarski} theorem, 44
1.40 \item {\tt List} theory, 80, 81
1.41 \item {\tt list} constant, 49
1.42 - \item {\tt list} type, 80, 95
1.43 + \item {\tt list} type, 80, 96
1.44 \item {\tt List.induct} theorem, 49
1.45 \item {\tt list_case} constant, 49
1.46 \item {\tt list_mono} theorem, 49
1.47 @@ -643,8 +644,8 @@
1.48 \item {\tt Pow_mono} theorem, 52
1.49 \item {\tt PowD} theorem, 33, 53, 73
1.50 \item {\tt PowI} theorem, 33, 53, 73
1.51 - \item primitive recursion, 90--91
1.52 - \item {\tt primrec}, 90--91
1.53 + \item primitive recursion, 90--92
1.54 + \item {\tt primrec}, 90--92
1.55 \item {\tt primrec} symbol, 79
1.56 \item {\tt PrimReplace} constant, 25, 29
1.57 \item priorities, 2