# HG changeset patch
# User krauss
# Date 1154361940 -7200
# Node ID c40070317ab81e6a19400a04004f801edd4d0f2e
# Parent  1fe9aed8fcaca07f92dd3335673cf8647d44e5f9
Removed an "apply arith" where there are already "No Subgoals"

diff -r 1fe9aed8fcac -r c40070317ab8 src/HOL/Import/HOL4Compat.thy
--- a/src/HOL/Import/HOL4Compat.thy	Mon Jul 31 15:29:36 2006 +0200
+++ b/src/HOL/Import/HOL4Compat.thy	Mon Jul 31 18:05:40 2006 +0200
@@ -221,9 +221,7 @@
   by simp
 
 lemma SUB: "(!m. (0::nat) - m = 0) & (!m n. (Suc m) - n = (if m < n then 0 else Suc (m - n)))"
-  apply simp
-  apply arith
-  done
+  by simp
 
 lemma MAX_DEF: "max (m::nat) n = (if m < n then n else m)"
   by (simp add: max_def)