# HG changeset patch
# User lcp
# Date 749990870 -3600
# Node ID 4433428596f966e02322ec1ef5be800e852bc9e6
# Parent  cebe01deba80257c5a2614ea494387a93bb76b35
used ~: for "not in"

diff -r cebe01deba80 -r 4433428596f9 src/ZF/ex/Enum.ML
--- a/src/ZF/ex/Enum.ML	Thu Oct 07 10:48:16 1993 +0100
+++ b/src/ZF/ex/Enum.ML	Thu Oct 07 11:47:50 1993 +0100
@@ -27,7 +27,7 @@
   val type_intrs = data_typechecks
   val type_elims = []);
 
-goal Enum.thy "~ con59=con60";
+goal Enum.thy "con59 ~= con60";
 by (simp_tac (ZF_ss addsimps Enum.free_iffs) 1);  (*2.3 secs*)
 result();
 
diff -r cebe01deba80 -r 4433428596f9 src/ZF/ex/Ramsey.ML
--- a/src/ZF/ex/Ramsey.ML	Thu Oct 07 10:48:16 1993 +0100
+++ b/src/ZF/ex/Ramsey.ML	Thu Oct 07 11:47:50 1993 +0100
@@ -65,7 +65,7 @@
 val Atleast_superset = result();
 
 val prems = goalw Ramsey.thy [Atleast_def,succ_def]
-    "[| Atleast(m,B);  ~ b: B |] ==> Atleast(succ(m), cons(b,B))";
+    "[| Atleast(m,B);  b~: B |] ==> Atleast(succ(m), cons(b,B))";
 by (cut_facts_tac prems 1);
 by (etac exE 1);
 by (rtac exI 1);
@@ -153,7 +153,7 @@
 
 (*For the Atleast part, proves ~(a:I) from the second premise!*)
 val prems = goalw Ramsey.thy [Symmetric_def,Indept_def]
-    "[| Symmetric(E);  Indept(I, {z: V-{a}. ~ <a,z>:E}, E);  a: V;  \
+    "[| Symmetric(E);  Indept(I, {z: V-{a}. <a,z> ~: E}, E);  a: V;  \
 \       Atleast(j,I) |] ==>   \
 \    Indept(cons(a,I), V, E) & Atleast(succ(j), cons(a,I))";
 by (cut_facts_tac prems 1);
diff -r cebe01deba80 -r 4433428596f9 src/ZF/ex/Ramsey.thy
--- a/src/ZF/ex/Ramsey.thy	Thu Oct 07 10:48:16 1993 +0100
+++ b/src/ZF/ex/Ramsey.thy	Thu Oct 07 11:47:50 1993 +0100
@@ -30,10 +30,10 @@
     "Symmetric(E) == (ALL x y. <x,y>:E --> <y,x>:E)"
 
   Clique_def
-    "Clique(C,V,E) == (C<=V) & (ALL x:C. ALL y:C. ~ x=y --> <x,y>:E)"
+    "Clique(C,V,E) == (C<=V) & (ALL x:C. ALL y:C. x~=y --> <x,y> : E)"
 
   Indept_def
-    "Indept(I,V,E) == (I<=V) & (ALL x:I. ALL y:I. ~ x=y --> ~ <x,y>:E)"
+    "Indept(I,V,E) == (I<=V) & (ALL x:I. ALL y:I. x~=y --> <x,y> ~: E)"
 
   Atleast_def
     "Atleast(n,S) == (EX f. f: inj(n,S))"
diff -r cebe01deba80 -r 4433428596f9 src/ZF/ex/enum.ML
--- a/src/ZF/ex/enum.ML	Thu Oct 07 10:48:16 1993 +0100
+++ b/src/ZF/ex/enum.ML	Thu Oct 07 11:47:50 1993 +0100
@@ -27,7 +27,7 @@
   val type_intrs = data_typechecks
   val type_elims = []);
 
-goal Enum.thy "~ con59=con60";
+goal Enum.thy "con59 ~= con60";
 by (simp_tac (ZF_ss addsimps Enum.free_iffs) 1);  (*2.3 secs*)
 result();
 
diff -r cebe01deba80 -r 4433428596f9 src/ZF/ex/misc.ML
--- a/src/ZF/ex/misc.ML	Thu Oct 07 10:48:16 1993 +0100
+++ b/src/ZF/ex/misc.ML	Thu Oct 07 11:47:50 1993 +0100
@@ -26,18 +26,18 @@
   addSEs [CollectE, equalityCE];
 
 (*The search is undirected and similar proof attempts fail*)
-goal ZF.thy "ALL f: A->Pow(A). EX S: Pow(A). ALL x:A. ~ f`x = S";
+goal ZF.thy "ALL f: A->Pow(A). EX S: Pow(A). ALL x:A. f`x ~= S";
 by (best_tac cantor_cs 1);
 result();
 
-(*This form displays the diagonal term, {x: A . ~ x: f`x} *)
+(*This form displays the diagonal term, {x: A . x ~: f`x} *)
 val [prem] = goal ZF.thy
-    "f: A->Pow(A) ==> (ALL x:A. ~ f`x = ?S) & ?S: Pow(A)";
+    "f: A->Pow(A) ==> (ALL x:A. f`x ~= ?S) & ?S: Pow(A)";
 by (best_tac cantor_cs 1);
 result();
 
 (*yet another version...*)
-goalw Perm.thy [surj_def] "~ f : surj(A,Pow(A))";
+goalw Perm.thy [surj_def] "f ~: surj(A,Pow(A))";
 by (safe_tac ZF_cs);
 by (etac ballE 1);
 by (best_tac (cantor_cs addSEs [bexE]) 1);
diff -r cebe01deba80 -r 4433428596f9 src/ZF/ex/ramsey.ML
--- a/src/ZF/ex/ramsey.ML	Thu Oct 07 10:48:16 1993 +0100
+++ b/src/ZF/ex/ramsey.ML	Thu Oct 07 11:47:50 1993 +0100
@@ -65,7 +65,7 @@
 val Atleast_superset = result();
 
 val prems = goalw Ramsey.thy [Atleast_def,succ_def]
-    "[| Atleast(m,B);  ~ b: B |] ==> Atleast(succ(m), cons(b,B))";
+    "[| Atleast(m,B);  b~: B |] ==> Atleast(succ(m), cons(b,B))";
 by (cut_facts_tac prems 1);
 by (etac exE 1);
 by (rtac exI 1);
@@ -153,7 +153,7 @@
 
 (*For the Atleast part, proves ~(a:I) from the second premise!*)
 val prems = goalw Ramsey.thy [Symmetric_def,Indept_def]
-    "[| Symmetric(E);  Indept(I, {z: V-{a}. ~ <a,z>:E}, E);  a: V;  \
+    "[| Symmetric(E);  Indept(I, {z: V-{a}. <a,z> ~: E}, E);  a: V;  \
 \       Atleast(j,I) |] ==>   \
 \    Indept(cons(a,I), V, E) & Atleast(succ(j), cons(a,I))";
 by (cut_facts_tac prems 1);
diff -r cebe01deba80 -r 4433428596f9 src/ZF/ex/ramsey.thy
--- a/src/ZF/ex/ramsey.thy	Thu Oct 07 10:48:16 1993 +0100
+++ b/src/ZF/ex/ramsey.thy	Thu Oct 07 11:47:50 1993 +0100
@@ -30,10 +30,10 @@
     "Symmetric(E) == (ALL x y. <x,y>:E --> <y,x>:E)"
 
   Clique_def
-    "Clique(C,V,E) == (C<=V) & (ALL x:C. ALL y:C. ~ x=y --> <x,y>:E)"
+    "Clique(C,V,E) == (C<=V) & (ALL x:C. ALL y:C. x~=y --> <x,y> : E)"
 
   Indept_def
-    "Indept(I,V,E) == (I<=V) & (ALL x:I. ALL y:I. ~ x=y --> ~ <x,y>:E)"
+    "Indept(I,V,E) == (I<=V) & (ALL x:I. ALL y:I. x~=y --> <x,y> ~: E)"
 
   Atleast_def
     "Atleast(n,S) == (EX f. f: inj(n,S))"