2014-01-13 blanchet 2014-01-13 repaired 'ctr' tactic w.r.t. 'split'
2014-01-10 blanchet 2014-01-10 cope gracefully with missing ctr equations by plugging in 'False ==> ...'
2014-01-10 blanchet 2014-01-10 strengthened tactic to handle 'disc_iff' equations of the form '... = False'
2014-01-10 blanchet 2014-01-10 tuning
2014-01-10 blanchet 2014-01-10 generate 'disc_iff' for all discriminators
2014-01-10 blanchet 2014-01-10 fixed 'disc_iff' tactic in the case where different equations use different variable names for the function arguments
2014-01-09 blanchet 2014-01-09 reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
2014-01-09 blanchet 2014-01-09 strengthened tactics w.r.t. 'lets' and tuples
2014-01-09 blanchet 2014-01-09 strengthen tac w.r.t. lets with tuples
2014-01-03 blanchet 2014-01-03 more SML-ish (less Haskell-ish) naming convention
2014-01-03 blanchet 2014-01-03 strengthened tactic
2014-01-03 blanchet 2014-01-03 refactoring
2014-01-03 blanchet 2014-01-03 instantiate schematics as projections to avoid HOU trouble
2014-01-02 blanchet 2014-01-02 generalized tactic to the case of several assumptions per equation
2014-01-02 blanchet 2014-01-02 made tactic behave better w.r.t. HO unification (might not be enough, and might have to fix some variables eventually though...)
2014-01-02 blanchet 2014-01-02 made tactic more robust
2014-01-02 blanchet 2014-01-02 made tactic handle corner cases, where some of the 'disc' properties are missing, correctly
2014-01-02 blanchet 2014-01-02 simplified code
2014-01-02 blanchet 2014-01-02 prevent tactic from getting out of sync and wrongly attack next subgoal
2014-01-02 blanchet 2014-01-02 properly synchronize parallel lists
2014-01-02 blanchet 2014-01-02 graceful handling of one-constructor case
2014-01-02 blanchet 2014-01-02 gracefully handle single-equation case, where 'nchotomy' is 'True'
2014-01-02 blanchet 2014-01-02 made tactic handle gracefully the case of missing constructors
2014-01-02 blanchet 2014-01-02 don't generate any proof obligation for implicit (de facto) exclusiveness
2014-01-02 blanchet 2014-01-02 generate 'disc_iff' property in 'primcorec'
2014-01-02 blanchet 2014-01-02 added tactic to prove 'disc_iff' properties in 'primcorec'
2013-12-21 blanchet 2013-12-21 generate exhaust from nchotomy
2013-12-21 blanchet 2013-12-21 made tactic work with theorems with multiple assumptions
2013-12-21 blanchet 2013-12-21 renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package)
2013-12-19 blanchet 2013-12-19 implemented 'exhaustive' option in tactic
2013-12-01 panny 2013-12-01 more work towards "exhaustive"
2013-11-06 blanchet 2013-11-06 removed dead code
2013-11-04 blanchet 2013-11-04 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')