src/HOL/Set.ML

 open Set;
 
 section "Relating predicates and sets";
 
 val [prem] = goal Set.thy "P(a) ==> a : {x.P(x)}";
-by (rtac (mem_Collect_eq RS ssubst) 1);
+by (stac mem_Collect_eq 1);
 by (rtac prem 1);
 qed "CollectI";
 
 val prems = goal Set.thy "[| a : {x.P(x)} |] ==> P(a)";
 by (resolve_tac (prems RL [mem_Collect_eq  RS subst]) 1);

 qed "singletonD";
 
 bind_thm ("singletonE", make_elim singletonD);
 
 qed_goal "singleton_iff" thy "(b : {a}) = (b=a)" (fn _ => [
-	rtac iffI 1,
-	etac singletonD 1,
-	hyp_subst_tac 1,
-	rtac singletonI 1]);
+        rtac iffI 1,
+        etac singletonD 1,
+        hyp_subst_tac 1,
+        rtac singletonI 1]);
 
 val [major] = goal Set.thy "{a}={b} ==> a=b";
 by (rtac (major RS equalityD1 RS subsetD RS singletonD) 1);
 by (rtac singletonI 1);
 qed "singleton_inject";

 
 (*** Set reasoning tools ***)
 
 
 val mem_simps = [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff, 
-		 mem_Collect_eq];
+                 mem_Collect_eq];
 
 (*Not for Addsimps -- it can cause goals to blow up!*)
 goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
 by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
 qed "mem_if";