doc-src/TutorialI/tutorial.ind

   \item binary trees, 18
   \item binomial coefficients, 99
   \item bisimulations, 106
   \item \isa {blast} (method), 79--80, 82
   \item \isa {bool} (type), 4, 5
-  \item boolean expressions example, 20--22
+  \item boolean expressions example, 19--22
   \item \isa {bspec} (theorem), \bold{98}
   \item \isacommand{by} (command), 63
 
   \indexspace
 

   \item LCF, 43
   \item \isa {LEAST} (symbol), 23, 75
   \item least number operator, \see{\protect\isa{LEAST}}{75}
   \item \isacommand {lemma} (command), 13
   \item \isacommand {lemmas} (command), 83, 92
-  \item \isa {length} (symbol), 18
+  \item \isa {length} (symbol), 17
   \item \isa {length_induct}, \bold{178}
   \item \isa {less_than} (constant), 104
   \item \isa {less_than_iff} (theorem), \bold{104}
   \item \isa {let} expressions, 5, 6, 31
   \item \isa {Let_def} (theorem), 31
   \item \isa {lex_prod_def} (theorem), \bold{105}
   \item lexicographic product, \bold{105}, 166
   \item {\texttt{lfp}}
     \subitem applications of, \see{CTL}{106}
-  \item linear arithmetic, 22--24, 139
+  \item linear arithmetic, 22--23, 139
   \item \isa {List} (theory), 17
   \item \isa {list} (type), 4, 9, 17
   \item \isa {list.split} (theorem), 32
   \item \isa {lists_mono} (theorem), \bold{127}
   \item Lowe, Gavin, 184--185
 
   \indexspace
 
   \item \isa {Main} (theory), 4
   \item major premise, \bold{65}
-  \item \isa {max} (constant), 23, 24
+  \item \isa {max} (constant), 23
   \item measure functions, 47, 104
   \item \isa {measure_def} (theorem), \bold{105}
   \item meta-logic, \bold{70}
-  \item methods, \bold{16}
-  \item \isa {min} (constant), 23, 24
+  \item methods, \bold{15}
+  \item \isa {min} (constant), 23
   \item \isa {mod} (symbol), 23
   \item \isa {mod_div_equality} (theorem), \bold{141}
   \item \isa {mod_mult_distrib} (theorem), \bold{141}
   \item model checking example, 106--116
   \item \emph{modus ponens}, 57, 62

   \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, 158
+  \item sorts, 157
   \item \isa {spec} (theorem), \bold{70}
   \item \isa {split} (attribute), 32
   \item \isa {split} (constant), 145
   \item \isa {split} (method), 31, 146
   \item \isa {split} (modifier), 32

     \subitem abandoning, \bold{16}
   \item \isacommand {theory} (command), 16
   \item theory files, 4
   \item \isacommand {thm} (command), 16
   \item \isa {tl} (constant), 17
-  \item \isa {ToyList} example, 9--15
+  \item \isa {ToyList} example, 9--14
   \item \isa {trace_simp} (flag), 33
   \item tracing the simplifier, \bold{33}
   \item \isa {trancl_trans} (theorem), \bold{103}
   \item transition systems, 107
   \item \isacommand {translations} (command), 26