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