src/ZF/Nat.ML

--- a/src/ZF/Nat.ML	Wed Jul 15 12:02:19 1998 +0200
+++ b/src/ZF/Nat.ML	Wed Jul 15 14:13:18 1998 +0200
@@ -168,8 +168,7 @@
 
 (** Induction principle analogous to trancl_induct **)
 
-Goal
- "!!m. m: nat ==> P(m,succ(m)) --> (ALL x: nat. P(m,x) --> P(m,succ(x))) --> \
+Goal "m: nat ==> P(m,succ(m)) --> (ALL x: nat. P(m,x) --> P(m,succ(x))) --> \
 \                 (ALL n:nat. m<n --> P(m,n))";
 by (etac nat_induct 1);
 by (ALLGOALS    (*blast_tac gives PROOF FAILED*)