src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
2013-09-26 blanchet 2013-09-26 tuning
2013-09-26 blanchet 2013-09-26 use new "sel_split(_asm)" to avoid giving rise to quantifiers, which would in turn require relying on injectivity
2013-09-26 blanchet 2013-09-26 strengthen tactic
2013-09-26 blanchet 2013-09-26 use needed case theorems
2013-09-26 blanchet 2013-09-26 more powerful/robust tactics
2013-09-26 blanchet 2013-09-26 tuning
2013-09-26 blanchet 2013-09-26 made tactic more flexible w.r.t. case expressions and such
2013-09-25 panny 2013-09-25 simplified code
2013-09-25 blanchet 2013-09-25 thread through bound types
2013-09-25 blanchet 2013-09-25 killed redundant argument
2013-09-25 blanchet 2013-09-25 move useful functions to library
2013-09-25 panny 2013-09-25 merge
2013-09-25 panny 2013-09-25 simplified code
2013-09-25 panny 2013-09-25 add non-corecursive constructor view theorems to simps
2013-09-25 blanchet 2013-09-25 more powerful fold
2013-09-24 blanchet 2013-09-24 commented out debugging output in "primcorec"
2013-09-24 blanchet 2013-09-24 started adding support for "nat_case" as case study for all "case" constructs
2013-09-24 panny 2013-09-24 support "of" syntax to disambiguate selector equations
2013-09-24 blanchet 2013-09-24 don't note more induction principles than there are functions + tuning
2013-09-24 panny 2013-09-24 add "primcorec" command (cf. ae7f50e70c09)
2013-09-24 blanchet 2013-09-24 set code and nitpick_simp attributes on primcorec theorems
2013-09-23 blanchet 2013-09-23 note coinduct theorems in "primcorec"
2013-09-23 blanchet 2013-09-23 generate "simps" from "primcorec"
2013-09-23 blanchet 2013-09-23 undid copy-paste
2013-09-23 blanchet 2013-09-23 avoid giving same name to simplifying constructor as to real one (to avoid risks of confusion when reading the code)
2013-09-23 blanchet 2013-09-23 tuned code
2013-09-20 blanchet 2013-09-20 renamed "primcorec" to "primcorecursive", to open the door to a 'theory -> theory' command called "primcorec" (cf. "fun" vs. "function")
2013-09-20 blanchet 2013-09-20 setting the stage for safe constructor simp rules
2013-09-19 blanchet 2013-09-19 added TODO
2013-09-19 traytel 2013-09-19 don't declare ctr view primcorec theorems as simp (they loop)
2013-09-19 panny 2013-09-19 simplified code; eliminated some dummyTs
2013-09-19 blanchet 2013-09-19 avoid infinite loop for unapplied terms + tuning
2013-09-19 blanchet 2013-09-19 generalize code to handle zero-argument case gracefully (e.g. for nullay functions defined over codatatypes that corecurse through "fun"
2013-09-19 blanchet 2013-09-19 simplified code
2013-09-19 panny 2013-09-19 generate more theorems (e.g. for types with only one constructor)
2013-09-18 panny 2013-09-18 generate constructor view theorems
2013-09-18 blanchet 2013-09-18 tuned tactics
2013-09-18 blanchet 2013-09-18 tuning
2013-09-16 panny 2013-09-16 prove simp theorems for newly generated definitions
2013-09-05 panny 2013-09-05 support indirect corecursion
2013-09-04 panny 2013-09-04 various refactoring; handle self-mappings; handle range types containing function types;
2013-09-02 panny 2013-09-02 handle direct corecursion
2013-09-01 panny 2013-09-01 improved interfaces
2013-09-01 panny 2013-09-01 simplified rewriting of map arguments
2013-08-31 traytel 2013-08-31 merged
2013-08-31 traytel 2013-08-31 honor mixfix specifications
2013-08-31 panny 2013-08-31 simplified recursive calls' replacement
2013-08-31 panny 2013-08-31 handle selector formulae with no corecursive calls
2013-08-30 panny 2013-08-30 fixed bug in primrec_new (allow indirect recursion through constructor arguments other than the first)
2013-08-30 blanchet 2013-08-30 more canonical naming
2013-08-30 blanchet 2013-08-30 moved keywords down the hierarchy
2013-08-30 blanchet 2013-08-30 polished newly included files after moving
2013-08-30 blanchet 2013-08-30 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository