diff -r 968d2dccf2de -r 4448d76f87ef ex/Simult.ML
--- a/ex/Simult.ML	Thu Oct 07 10:20:30 1993 +0100
+++ b/ex/Simult.ML	Thu Oct 07 10:29:23 1993 +0100
@@ -191,7 +191,7 @@
 
 (** Distinctness of TCONS, FNIL and FCONS **)
 
-goalw Simult.thy TF_Rep_defs "~ TCONS(M,N) = FNIL";
+goalw Simult.thy TF_Rep_defs "TCONS(M,N) ~= FNIL";
 by (fast_tac TF_Rep_cs 1);
 val TCONS_not_FNIL = result();
 val FNIL_not_TCONS = standard (TCONS_not_FNIL RS not_sym);
@@ -199,7 +199,7 @@
 val TCONS_neq_FNIL = standard (TCONS_not_FNIL RS notE);
 val FNIL_neq_TCONS = sym RS TCONS_neq_FNIL;
 
-goalw Simult.thy TF_Rep_defs "~ FCONS(M,N) = FNIL";
+goalw Simult.thy TF_Rep_defs "FCONS(M,N) ~= FNIL";
 by (fast_tac TF_Rep_cs 1);
 val FCONS_not_FNIL = result();
 val FNIL_not_FCONS = standard (FCONS_not_FNIL RS not_sym);
@@ -207,7 +207,7 @@
 val FCONS_neq_FNIL = standard (FCONS_not_FNIL RS notE);
 val FNIL_neq_FCONS = sym RS FCONS_neq_FNIL;
 
-goalw Simult.thy TF_Rep_defs "~ TCONS(M,N) = FCONS(K,L)";
+goalw Simult.thy TF_Rep_defs "TCONS(M,N) ~= FCONS(K,L)";
 by (fast_tac TF_Rep_cs 1);
 val TCONS_not_FCONS = result();
 val FCONS_not_TCONS = standard (TCONS_not_FCONS RS not_sym);
@@ -236,7 +236,7 @@
 val Tcons_Tcons_eq = result();
 val Tcons_inject = standard (Tcons_Tcons_eq RS iffD1 RS conjE);
 
-goalw Simult.thy [Fcons_def,Fnil_def] "~ Fcons(x,xs) = Fnil";
+goalw Simult.thy [Fcons_def,Fnil_def] "Fcons(x,xs) ~= Fnil";
 by (fast_tac TF_cs 1);
 val Fcons_not_Fnil = result();