changeset 3024 | 005d899b5c48 |
parent 2922 | 580647a879cf |
child 3439 | 54785105178c |
--- a/src/HOL/Lambda/Commutation.ML Wed Apr 23 11:18:29 1997 +0200 +++ b/src/HOL/Lambda/Commutation.ML Wed Apr 23 11:20:18 1997 +0200 @@ -94,6 +94,6 @@ rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1); by (etac rtrancl_induct 1); by (Blast_tac 1); -by (blast_tac (!claset delrules [rtrancl_refl] - addIs [r_into_rtrancl, rtrancl_trans]) 1); +by (Blast.depth_tac (!claset delrules [rtrancl_refl] + addIs [r_into_rtrancl, rtrancl_trans]) 12 1); qed "Church_Rosser_confluent";