diff -r 10e033194e9d -r adafef6eb295 src/ZF/ex/Integ.ML
--- a/src/ZF/ex/Integ.ML	Tue Jul 21 08:54:09 1998 +0200
+++ b/src/ZF/ex/Integ.ML	Tue Jul 21 12:12:52 1998 +0200
@@ -140,7 +140,7 @@
 
 Goalw [znegative_def, znat_def] "n: nat ==> znegative($~ $# succ(n))";
 by (asm_simp_tac (simpset() addsimps [zminus]) 1);
-by(blast_tac (claset() addIs [nat_0_le]) 1);
+by (blast_tac (claset() addIs [nat_0_le]) 1);
 qed "znegative_zminus_znat";