src/HOL/Import/HOL4Compat.thy
changeset 20432 07ec57376051
parent 20269 c40070317ab8
child 23389 aaca6a8e5414
     1.1 --- a/src/HOL/Import/HOL4Compat.thy	Tue Aug 29 21:43:34 2006 +0200
     1.2 +++ b/src/HOL/Import/HOL4Compat.thy	Wed Aug 30 03:19:08 2006 +0200
     1.3 @@ -221,7 +221,7 @@
     1.4    by simp
     1.5  
     1.6  lemma SUB: "(!m. (0::nat) - m = 0) & (!m n. (Suc m) - n = (if m < n then 0 else Suc (m - n)))"
     1.7 -  by simp
     1.8 +  by (simp, arith)
     1.9  
    1.10  lemma MAX_DEF: "max (m::nat) n = (if m < n then n else m)"
    1.11    by (simp add: max_def)