src/HOL/Relation.ML
changeset 11136 e34e7f6d9b57
parent 10832 e33b47e4246d
child 11451 8abfb4f7bd02
     1.1 --- a/src/HOL/Relation.ML	Thu Feb 15 16:00:38 2001 +0100
     1.2 +++ b/src/HOL/Relation.ML	Thu Feb 15 16:00:40 2001 +0100
     1.3 @@ -468,3 +468,13 @@
     1.4  by (atac 1);
     1.5  by (atac 1);
     1.6  qed "fun_rel_comp_unique";
     1.7 +
     1.8 +
     1.9 +section "inverse image";
    1.10 +
    1.11 +Goalw [trans_def,inv_image_def]
    1.12 +    "!!r. trans r ==> trans (inv_image r f)";
    1.13 +by (Simp_tac 1);
    1.14 +by (Blast_tac 1);
    1.15 +qed "trans_inv_image";
    1.16 +