src/ZF/UNITY/Constrains.ML

    "[| F : A Co A'; B<=A; A'<=B' |] ==> F : B Co B'";
 by (blast_tac (claset() addIs [constrains_weaken, st_set_subset]) 1);
 qed "Constrains_weaken";
 
 (** Union **)
-Goalw [Constrains_def2]
+Goalw [Constrains_def2] 
 "[| F : A Co A'; F : B Co B' |] ==> F : (A Un B) Co (A' Un B')";
 by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [Int_Un_distrib2 RS sym]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Int_Un_distrib]) 1);
 by (blast_tac (claset() addIs [constrains_Un]) 1);
 qed "Constrains_Un";
 
 val [major, minor] = Goalw [Constrains_def2]
 "[|(!!i. i:I==>F:A(i) Co A'(i)); F:program|] ==> F:(UN i:I. A(i)) Co (UN i:I. A'(i))";
 by (cut_facts_tac [minor] 1);
 by (auto_tac (claset() addDs [major]
                        addIs [constrains_UN],
-              simpset() addsimps [Int_UN_distrib]));
+              simpset() delsimps UN_simps addsimps [Int_UN_distrib]));
 qed "Constrains_UN";
 
 (** Intersection **)
 
 Goalw [Constrains_def]

 by (case_tac "I=0" 1);
 by (asm_full_simp_tac (simpset() addsimps [Inter_def]) 1);
 by (subgoal_tac "reachable(F) Int Inter(RepFun(I, A)) = (INT i:I. reachable(F) Int A(i))" 1);
 by (force_tac (claset(), simpset() addsimps [Inter_def]) 2);
 by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1);
+by (subgoal_tac "reachable(F) Int Inter(RepFun(I, A)) = (INT i:I. reachable(F) Int A(i))" 1);
+by (Force_tac 2);
+by (asm_simp_tac (simpset() delsimps INT_simps) 1);
 by (rtac constrains_INT 1);
 by (etac not_emptyE 1);
 by (dresolve_tac [major] 1);
 by (rewrite_goal_tac [Constrains_def] 1);
 by (ALLGOALS(Asm_full_simp_tac));

 by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1);
 qed "Constrains_trans";
 
 Goalw [Constrains_def2]
 "[| F : A Co (A' Un B); F : B Co B' |] ==> F : A Co (A' Un B')";
-by (full_simp_tac (simpset() addsimps [Int_Un_distrib2 RS sym]) 1);
+by (full_simp_tac (simpset() addsimps [Int_Un_distrib]) 1);
 by (blast_tac (claset() addIs [constrains_cancel]) 1);
 qed "Constrains_cancel";
 
 (*** Stable ***)
 (* Useful because there's no Stable_weaken.  [Tanja Vos] *)