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