1.1 --- a/doc-src/TutorialI/tutorial.ind	Fri Dec 21 00:43:58 2001 +0100
     1.2 +++ b/doc-src/TutorialI/tutorial.ind	Fri Dec 21 00:44:35 2001 +0100
     1.3 @@ -70,9 +70,9 @@
     1.4      \subitem renaming, 72--73
     1.5      \subitem reusing, 73
     1.6    \item \isa {auto} (method), 38, 82
     1.7 -  \item \isa {axclass}, 153--159
     1.8 +  \item \isa {axclass}, 154--160
     1.9    \item axiom of choice, 76
    1.10 -  \item axiomatic type classes, 153--159
    1.11 +  \item axiomatic type classes, 154--160
    1.12  
    1.13    \indexspace
    1.14  
    1.15 @@ -105,7 +105,7 @@
    1.16    \item case distinctions, 19
    1.17    \item case splits, \bold{31}
    1.18    \item \isa {case_tac} (method), 19, 91, 147
    1.19 -  \item \isa {cases} (method), 151
    1.20 +  \item \isa {cases} (method), 152
    1.21    \item \isa {clarify} (method), 81, 82
    1.22    \item \isa {clarsimp} (method), 81, 82
    1.23    \item \isa {classical} (theorem), \bold{63}
    1.24 @@ -196,6 +196,7 @@
    1.25    \item \isa {exE} (theorem), \bold{72}
    1.26    \item \isa {exI} (theorem), \bold{72}
    1.27    \item \isa {ext} (theorem), \bold{99}
    1.28 +  \item \isa {extend} (constant), 153
    1.29    \item extensionality
    1.30      \subitem for functions, \bold{99, 100}
    1.31      \subitem for records, 151
    1.32 @@ -207,6 +208,7 @@
    1.33    \item \isa {False} (constant), 5
    1.34    \item \isa {fast} (method), 82, 114
    1.35    \item Fibonacci function, 47
    1.36 +  \item \isa {fields} (constant), 153
    1.37    \item \isa {finite} (symbol), 99
    1.38    \item \isa {Finites} (constant), 99
    1.39    \item fixed points, 106
    1.40 @@ -286,7 +288,7 @@
    1.41    \item injections, 100
    1.42    \item \isa {insert} (constant), 97
    1.43    \item \isa {insert} (method), 87--88
    1.44 -  \item instance, \bold{154}
    1.45 +  \item instance, \bold{155}
    1.46    \item \texttt {INT}, \bold{199}
    1.47    \item \texttt {Int}, \bold{199}
    1.48    \item \isa {int} (type), 143--144
    1.49 @@ -302,7 +304,7 @@
    1.50    \item \isa {IntI} (theorem), \bold{95}
    1.51    \item \isa {intro} (method), 64
    1.52    \item \isa {intro!} (attribute), 118
    1.53 -  \item \isa {intro_classes} (method), 154
    1.54 +  \item \isa {intro_classes} (method), 155
    1.55    \item introduction rules, 58--59
    1.56    \item \isa {inv} (constant), 76
    1.57    \item \isa {inv_image_def} (theorem), \bold{105}
    1.58 @@ -348,6 +350,7 @@
    1.59  
    1.60    \item \isa {Main} (theory), 4
    1.61    \item major premise, \bold{65}
    1.62 +  \item \isa {make} (constant), 153
    1.63    \item \isa {max} (constant), 23, 24
    1.64    \item measure functions, 47, 104
    1.65    \item \isa {measure_def} (theorem), \bold{105}
    1.66 @@ -365,7 +368,7 @@
    1.67    \item \isa {more} (constant), 148--150
    1.68    \item \isa {mp} (theorem), \bold{62}
    1.69    \item \isa {mult_ac} (theorems), 142
    1.70 -  \item multiple inheritance, \bold{158}
    1.71 +  \item multiple inheritance, \bold{159}
    1.72    \item multiset ordering, \bold{105}
    1.73  
    1.74    \indexspace
    1.75 @@ -400,7 +403,7 @@
    1.76    \item \isacommand {oops} (command), 13
    1.77    \item \isa {option} (type), \bold{24}
    1.78    \item ordered rewriting, \bold{166}
    1.79 -  \item overloading, 23, 153--156
    1.80 +  \item overloading, 23, 154--157
    1.81      \subitem and arithmetic, 140
    1.82  
    1.83    \indexspace
    1.84 @@ -451,9 +454,9 @@
    1.85    \item \isa {recdef_cong} (attribute), 172
    1.86    \item \isa {recdef_simp} (attribute), 49
    1.87    \item \isa {recdef_wf} (attribute), 170
    1.88 -  \item \isacommand {record} (command), 148
    1.89 -  \item records, 148--153
    1.90 -    \subitem extensible, 149--150
    1.91 +  \item \isacommand {record} (command), 149
    1.92 +  \item records, 148--154
    1.93 +    \subitem extensible, 150
    1.94    \item recursion
    1.95      \subitem guarded, 173
    1.96      \subitem primitive, 18
    1.97 @@ -525,7 +528,7 @@
    1.98    \item \isa {split_if_asm} (theorem), 32
    1.99    \item \isa {ssubst} (theorem), \bold{67}
   1.100    \item structural induction, \see{induction, structural}{1}
   1.101 -  \item subclasses, 153, 157
   1.102 +  \item subclasses, 154, 158
   1.103    \item subgoal numbering, 46
   1.104    \item \isa {subgoal_tac} (method), 88
   1.105    \item subgoals, 12
   1.106 @@ -567,6 +570,7 @@
   1.107    \item \isacommand {translations} (command), 26
   1.108    \item tries, 44--46
   1.109    \item \isa {True} (constant), 5
   1.110 +  \item \isa {truncate} (constant), 153
   1.111    \item tuples, \see{pairs and tuples}{1}
   1.112    \item \isacommand {typ} (command), 16
   1.113    \item type constraints, \bold{6}
   1.114 @@ -574,11 +578,11 @@
   1.115    \item type inference, \bold{5}
   1.116    \item type synonyms, 25
   1.117    \item type variables, 5
   1.118 -  \item \isacommand {typedecl} (command), 107, 159
   1.119 -  \item \isacommand {typedef} (command), 160--163
   1.120 +  \item \isacommand {typedecl} (command), 107, 161
   1.121 +  \item \isacommand {typedef} (command), 161--164
   1.122    \item types, 4--5
   1.123 -    \subitem declaring, 159--160
   1.124 -    \subitem defining, 160--163
   1.125 +    \subitem declaring, 161
   1.126 +    \subitem defining, 161--164
   1.127    \item \isacommand {types} (command), 25
   1.128  
   1.129    \indexspace