diff -r d199410f1db1 -r 968d2dccf2de nat.ML
--- a/nat.ML	Mon Oct 04 15:43:54 1993 +0100
+++ b/nat.ML	Thu Oct 07 10:20:30 1993 +0100
@@ -90,7 +90,7 @@
 
 (*** Distinctness of constructors ***)
 
-goalw Nat.thy [Zero_def,Suc_def] "~ Suc(m)=0";
+goalw Nat.thy [Zero_def,Suc_def] "Suc(m) ~= 0";
 by (rtac (inj_onto_Abs_Nat RS inj_onto_contraD) 1);
 by (rtac Suc_Rep_not_Zero_Rep 1);
 by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI, Zero_RepI] 1));
@@ -117,7 +117,7 @@
 by (EVERY1 [rtac iffI, etac Suc_inject, etac arg_cong]); 
 val Suc_Suc_eq = result();
 
-goal Nat.thy "~ n=Suc(n)";
+goal Nat.thy "n ~= Suc(n)";
 by (nat_ind_tac "n" 1);
 by (ALLGOALS(asm_simp_tac (HOL_ss addsimps [Zero_not_Suc,Suc_Suc_eq])));
 val n_not_Suc_n = result();