--- a/src/HOL/Integ/IntDef.ML Mon Jan 11 12:52:53 1999 +0100
+++ b/src/HOL/Integ/IntDef.ML Mon Jan 11 16:50:49 1999 +0100
@@ -149,7 +149,6 @@
Goalw [neg_def, int_def] "~ neg(int n)";
by (Simp_tac 1);
-by Safe_tac;
qed "not_neg_nat";
Goalw [neg_def, int_def] "neg(- (int (Suc n)))";