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