src/HOL/Import/HOL4Compat.thy
changeset 20269 c40070317ab8
parent 19064 bf19cc5a7899
child 20432 07ec57376051
     1.1 --- a/src/HOL/Import/HOL4Compat.thy	Mon Jul 31 15:29:36 2006 +0200
     1.2 +++ b/src/HOL/Import/HOL4Compat.thy	Mon Jul 31 18:05:40 2006 +0200
     1.3 @@ -221,9 +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 -  apply simp
     1.8 -  apply arith
     1.9 -  done
    1.10 +  by simp
    1.11  
    1.12  lemma MAX_DEF: "max (m::nat) n = (if m < n then n else m)"
    1.13    by (simp add: max_def)