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