Fri, 14 Sep 2012 22:23:10 +0200 blanchet use right version of "mk_UnIN"
Fri, 14 Sep 2012 22:23:10 +0200 blanchet select the right premise in "mk_induct_discharge_prem_prems_tac" instead of relying on backtracking
Fri, 14 Sep 2012 22:23:10 +0200 blanchet tuned code before fixing "mk_induct_discharge_prem_prems_tac"
Fri, 14 Sep 2012 21:26:01 +0200 wenzelm tuned proofs;
Fri, 14 Sep 2012 21:23:06 +0200 wenzelm merged
Fri, 14 Sep 2012 12:09:27 +0200 blanchet polished the induction
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip