src/HOL/Relation.ML
 changeset 1454 d0266c81a85e parent 1264 3eb91524b938 child 1465 5d7a7e439cec
```--- a/src/HOL/Relation.ML	Fri Jan 26 13:43:36 1996 +0100
+++ b/src/HOL/Relation.ML	Fri Jan 26 20:25:39 1996 +0100
@@ -35,7 +35,7 @@

val prems = goalw Relation.thy [comp_def]
"[| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
-by (fast_tac (set_cs addIs prems) 1);
+by (fast_tac (prod_cs addIs prems) 1);
qed "compI";

(*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
@@ -44,7 +44,7 @@
\       !!x y z. [| xz = (x,z);  (x,y):s;  (y,z):r |] ==> P \
\    |] ==> P";
by (cut_facts_tac prems 1);
-by (REPEAT (eresolve_tac [CollectE, exE, conjE] 1 ORELSE ares_tac prems 1));
+by (REPEAT (eresolve_tac [CollectE, splitE, exE, conjE] 1 ORELSE ares_tac prems 1));
qed "compE";

val prems = goal Relation.thy
@@ -84,7 +84,6 @@

goalw Relation.thy [converse_def] "!!a b r. (a,b):r ==> (b,a):converse(r)";
by (Simp_tac 1);
-by (fast_tac set_cs 1);
qed "converseI";

goalw Relation.thy [converse_def] "!!a b r. (a,b) : converse(r) ==> (b,a) : r";
@@ -97,8 +96,7 @@
\    |] ==> P"
(fn [major,minor]=>
[ (rtac (major RS CollectE) 1),
-    (REPEAT (eresolve_tac [bexE,exE, conjE, minor] 1)),
-    (hyp_subst_tac 1),
+    (REPEAT (eresolve_tac [splitE, bexE,exE, conjE, minor] 1)),
(assume_tac 1) ]);

val converse_cs = comp_cs addSIs [converseI] ```