diff -r 93d5408eb7d9 -r fbd097aec213 doc-src/TutorialI/tutorial.ind --- a/doc-src/TutorialI/tutorial.ind Sun Oct 21 19:48:19 2001 +0200 +++ b/doc-src/TutorialI/tutorial.ind Sun Oct 21 19:49:29 2001 +0200 @@ -91,7 +91,7 @@ \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 @@ -327,7 +327,7 @@ \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} @@ -337,7 +337,7 @@ \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 @@ -348,12 +348,12 @@ \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} @@ -514,7 +514,7 @@ \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 @@ -559,7 +559,7 @@ \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}