src/HOL/Relation.ML

 by (rtac (major RS CollectE) 1);
 by (etac exE 1);
 by (eresolve_tac prems 1);
 qed "IdE";
 
-Goalw [Id_def] "(a,b):Id = (a=b)";
+Goalw [Id_def] "((a,b):Id) = (a=b)";
 by (Blast_tac 1);
 qed "pair_in_Id_conv";
 AddIffs [pair_in_Id_conv];
 
 Goalw [refl_def] "reflexive Id";

 by (Blast_tac 1);
 qed "trans_converse";
 
 (** Domain **)
 
-Goalw [Domain_def] "a: Domain(r) = (EX y. (a,y): r)";
+Goalw [Domain_def] "(a: Domain(r)) = (EX y. (a,y): r)";
 by (Blast_tac 1);
 qed "Domain_iff";
 
 Goal "(a,b): r ==> a: Domain(r)";
 by (etac (exI RS (Domain_iff RS iffD2)) 1) ;

 qed "Domain_mono";
 
 
 (** Range **)
 
-Goalw [Domain_def, Range_def] "a: Range(r) = (EX y. (y,a): r)";
+Goalw [Domain_def, Range_def] "(a: Range(r)) = (EX y. (y,a): r)";
 by (Blast_tac 1);
 qed "Range_iff";
 
 Goalw [Range_def] "(a,b): r ==> b : Range(r)";
 by (etac (converseI RS DomainI) 1);

 
 (*** Image of a set under a relation ***)
 
 overload_1st_set "Relation.Image";
 
-Goalw [Image_def] "b : r``A = (EX x:A. (x,b):r)";
+Goalw [Image_def] "(b : r``A) = (EX x:A. (x,b):r)";
 by (Blast_tac 1);
 qed "Image_iff";
 
 Goalw [Image_def] "r``{a} = {b. (a,b):r}";
 by (Blast_tac 1);