# HG changeset patch
# User wenzelm
# Date 1008891875 -3600
# Node ID c76c4b88ca6aeb8f6e3710e4043e0f85a687207a
# Parent  56eb790f3a03ec7abac37684b28578cc6bcd58b1
updated;

diff -r 56eb790f3a03 -r c76c4b88ca6a doc-src/TutorialI/tutorial.ind
--- a/doc-src/TutorialI/tutorial.ind	Fri Dec 21 00:43:58 2001 +0100
+++ b/doc-src/TutorialI/tutorial.ind	Fri Dec 21 00:44:35 2001 +0100
@@ -70,9 +70,9 @@
     \subitem renaming, 72--73
     \subitem reusing, 73
   \item \isa {auto} (method), 38, 82
-  \item \isa {axclass}, 153--159
+  \item \isa {axclass}, 154--160
   \item axiom of choice, 76
-  \item axiomatic type classes, 153--159
+  \item axiomatic type classes, 154--160
 
   \indexspace
 
@@ -105,7 +105,7 @@
   \item case distinctions, 19
   \item case splits, \bold{31}
   \item \isa {case_tac} (method), 19, 91, 147
-  \item \isa {cases} (method), 151
+  \item \isa {cases} (method), 152
   \item \isa {clarify} (method), 81, 82
   \item \isa {clarsimp} (method), 81, 82
   \item \isa {classical} (theorem), \bold{63}
@@ -196,6 +196,7 @@
   \item \isa {exE} (theorem), \bold{72}
   \item \isa {exI} (theorem), \bold{72}
   \item \isa {ext} (theorem), \bold{99}
+  \item \isa {extend} (constant), 153
   \item extensionality
     \subitem for functions, \bold{99, 100}
     \subitem for records, 151
@@ -207,6 +208,7 @@
   \item \isa {False} (constant), 5
   \item \isa {fast} (method), 82, 114
   \item Fibonacci function, 47
+  \item \isa {fields} (constant), 153
   \item \isa {finite} (symbol), 99
   \item \isa {Finites} (constant), 99
   \item fixed points, 106
@@ -286,7 +288,7 @@
   \item injections, 100
   \item \isa {insert} (constant), 97
   \item \isa {insert} (method), 87--88
-  \item instance, \bold{154}
+  \item instance, \bold{155}
   \item \texttt {INT}, \bold{199}
   \item \texttt {Int}, \bold{199}
   \item \isa {int} (type), 143--144
@@ -302,7 +304,7 @@
   \item \isa {IntI} (theorem), \bold{95}
   \item \isa {intro} (method), 64
   \item \isa {intro!} (attribute), 118
-  \item \isa {intro_classes} (method), 154
+  \item \isa {intro_classes} (method), 155
   \item introduction rules, 58--59
   \item \isa {inv} (constant), 76
   \item \isa {inv_image_def} (theorem), \bold{105}
@@ -348,6 +350,7 @@
 
   \item \isa {Main} (theory), 4
   \item major premise, \bold{65}
+  \item \isa {make} (constant), 153
   \item \isa {max} (constant), 23, 24
   \item measure functions, 47, 104
   \item \isa {measure_def} (theorem), \bold{105}
@@ -365,7 +368,7 @@
   \item \isa {more} (constant), 148--150
   \item \isa {mp} (theorem), \bold{62}
   \item \isa {mult_ac} (theorems), 142
-  \item multiple inheritance, \bold{158}
+  \item multiple inheritance, \bold{159}
   \item multiset ordering, \bold{105}
 
   \indexspace
@@ -400,7 +403,7 @@
   \item \isacommand {oops} (command), 13
   \item \isa {option} (type), \bold{24}
   \item ordered rewriting, \bold{166}
-  \item overloading, 23, 153--156
+  \item overloading, 23, 154--157
     \subitem and arithmetic, 140
 
   \indexspace
@@ -451,9 +454,9 @@
   \item \isa {recdef_cong} (attribute), 172
   \item \isa {recdef_simp} (attribute), 49
   \item \isa {recdef_wf} (attribute), 170
-  \item \isacommand {record} (command), 148
-  \item records, 148--153
-    \subitem extensible, 149--150
+  \item \isacommand {record} (command), 149
+  \item records, 148--154
+    \subitem extensible, 150
   \item recursion
     \subitem guarded, 173
     \subitem primitive, 18
@@ -525,7 +528,7 @@
   \item \isa {split_if_asm} (theorem), 32
   \item \isa {ssubst} (theorem), \bold{67}
   \item structural induction, \see{induction, structural}{1}
-  \item subclasses, 153, 157
+  \item subclasses, 154, 158
   \item subgoal numbering, 46
   \item \isa {subgoal_tac} (method), 88
   \item subgoals, 12
@@ -567,6 +570,7 @@
   \item \isacommand {translations} (command), 26
   \item tries, 44--46
   \item \isa {True} (constant), 5
+  \item \isa {truncate} (constant), 153
   \item tuples, \see{pairs and tuples}{1}
   \item \isacommand {typ} (command), 16
   \item type constraints, \bold{6}
@@ -574,11 +578,11 @@
   \item type inference, \bold{5}
   \item type synonyms, 25
   \item type variables, 5
-  \item \isacommand {typedecl} (command), 107, 159
-  \item \isacommand {typedef} (command), 160--163
+  \item \isacommand {typedecl} (command), 107, 161
+  \item \isacommand {typedef} (command), 161--164
   \item types, 4--5
-    \subitem declaring, 159--160
-    \subitem defining, 160--163
+    \subitem declaring, 161
+    \subitem defining, 161--164
   \item \isacommand {types} (command), 25
 
   \indexspace