1.1 --- a/src/HOL/Trancl.ML	Thu Aug 20 09:25:59 1998 +0200
     1.2 +++ b/src/HOL/Trancl.ML	Thu Aug 20 10:17:18 1998 +0200
     1.3 @@ -170,19 +170,8 @@
     1.4  by (blast_tac (claset() addIs prems addSDs[rtrancl_converseD])1);
     1.5  qed "converse_rtrancl_induct";
     1.6  
     1.7 -val prems = Goal
     1.8 - "[| ((a,b),(c,d)) : r^*; P c d; \
     1.9 -\    !!x y z u.[| ((x,y),(z,u)) : r;  ((z,u),(c,d)) : r^*;  P z u |] ==> P x y\
    1.10 -\ |] ==> P a b";
    1.11 -by (res_inst_tac[("R","P")]splitD 1);
    1.12 -by (res_inst_tac[("P","split P")]converse_rtrancl_induct 1);
    1.13 -by (resolve_tac prems 1);
    1.14 -by (Simp_tac 1);
    1.15 -by (resolve_tac prems 1);
    1.16 -by (split_all_tac 1);
    1.17 -by (Asm_full_simp_tac 1);
    1.18 -by (REPEAT(ares_tac prems 1));
    1.19 -qed "converse_rtrancl_induct2";
    1.20 +bind_thm ("converse_rtrancl_induct2", split_rule
    1.21 +  (read_instantiate [("a","(ax,ay)"),("b","(bx,by)")]converse_rtrancl_induct));
    1.22  
    1.23  val major::prems = Goal
    1.24   "[| (x,z):r^*; \
    1.25 @@ -194,10 +183,13 @@
    1.26  by (blast_tac (claset() addIs prems) 2);
    1.27  by (blast_tac (claset() addIs prems) 2);
    1.28  by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
    1.29 -qed "rtranclE2";
    1.30 +qed "converse_rtranclE";
    1.31 +
    1.32 +bind_thm ("converse_rtranclE2", split_rule
    1.33 +  (read_instantiate [("x","(xa,xb)"), ("z","(za,zb)")] converse_rtranclE));
    1.34  
    1.35  Goal "r O r^* = r^* O r";
    1.36 -by (blast_tac (claset() addEs [rtranclE, rtranclE2] 
    1.37 +by (blast_tac (claset() addEs [rtranclE, converse_rtranclE] 
    1.38  	               addIs [rtrancl_into_rtrancl, rtrancl_into_rtrancl2]) 1);
    1.39  qed "r_comp_rtrancl_eq";
    1.40