doc-src/TutorialI/Misc/natsum.thy
changeset 10971 6852682eaf16
parent 10788 ea48dd8b0232
child 10978 5eebea8f359f
     1.1 --- a/doc-src/TutorialI/Misc/natsum.thy	Wed Jan 24 11:59:15 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Misc/natsum.thy	Wed Jan 24 12:29:10 2001 +0100
     1.3 @@ -69,7 +69,8 @@
     1.4  For more complex goals, there is the special method \isaindexbold{arith}
     1.5  (which attacks the first subgoal). It proves arithmetic goals involving the
     1.6  usual logical connectives (@{text"\<not>"}, @{text"\<and>"}, @{text"\<or>"},
     1.7 -@{text"\<longrightarrow>"}), the relations @{text"\<le>"} and @{text"<"}, and the operations
     1.8 +@{text"\<longrightarrow>"}), the relations @{text"="}, @{text"\<le>"} and @{text"<"},
     1.9 +and the operations
    1.10  @{text"+"}, @{text"-"}, @{term min} and @{term max}. Technically, this is
    1.11  known as the class of (quantifier free) \bfindex{linear arithmetic} formulae.
    1.12  For example,