src/HOL/Trancl.ML
changeset 4799 82b0ed20c2cb
parent 4772 8c7e7eaffbdf
child 4830 bd73675adbed
     1.1 --- a/src/HOL/Trancl.ML	Sat Apr 04 14:30:19 1998 +0200
     1.2 +++ b/src/HOL/Trancl.ML	Tue Apr 07 13:43:07 1998 +0200
     1.3 @@ -153,7 +153,8 @@
     1.4  qed "rtrancl_converseI";
     1.5  
     1.6  goal Trancl.thy "(r^-1)^* = (r^*)^-1";
     1.7 -by (safe_tac (claset() addSDs [rtrancl_converseD] addSIs [rtrancl_converseI]));
     1.8 +by (safe_tac (claset() addSDs [rtrancl_converseD] addSIs [rtrancl_converseI]
     1.9 +			addSaltern ("split_all_tac", split_all_tac)));
    1.10  qed "rtrancl_converse";
    1.11  
    1.12  val major::prems = goal Trancl.thy
    1.13 @@ -331,7 +332,7 @@
    1.14  
    1.15  
    1.16  goal Trancl.thy "(r^+)^= = r^*";
    1.17 -by Safe_tac;
    1.18 +by (safe_tac (claset() addSaltern ("split_all_tac", split_all_tac)));
    1.19  by  (etac trancl_into_rtrancl 1);
    1.20  by (etac rtranclE 1);
    1.21  by  (Auto_tac );
    1.22 @@ -341,7 +342,7 @@
    1.23  Addsimps[reflcl_trancl];
    1.24  
    1.25  goal Trancl.thy "(r^=)^+ = r^*";
    1.26 -by Safe_tac;
    1.27 +by (safe_tac (claset() addSaltern ("split_all_tac", split_all_tac)));
    1.28  by  (dtac trancl_into_rtrancl 1);
    1.29  by  (Asm_full_simp_tac 1);
    1.30  by (etac rtranclE 1);