doc-src/TutorialI/tutorial.ind

   \item \isa {?} (tactical), 89
   \item \texttt{|} (tactical), 89
 
   \indexspace
 
-  \item \isa {0} (constant), 22, 23, 141
-  \item \isa {1} (symbol), 141
-  \item \isa {2} (symbol), 141
+  \item \isa {0} (constant), 22, 23, 140
+  \item \isa {1} (constant), 140, 141
 
   \indexspace
 
   \item abandoning a proof, \bold{13}
   \item abandoning a theory, \bold{16}

   \item \isa {insert} (constant), 97
   \item \isa {insert} (method), 87--88
   \item instance, \bold{153}
   \item \texttt {INT}, \bold{195}
   \item \texttt {Int}, \bold{195}
-  \item \isa {int} (type), 143
+  \item \isa {int} (type), 143--144
   \item \isa {INT_iff} (theorem), \bold{98}
   \item \isa {IntD1} (theorem), \bold{95}
   \item \isa {IntD2} (theorem), \bold{95}
-  \item integers, 143
+  \item integers, 143--144
   \item \isa {INTER} (constant), 99
   \item \texttt {Inter}, \bold{195}
   \item \isa {Inter_iff} (theorem), \bold{98}
   \item intersection, 95
     \subitem indexed, 98

   \item model checking example, 106--116
   \item \emph{modus ponens}, 57, 62
   \item \isa {mono_def} (theorem), \bold{106}
   \item monotone functions, \bold{106}, 129
     \subitem and inductive definitions, 127--128
-  \item \isa {more} (constant), 148, 149
+  \item \isa {more} (constant), 148--150
   \item \isa {mp} (theorem), \bold{62}
   \item \isa {mult_ac} (theorems), 142
   \item multiple inheritance, \bold{157}
   \item multiset ordering, \bold{105}
 
   \indexspace
 
-  \item \isa {nat} (type), 4, 22, 141--142
+  \item \isa {nat} (type), 4, 22, 141--143
   \item \isa {nat_less_induct} (theorem), 176
   \item natural deduction, 57--58
-  \item natural numbers, 22, 141--142
+  \item natural numbers, 22, 141--143
   \item Needham-Schroeder protocol, 183--185
   \item negation, 63--65
   \item \isa {Nil} (constant), 9
   \item \isa {no_asm} (modifier), 29
   \item \isa {no_asm_simp} (modifier), 29

   \item \isa {notE} (theorem), \bold{63}
   \item \isa {notI} (theorem), \bold{63}
   \item numbers, 139--145
   \item numeric literals, 140
     \subitem for type \protect\isa{nat}, 141
-    \subitem for type \protect\isa{real}, 144
+    \subitem for type \protect\isa{real}, 145
 
   \indexspace
 
   \item \isa {O} (symbol), 102
   \item \texttt {o}, \bold{195}

   \item \isa {of} (attribute), 83, 86
   \item \isa {only} (modifier), 29
   \item \isacommand {oops} (command), 13
   \item \isa {option} (type), \bold{24}
   \item ordered rewriting, \bold{164}
-  \item overloading, 23, 152--154
+  \item overloading, 23, 152--155
     \subitem and arithmetic, 140
 
   \indexspace
 
   \item pairs and tuples, 24, 145--148

     \subitem and numeric literals, 140
   \item \isa {recdef_cong} (attribute), 170
   \item \isa {recdef_simp} (attribute), 48
   \item \isa {recdef_wf} (attribute), 168
   \item \isacommand {record} (command), 148
-  \item \isa {record_split} (method), 151
+  \item \isa {record_split} (method), 152
   \item records, 148--152
-    \subitem extensible, 149--150
+    \subitem extensible, 149--151
   \item recursion
     \subitem guarded, 171
     \subitem primitive, 18
     \subitem well-founded, \bold{167}
   \item recursion induction, 51--52

   \item \isa {Some} (constant), \bold{24}
   \item \isa {some_equality} (theorem), \bold{76}
   \item \isa {someI} (theorem), \bold{76}
   \item \isa {someI2} (theorem), \bold{76}
   \item \isa {someI_ex} (theorem), \bold{77}
-  \item sorts, 157
+  \item sorts, 158
   \item \isa {spec} (theorem), \bold{70}
   \item \isa {split} (attribute), 32
-  \item \isa {split} (constant), 145
+  \item \isa {split} (constant), 146
   \item \isa {split} (method), 31, 146
   \item \isa {split} (modifier), 32
   \item split rule, \bold{32}
   \item \isa {split_if} (theorem), 32
   \item \isa {split_if_asm} (theorem), 32