Set.ML

     "[| ! x:A. P(x);  x:A |] ==> P(x)";
 by (rtac (minor RS (major RS spec RS mp)) 1);
 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();
 
 (*Takes assumptions ! x:A.P(x) and a:A; creates assumption P(a)*)

 val rev_subsetD = prove_goal Set.thy "[| c:A;  A <= B |] ==> c:B"
  (fn prems=>  [ (REPEAT (resolve_tac (prems@[subsetD]) 1)) ]);
 
 (*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();
 
 (*Takes assumptions A<=B; c:A and creates the assumption c:B *)

 by (resolve_tac prems 1);
 by (REPEAT (resolve_tac (prems RL [equalityD1,equalityD2]) 1));
 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();
 
 (*Lemma for creating induction formulae -- for "pattern matching" on p

 
 (*This form, with negated conclusion, works well with the Classical prover.
   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();
 
 val ComplE = make_elim ComplD;
 

 val prems = goalw Set.thy [Un_def] "c:B ==> c : A Un B";
 by (REPEAT (resolve_tac (prems @ [CollectI,disjI2]) 1));
 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)),
     (REPEAT (ares_tac (prems@[UnI2,notE]) 1)) ]);
 

 
 
 (*** 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]
     "c : A - B ==> c : A"
  (fn [major]=> [ (rtac (major RS CollectD RS conjunct1) 1) ]);

     "[| c : A - B;  c : B |] ==> P"
  (fn [major,minor]=>
      [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) ]);
 
 
 (*** The empty set -- {} ***)
 

 
 val insert_iff = prove_goal Set.thy "a : insert(b,A) = (a=b | a:A)"
  (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) ]);
 
 (*** Singletons, using insert ***)

 by (resolve_tac prems 1);
 val INT_D = result();
 
 (*"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();
 
 val prems = goal Set.thy

 by (resolve_tac prems 1);
 val InterD = result();
 
 (*"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();