src/ZF/equalities.ML

 
 Goal "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)";
 by (blast_tac (claset() addSEs [equalityE]) 1);
 qed "Union_disjoint";
 
-goalw ZF.thy [Inter_def] "Inter(0) = 0";
+Goal "Union(A) = 0 <-> (ALL B:A. B=0)";
+by (Blast_tac 1);
+qed "Union_empty_iff";
+
+Goalw [Inter_def] "Inter(0) = 0";
 by (Blast_tac 1);
 qed "Inter_0";
 
 Goal "[| z:A; z:B |] ==> Inter(A) Un Inter(B) <= Inter(A Int B)";
 by (Blast_tac 1);

 
 Goal "Union(A) = (UN x:A. x)";
 by (Blast_tac 1);
 qed "Union_eq_UN";
 
-goalw ZF.thy [Inter_def] "Inter(A) = (INT x:A. x)";
+Goalw [Inter_def] "Inter(A) = (INT x:A. x)";
 by (Blast_tac 1);
 qed "Inter_eq_INT";
 
 Goal "(UN i:0. A(i)) = 0";
 by (Blast_tac 1);

 
 Goal "b:B ==> domain(A*B) = A";
 by (Blast_tac 1);
 qed "domain_of_prod";
 
-qed_goal "domain_0" ZF.thy "domain(0) = 0"
+qed_goal "domain_0" thy "domain(0) = 0"
  (fn _ => [ Blast_tac 1 ]);
 
-qed_goal "domain_cons" ZF.thy
+qed_goal "domain_cons" thy
     "domain(cons(<a,b>,r)) = cons(a, domain(r))"
  (fn _ => [ Blast_tac 1 ]);
 
 Goal "domain(A Un B) = domain(A) Un domain(B)";
 by (Blast_tac 1);

 
 Goal "a:A ==> range(A*B) = B";
 by (Blast_tac 1);
 qed "range_of_prod";
 
-qed_goal "range_0" ZF.thy "range(0) = 0"
+qed_goal "range_0" thy "range(0) = 0"
  (fn _ => [ Blast_tac 1 ]); 
 
-qed_goal "range_cons" ZF.thy
+qed_goal "range_cons" thy
     "range(cons(<a,b>,r)) = cons(b, range(r))"
  (fn _ => [ Blast_tac 1 ]);
 
 Goal "range(A Un B) = range(A) Un range(B)";
 by (Blast_tac 1);

 Addsimps [range_0, range_cons, range_Un_eq, range_converse];
 
 
 (** Field **)
 
-qed_goal "field_of_prod" ZF.thy "field(A*A) = A"
+qed_goal "field_of_prod" thy "field(A*A) = A"
  (fn _ => [ Blast_tac 1 ]); 
 
-qed_goal "field_0" ZF.thy "field(0) = 0"
+qed_goal "field_0" thy "field(0) = 0"
  (fn _ => [ Blast_tac 1 ]); 
 
-qed_goal "field_cons" ZF.thy
+qed_goal "field_cons" thy
     "field(cons(<a,b>,r)) = cons(a, cons(b, field(r)))"
  (fn _ => [ rtac equalityI 1, ALLGOALS (Blast_tac) ]);
 
 Goal "field(A Un B) = field(A) Un field(B)";
 by (Blast_tac 1);

 Goal "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))";
 by (Blast_tac 1);
 qed "converse_UN";
 
 (*Unfolding Inter avoids using excluded middle on A=0*)
-goalw ZF.thy [Inter_def] "converse(INT x:A. B(x)) = (INT x:A. converse(B(x)))";
+Goalw [Inter_def] "converse(INT x:A. B(x)) = (INT x:A. converse(B(x)))";
 by (Blast_tac 1);
 qed "converse_INT";
 
 Addsimps [converse_Un, converse_Int, converse_Diff, converse_UN, converse_INT];