Tue, 21 Apr 1998 17:25:19 +0200 improved pair_tac to call prune_params_tac afterwards
oheimb [Tue, 21 Apr 1998 17:25:19 +0200] rev 4819
improved pair_tac to call prune_params_tac afterwards improved the (bad) efficiency of split_all_tac by about 50% split_all_tac is now added to claset() _before_ other safe tactics
Tue, 21 Apr 1998 17:23:24 +0200 split_all_tac is now added to claset() _before_ other safe tactics
oheimb [Tue, 21 Apr 1998 17:23:24 +0200] rev 4818
split_all_tac is now added to claset() _before_ other safe tactics
(0) -3000 -1000 -300 -100 -30 -10 -2 +2 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip