src/HOL/Relation.ML
changeset 1454 d0266c81a85e
parent 1264 3eb91524b938
child 1465 5d7a7e439cec
     1.1 --- a/src/HOL/Relation.ML	Fri Jan 26 13:43:36 1996 +0100
     1.2 +++ b/src/HOL/Relation.ML	Fri Jan 26 20:25:39 1996 +0100
     1.3 @@ -35,7 +35,7 @@
     1.4  
     1.5  val prems = goalw Relation.thy [comp_def]
     1.6      "[| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
     1.7 -by (fast_tac (set_cs addIs prems) 1);
     1.8 +by (fast_tac (prod_cs addIs prems) 1);
     1.9  qed "compI";
    1.10  
    1.11  (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
    1.12 @@ -44,7 +44,7 @@
    1.13  \       !!x y z. [| xz = (x,z);  (x,y):s;  (y,z):r |] ==> P \
    1.14  \    |] ==> P";
    1.15  by (cut_facts_tac prems 1);
    1.16 -by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1));
    1.17 +by (REPEAT (eresolve_tac [CollectE, splitE, exE, conjE] 1 ORELSE ares_tac prems 1));
    1.18  qed "compE";
    1.19  
    1.20  val prems = goal Relation.thy
    1.21 @@ -84,7 +84,6 @@
    1.22  
    1.23  goalw Relation.thy [converse_def] "!!a b r. (a,b):r ==> (b,a):converse(r)";
    1.24  by (Simp_tac 1);
    1.25 -by (fast_tac set_cs 1);
    1.26  qed "converseI";
    1.27  
    1.28  goalw Relation.thy [converse_def] "!!a b r. (a,b) : converse(r) ==> (b,a) : r";
    1.29 @@ -97,8 +96,7 @@
    1.30  \    |] ==> P"
    1.31   (fn [major,minor]=>
    1.32    [ (rtac (major RS CollectE) 1),
    1.33 -    (REPEAT (eresolve_tac [bexE,exE, conjE, minor] 1)),
    1.34 -    (hyp_subst_tac 1),
    1.35 +    (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1)),
    1.36      (assume_tac 1) ]);
    1.37  
    1.38  val converse_cs = comp_cs addSIs [converseI]