src/HOL/Relation.ML
changeset 4601 87fc0d44b837
parent 4593 6fc8f224655f
child 4644 ecf8f17f6fe0
     1.1 --- a/src/HOL/Relation.ML	Thu Feb 05 10:47:29 1998 +0100
     1.2 +++ b/src/HOL/Relation.ML	Thu Feb 05 10:48:43 1998 +0100
     1.3 @@ -178,6 +178,12 @@
     1.4  
     1.5  Addsimps [Image_empty];
     1.6  
     1.7 +goal thy "id ^^ A = A";
     1.8 +by (Blast_tac 1);
     1.9 +qed "Image_id";
    1.10 +
    1.11 +Addsimps [Image_id];
    1.12 +
    1.13  qed_goal "Image_Int_subset" Relation.thy
    1.14      "R ^^ (A Int B) <= R ^^ A Int R ^^ B"
    1.15   (fn _ => [ Blast_tac 1 ]);