1.1 --- a/src/ZF/ex/Integ.ML	Tue Jul 21 08:54:09 1998 +0200
     1.2 +++ b/src/ZF/ex/Integ.ML	Tue Jul 21 12:12:52 1998 +0200
     1.3 @@ -140,7 +140,7 @@
     1.4  
     1.5  Goalw [znegative_def, znat_def] "n: nat ==> znegative($~ $# succ(n))";
     1.6  by (asm_simp_tac (simpset() addsimps [zminus]) 1);
     1.7 -by(blast_tac (claset() addIs [nat_0_le]) 1);
     1.8 +by (blast_tac (claset() addIs [nat_0_le]) 1);
     1.9  qed "znegative_zminus_znat";
    1.10  
    1.11