src/HOL/ex/BinEx.thy
changeset 15965 f422f8283491
parent 15013 34264f5e4691
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/ex/BinEx.thy	Mon May 16 09:35:05 2005 +0200
     1.2 +++ b/src/HOL/ex/BinEx.thy	Mon May 16 10:29:15 2005 +0200
     1.3 @@ -186,6 +186,10 @@
     1.4  lemma "(1234567::int) \<le> 1234567"
     1.5    by simp
     1.6  
     1.7 +text{*No integer overflow!*}
     1.8 +lemma "1234567 * (1234567::int) < 1234567*1234567*1234567"
     1.9 +  by simp
    1.10 +
    1.11  
    1.12  text {* \medskip Quotient and Remainder *}
    1.13  
    1.14 @@ -205,7 +209,7 @@
    1.15  
    1.16  text {*
    1.17    A negative dividend\footnote{The definition agrees with mathematical
    1.18 -  convention but not with the hardware of most computers}
    1.19 +  convention and with ML, but not with the hardware of most computers}
    1.20  *}
    1.21  
    1.22  lemma "(-10::int) div 3 = -4"