diff -r 14bd6e5985f1 -r a75558a4ed37 src/HOL/Subst/Setplus.ML
--- a/src/HOL/Subst/Setplus.ML	Thu May 15 12:29:59 1997 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-(*  Title:      Substitutions/setplus.ML
-    Author:     Martin Coen, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
-
-For setplus.thy.
-Properties of subsets and empty sets.
-*)
-
-open Setplus;
-
-(*********)
-
-(*** Rules for subsets ***)
-
-goal Set.thy "A <= B =  (! t.t:A --> t:B)";
-by (fast_tac set_cs 1);
-qed "subset_iff";
-
-goalw Setplus.thy [ssubset_def] "A < B = ((A <= B) & ~(A=B))";
-by (rtac refl 1);
-qed "ssubset_iff";
-
-goal Setplus.thy "((A::'a set) <= B) = ((A < B) | (A=B))";
-by (simp_tac (simpset_of "Fun" addsimps [ssubset_iff]) 1);
-by (fast_tac set_cs 1);
-qed "subseteq_iff_subset_eq";
-
-(*Rule in Modus Ponens style*)
-goal Setplus.thy "A < B --> c:A --> c:B";
-by (simp_tac (simpset_of "Fun" addsimps [ssubset_iff]) 1);
-by (fast_tac set_cs 1);
-qed "ssubsetD";
-
-(*********)
-
-goalw Setplus.thy [empty_def] "~ a : {}";
-by (fast_tac set_cs 1);
-qed "not_in_empty";
-
-goalw Setplus.thy [empty_def] "(A = {}) = (ALL a.~ a:A)";
-by (fast_tac (set_cs addIs [set_ext]) 1);
-qed "empty_iff";
-
-
-(*********)
-
-goal Set.thy "(~A=B)  = ((? x.x:A & ~x:B) | (? x.~x:A & x:B))";
-by (fast_tac (set_cs addIs [set_ext]) 1);
-qed "not_equal_iff";
-
-(*********)
-
-val setplus_rews = [ssubset_iff,not_in_empty,empty_iff];
-
-(*********)
-
-(*Case analysis for rewriting; P also gets rewritten*)
-val [prem1,prem2] = goal HOL.thy "[| P-->Q;  ~P-->Q |] ==> Q";
-by (rtac (excluded_middle RS disjE) 1);
-by (etac (prem2 RS mp) 1);
-by (etac (prem1 RS mp) 1);
-qed "imp_excluded_middle";
-
-fun imp_excluded_middle_tac s = res_inst_tac [("P",s)] imp_excluded_middle;