Removed an "apply arith" where there are already "No Subgoals"
authorkrauss
Mon Jul 31 18:05:40 2006 +0200 (2006-07-31)
changeset 20269c40070317ab8
parent 20268 1fe9aed8fcac
child 20270 3abe7dae681e
Removed an "apply arith" where there are already "No Subgoals"
src/HOL/Import/HOL4Compat.thy
     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)