set.ML

--- a/set.ML	Mon Oct 04 15:43:54 1993 +0100
+++ b/set.ML	Thu Oct 07 10:20:30 1993 +0100
@@ -42,7 +42,7 @@
 val bspec = result();
 
 val major::prems = goalw Set.thy [Ball_def]
-    "[| ! x:A. P(x);  P(x) ==> Q;  ~ x:A ==> Q |] ==> Q";
+    "[| ! x:A. P(x);  P(x) ==> Q;  x~:A ==> Q |] ==> Q";
 by (rtac (major RS spec RS impCE) 1);
 by (REPEAT (eresolve_tac prems 1));
 val ballE = result();
@@ -109,7 +109,7 @@
 
 (*Classical elimination rule*)
 val major::prems = goalw Set.thy [subset_def] 
-    "[| A <= B;  ~(c:A) ==> P;  c:B ==> P |] ==> P";
+    "[| A <= B;  c~:A ==> P;  c:B ==> P |] ==> P";
 by (rtac (major RS ballE) 1);
 by (REPEAT (eresolve_tac prems 1));
 val subsetCE = result();
@@ -153,7 +153,7 @@
 val equalityE = result();
 
 val major::prems = goal Set.thy
-    "[| A = B;  [| c:A; c:B |] ==> P;  [| ~ c:A; ~ c:B |] ==> P |]  ==>  P";
+    "[| A = B;  [| c:A; c:B |] ==> P;  [| c~:A; c~:B |] ==> P |]  ==>  P";
 by (rtac (major RS equalityE) 1);
 by (REPEAT (contr_tac 1 ORELSE eresolve_tac ([asm_rl,subsetCE]@prems) 1));
 val equalityCE = result();
@@ -179,7 +179,7 @@
   Negated assumptions behave like formulae on the right side of the notional
   turnstile...*)
 val major::prems = goalw Set.thy [Compl_def]
-    "[| c : Compl(A) |] ==> ~c:A";
+    "[| c : Compl(A) |] ==> c~:A";
 by (rtac (major RS CollectD) 1);
 val ComplD = result();
 
@@ -197,7 +197,7 @@
 val UnI2 = result();
 
 (*Classical introduction rule: no commitment to A vs B*)
-val UnCI = prove_goal Set.thy "(~c:B ==> c:A) ==> c : A Un B"
+val UnCI = prove_goal Set.thy "(c~:B ==> c:A) ==> c : A Un B"
  (fn prems=>
   [ (rtac classical 1),
     (REPEAT (ares_tac (prems@[UnI1,notI]) 1)),
@@ -236,7 +236,7 @@
 (*** Set difference ***)
 
 val DiffI = prove_goalw Set.thy [set_diff_def]
-    "[| c : A;  ~ c : B |] ==> c : A - B"
+    "[| c : A;  c ~: B |] ==> c : A - B"
  (fn prems=> [ (REPEAT (resolve_tac (prems @ [CollectI,conjI]) 1)) ]);
 
 val DiffD1 = prove_goalw Set.thy [set_diff_def]
@@ -249,12 +249,12 @@
      [rtac (minor RS (major RS CollectD RS conjunct2 RS notE)) 1]);
 
 val DiffE = prove_goal Set.thy
-    "[| c : A - B;  [| c:A; ~ c:B |] ==> P |] ==> P"
+    "[| c : A - B;  [| c:A; c~:B |] ==> P |] ==> P"
  (fn prems=>
   [ (resolve_tac prems 1),
     (REPEAT (ares_tac (prems RL [DiffD1, DiffD2 RS notI]) 1)) ]);
 
-val Diff_iff = prove_goal Set.thy "(c : A-B) = (c:A & ~ c:B)"
+val Diff_iff = prove_goal Set.thy "(c : A-B) = (c:A & c~:B)"
  (fn _ => [ (fast_tac (HOL_cs addSIs [DiffI] addSEs [DiffE]) 1) ]);
 
 
@@ -294,7 +294,7 @@
  (fn _ => [fast_tac (HOL_cs addIs [insertI1,insertI2] addSEs [insertE]) 1]);
 
 (*Classical introduction rule*)
-val insertCI = prove_goal Set.thy "(~a:B ==> a=b) ==> a: insert(b,B)"
+val insertCI = prove_goal Set.thy "(a~:B ==> a=b) ==> a: insert(b,B)"
  (fn [prem]=>
   [ (rtac (disjCI RS (insert_iff RS iffD2)) 1),
     (etac prem 1) ]);
@@ -358,7 +358,7 @@
 
 (*"Classical" elimination -- by the Excluded Middle on a:A *)
 val major::prems = goalw Set.thy [INTER_def]
-    "[| b : (INT x:A. B(x));  b: B(a) ==> R;  ~ a:A ==> R |] ==> R";
+    "[| b : (INT x:A. B(x));  b: B(a) ==> R;  a~:A ==> R |] ==> R";
 by (rtac (major RS CollectD RS ballE) 1);
 by (REPEAT (eresolve_tac prems 1));
 val INT_E = result();
@@ -430,7 +430,7 @@
 
 (*"Classical" elimination rule -- does not require proving X:C *)
 val major::prems = goalw Set.thy [Inter_def]
-    "[| A : Inter(C);  A:X ==> R;  ~ X:C ==> R |] ==> R";
+    "[| A : Inter(C);  A:X ==> R;  X~:C ==> R |] ==> R";
 by (rtac (major RS INT_E) 1);
 by (REPEAT (eresolve_tac prems 1));
 val InterE = result();