src/HOL/Relation.ML
changeset 1642 21db0cf9a1a4
parent 1605 248e1e125ca0
child 1694 3452958f85a8
     1.1 --- a/src/HOL/Relation.ML	Thu Apr 04 11:43:25 1996 +0200
     1.2 +++ b/src/HOL/Relation.ML	Thu Apr 04 11:45:01 1996 +0200
     1.3 @@ -62,8 +62,8 @@
     1.4  qed "comp_mono";
     1.5  
     1.6  goal Relation.thy
     1.7 -    "!!r s. [| s <= Sigma A (%x.B);  r <= Sigma B (%x.C) |] ==> \
     1.8 -\           (r O s) <= Sigma A (%x.C)";
     1.9 +    "!!r s. [| s <= A Times B;  r <= B Times C |] ==> \
    1.10 +\           (r O s) <= A Times C";
    1.11  by (fast_tac comp_cs 1);
    1.12  qed "comp_subset_Sigma";
    1.13  
    1.14 @@ -161,7 +161,7 @@
    1.15      (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);
    1.16  
    1.17  qed_goal "Image_subset" Relation.thy
    1.18 -    "!!A B r. r <= Sigma A (%x.B) ==> r^^C <= B"
    1.19 +    "!!A B r. r <= A Times B ==> r^^C <= B"
    1.20   (fn _ =>
    1.21    [ (rtac subsetI 1),
    1.22      (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]);