equal
deleted
inserted
replaced
30 \ttindexboldpos{<}{$HOL2arithrel}. There is even a least number operation |
30 \ttindexboldpos{<}{$HOL2arithrel}. There is even a least number operation |
31 \isaindexbold{LEAST}. For example, @{prop"(LEAST n. 1 < n) = 2"}, although |
31 \isaindexbold{LEAST}. For example, @{prop"(LEAST n. 1 < n) = 2"}, although |
32 Isabelle does not prove this completely automatically. Note that @{term 1} |
32 Isabelle does not prove this completely automatically. Note that @{term 1} |
33 and @{term 2} are available as abbreviations for the corresponding |
33 and @{term 2} are available as abbreviations for the corresponding |
34 @{term Suc}-expressions. If you need the full set of numerals, |
34 @{term Suc}-expressions. If you need the full set of numerals, |
35 see~\S\ref{nat-numerals}. |
35 see~\S\ref{sec:numerals}. |
36 |
36 |
37 \begin{warn} |
37 \begin{warn} |
38 The constant \ttindexbold{0} and the operations |
38 The constant \ttindexbold{0} and the operations |
39 \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun}, |
39 \ttindexboldpos{+}{$HOL2arithfun}, \ttindexboldpos{-}{$HOL2arithfun}, |
40 \ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min}, |
40 \ttindexboldpos{\mystar}{$HOL2arithfun}, \isaindexbold{min}, |