src/HOL/NatArith.thy

--- a/src/HOL/NatArith.thy	Fri Sep 26 10:34:28 2003 +0200
+++ b/src/HOL/NatArith.thy	Fri Sep 26 10:34:57 2003 +0200
@@ -13,10 +13,8 @@
 
 
 lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m <= n)"
-apply (simp add: less_eq reflcl_trancl [symmetric]
-            del: reflcl_trancl)
-apply arith
-done
+by (simp add: less_eq reflcl_trancl [symmetric]
+            del: reflcl_trancl, arith)
 
 lemma nat_diff_split:
     "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"