src/HOL/Univ.ML

 val dsum_subset_Sigma = [dsum_mono, dsum_Sigma] MRS subset_trans |> standard;
 
 
 (*** Domain ***)
 
-Goal "fst `` diag(A) = A";
+Goal "Domain (diag A) = A";
 by Auto_tac;
-qed "fst_image_diag";
-
-Goal "fst `` (r<**>s) = (fst``r) <*> (fst``s)";
+qed "Domain_diag";
+
+Goal "Domain (r<**>s) = (Domain r) <*> (Domain s)";
 by Auto_tac;
-qed "fst_image_dprod";
-
-Goal "fst `` (r<++>s) = (fst``r) <+> (fst``s)";
+qed "Domain_dprod";
+
+Goal "Domain (r<++>s) = (Domain r) <+> (Domain s)";
 by Auto_tac;
-qed "fst_image_dsum";
-
-Addsimps [fst_image_diag, fst_image_dprod, fst_image_dsum];
+qed "Domain_dsum";
+
+Addsimps [Domain_diag, Domain_dprod, Domain_dsum];