# HG changeset patch
# User paulson
# Date 971345759 -7200
# Node ID 4d1af711cf7ba291c31b044af5b315b570565e4d
# Parent  325b6279ae4f9806195721b9a01e7388045aa5f5
new I-rules r_into_rtrancl, r_into_trancl and a simpler proof

diff -r 325b6279ae4f -r 4d1af711cf7b src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Thu Oct 12 12:15:23 2000 +0200
+++ b/src/HOL/Trancl.ML	Thu Oct 12 12:15:59 2000 +0200
@@ -39,6 +39,8 @@
 by (etac (rtrancl_refl RS rtrancl_into_rtrancl) 1);
 qed "r_into_rtrancl";
 
+AddIs [r_into_rtrancl];
+
 (*monotonicity of rtrancl*)
 Goalw [rtrancl_def] "r <= s ==> r^* <= s^*";
 by (REPEAT(ares_tac [lfp_mono,Un_mono,comp_mono,subset_refl] 1));
@@ -103,7 +105,6 @@
 
 Goal "(r^*)^* = r^*";
 by Auto_tac;
-by (etac r_into_rtrancl 2);
 by (etac rtrancl_induct 1);
 by (rtac rtrancl_refl 1);
 by (blast_tac (claset() addIs rtranclIs) 1);
@@ -224,6 +225,7 @@
 by (split_all_tac 1);
 by (REPEAT (ares_tac [prem,compI,rtrancl_refl] 1));
 qed "r_into_trancl";
+AddIs [r_into_trancl];
 
 (*intro rule by definition: from rtrancl and r*)
 Goalw [trancl_def] "[| (a,b) : r^*;  (b,c) : r |]   ==>  (a,c) : r^+";
@@ -336,10 +338,7 @@
 Goal "(x,y):R^+ ==> ? z. (x,z):R & (z,y):R^*";
 be converse_trancl_induct 1;
 by Auto_tac;
-br exI 1;
-be conjI 1;
-be (r_into_rtrancl RS rtrancl_trans) 1;
-ba 1;
+by (blast_tac (claset() addIs [rtrancl_trans]) 1);
 qed "tranclD";
 
 (*Unused*)