2012-09-17 blanchet 2012-09-17 tuned simpset
2012-09-17 blanchet 2012-09-17 cleaner way of dealing with the set functions of sums and products
2012-09-17 blanchet 2012-09-17 handle the general case with more than two levels of nesting when discharging induction prem prems
2012-09-17 blanchet 2012-09-17 clean unfolding of prod and sum sets
2012-09-17 blanchet 2012-09-17 got rid of one "auto" in induction tactic
2012-09-15 blanchet 2012-09-15 tuning
2012-09-14 blanchet 2012-09-14 killed spurious rotate_tac; use auto instead of blast
2012-09-14 blanchet 2012-09-14 polished the induction
2012-09-14 blanchet 2012-09-14 added induct tactic
2012-09-12 blanchet 2012-09-12 added sumEN_tupled_balanced
2012-09-12 blanchet 2012-09-12 tuning
2012-09-12 blanchet 2012-09-12 moved theorems closer to where they are used
2012-09-12 blanchet 2012-09-12 split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
2012-09-12 blanchet 2012-09-12 reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping