# HG changeset patch
# User lcp
# Date 749986163 -3600
# Node ID 4448d76f87efcc0ea56ac96ae8a06552e27ea7c7
# Parent  968d2dccf2dec9ce6412e03011978309ec870a2a
used ~= for "not equals" and ~: for "not in"

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();
 
diff -r 968d2dccf2de -r 4448d76f87ef ex/set.ML
--- a/ex/set.ML	Thu Oct 07 10:20:30 1993 +0100
+++ b/ex/set.ML	Thu Oct 07 10:29:23 1993 +0100
@@ -17,12 +17,12 @@
 val cantor1 = result();
 
 (*This form displays the diagonal term*)
-goal Set.thy "! f:: 'a=>'a set. ! x. ~ f(x) = ?S(f)";
+goal Set.thy "! f:: 'a=>'a set. ! x. f(x) ~= ?S(f)";
 by (best_tac (set_cs addSEs [equalityCE]) 1);
 uresult();
 
 (*This form exploits the set constructs*)
-goal Set.thy "~ ?S : range(f :: 'a=>'a set)";
+goal Set.thy "?S ~: range(f :: 'a=>'a set)";
 by (rtac notI 1);
 by (etac rangeE 1);
 by (etac equalityCE 1);
@@ -43,11 +43,11 @@
 by (fast_tac (set_cs addEs [Inv_f_f RS ssubst]) 1);
 val inv_image_comp = result();
 
-val prems = goal Set.thy "~ f(a) : (f``X) ==> ~ a:X";
+val prems = goal Set.thy "f(a) ~: (f``X) ==> a~:X";
 by (cfast_tac prems 1);
 val contra_imageI = result();
 
-goal Lfp.thy "(~ a : Compl(X)) = (a:X)";
+goal Lfp.thy "(a ~: Compl(X)) = (a:X)";
 by (fast_tac set_cs 1);
 val not_Compl = result();
 
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();