src/HOL/equalities.ML
changeset 5967 e25938358318
parent 5941 1db9fad40a4f
child 5999 84fe61a08c17
equal deleted inserted replaced
5966:60f80b2a2777 5967:e25938358318
   106 qed "image_UNION";
   106 qed "image_UNION";
   107 
   107 
   108 Goal "(%x. x) `` Y = Y";
   108 Goal "(%x. x) `` Y = Y";
   109 by (Blast_tac 1);
   109 by (Blast_tac 1);
   110 qed "image_id";
   110 qed "image_id";
       
   111 Addsimps [image_id];
   111 
   112 
   112 Goal "f``(g``A) = (%x. f (g x)) `` A";
   113 Goal "f``(g``A) = (%x. f (g x)) `` A";
   113 by (Blast_tac 1);
   114 by (Blast_tac 1);
   114 qed "image_image";
   115 qed "image_image";
   115 
   116