# HG changeset patch
# User lcp
# Date 777203660 -7200
# Node ID 82c4117aff7f011151f6ee9fc8348e88f3aec1af
# Parent  960e332d2e70ed2205316dad2dd3c41f06ee9b5a
HOL/Trancl: comp_cs is based upon prod_cs; tidied proofs

diff -r 960e332d2e70 -r 82c4117aff7f Trancl.ML
--- a/Trancl.ML	Thu Aug 18 11:43:40 1994 +0200
+++ b/Trancl.ML	Thu Aug 18 11:54:20 1994 +0200
@@ -61,20 +61,16 @@
 by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Pair_inject,ssubst] 1));
 val compEpair = result();
 
-val comp_cs = set_cs addIs [compI,idI] 
-		     addSEs [compE,idE,Pair_inject];
+val comp_cs = prod_cs addIs [compI, idI] addSEs [compE, idE];
 
-val prems = goal Trancl.thy
-    "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
-by (cut_facts_tac prems 1);
+goal Trancl.thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
 by (fast_tac comp_cs 1);
 val comp_mono = result();
 
-val prems = goal Trancl.thy
-    "[| s <= Sigma(A,%x.B);  r <= Sigma(B,%x.C) |] ==> \
-\    (r O s) <= Sigma(A,%x.C)";
-by (cut_facts_tac prems 1);
-by (fast_tac (comp_cs addIs [SigmaI] addSEs [SigmaE2]) 1);
+goal Trancl.thy
+    "!!r s. [| s <= Sigma(A,%x.B);  r <= Sigma(B,%x.C) |] ==> \
+\           (r O s) <= Sigma(A,%x.C)";
+by (fast_tac comp_cs 1);
 val comp_subset_Sigma = result();
 
 
@@ -230,11 +226,8 @@
 by (fast_tac (comp_cs addSEs [SigmaE2]) 1);
 val trancl_subset_Sigma_lemma = result();
 
-val prems = goalw Trancl.thy [trancl_def]
-    "r <= Sigma(A,%x.A) ==> trancl(r) <= Sigma(A,%x.A)";
-by (cut_facts_tac prems 1);
-by (fast_tac (comp_cs addIs [SigmaI] 
-                      addSDs [trancl_subset_Sigma_lemma]
-                      addSEs [SigmaE2]) 1);
+goalw Trancl.thy [trancl_def]
+    "!!r. r <= Sigma(A,%x.A) ==> trancl(r) <= Sigma(A,%x.A)";
+by (fast_tac (comp_cs addSDs [trancl_subset_Sigma_lemma]) 1);
 val trancl_subset_Sigma = result();