src/HOL/Relation.ML
changeset 11655 923e4d0d36d5
parent 11451 8abfb4f7bd02
child 12487 bbd564190c9b
     1.1 --- a/src/HOL/Relation.ML	Wed Oct 03 20:54:05 2001 +0200
     1.2 +++ b/src/HOL/Relation.ML	Wed Oct 03 20:54:16 2001 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4  by (eresolve_tac prems 1);
     1.5  qed "IdE";
     1.6  
     1.7 -Goalw [Id_def] "(a,b):Id = (a=b)";
     1.8 +Goalw [Id_def] "((a,b):Id) = (a=b)";
     1.9  by (Blast_tac 1);
    1.10  qed "pair_in_Id_conv";
    1.11  AddIffs [pair_in_Id_conv];
    1.12 @@ -217,7 +217,7 @@
    1.13  
    1.14  (** Domain **)
    1.15  
    1.16 -Goalw [Domain_def] "a: Domain(r) = (EX y. (a,y): r)";
    1.17 +Goalw [Domain_def] "(a: Domain(r)) = (EX y. (a,y): r)";
    1.18  by (Blast_tac 1);
    1.19  qed "Domain_iff";
    1.20  
    1.21 @@ -275,7 +275,7 @@
    1.22  
    1.23  (** Range **)
    1.24  
    1.25 -Goalw [Domain_def, Range_def] "a: Range(r) = (EX y. (y,a): r)";
    1.26 +Goalw [Domain_def, Range_def] "(a: Range(r)) = (EX y. (y,a): r)";
    1.27  by (Blast_tac 1);
    1.28  qed "Range_iff";
    1.29  
    1.30 @@ -333,7 +333,7 @@
    1.31  
    1.32  overload_1st_set "Relation.Image";
    1.33  
    1.34 -Goalw [Image_def] "b : r``A = (EX x:A. (x,b):r)";
    1.35 +Goalw [Image_def] "(b : r``A) = (EX x:A. (x,b):r)";
    1.36  by (Blast_tac 1);
    1.37  qed "Image_iff";
    1.38