--- 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();