Fri, 14 Sep 2012 22:23:10 +0200 | blanchet | use right version of "mk_UnIN" | changeset | files |
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 | changeset | files |
Fri, 14 Sep 2012 22:23:10 +0200 | blanchet | tuned code before fixing "mk_induct_discharge_prem_prems_tac" | changeset | files |
Fri, 14 Sep 2012 21:26:01 +0200 | wenzelm | tuned proofs; | changeset | files |
Fri, 14 Sep 2012 21:23:06 +0200 | wenzelm | merged | changeset | files |
Fri, 14 Sep 2012 12:09:27 +0200 | blanchet | polished the induction | changeset | files |