src/ZF/Arith.thy

--- a/src/ZF/Arith.thy	Wed May 22 18:11:57 2002 +0200
+++ b/src/ZF/Arith.thy	Wed May 22 18:55:47 2002 +0200
@@ -186,9 +186,7 @@
 (** Difference **)
 
 lemma raw_diff_type: "[| m:nat;  n:nat |] ==> raw_diff (m, n) : nat"
-apply (induct_tac "n", auto)
-apply (fast intro: nat_case_type)
-done
+by (induct_tac "n", auto)
 
 lemma diff_type [iff,TC]: "m #- n : nat"
 by (simp add: diff_def raw_diff_type)