Fri, 14 Sep 2012 22:23:10 +0200 select the right premise in "mk_induct_discharge_prem_prems_tac" instead of relying on backtracking
blanchet [Fri, 14 Sep 2012 22:23:10 +0200] rev 49376
select the right premise in "mk_induct_discharge_prem_prems_tac" instead of relying on backtracking
Fri, 14 Sep 2012 22:23:10 +0200 tuned code before fixing "mk_induct_discharge_prem_prems_tac"
blanchet [Fri, 14 Sep 2012 22:23:10 +0200] rev 49375
tuned code before fixing "mk_induct_discharge_prem_prems_tac"
Fri, 14 Sep 2012 21:26:01 +0200 tuned proofs;
wenzelm [Fri, 14 Sep 2012 21:26:01 +0200] rev 49374
tuned proofs;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip