src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
2013-10-01 blanchet 2013-10-01 renamed theory file
2013-09-28 wenzelm 2013-09-28 make SML/NJ more happy;
2013-09-27 blanchet 2013-09-27 faster exit in common case
2013-09-26 blanchet 2013-09-26 tuning
2013-09-26 blanchet 2013-09-26 avoid calls to nth with ~1
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 use needed case theorems
2013-09-25 panny 2013-09-25 simplified code
2013-09-25 blanchet 2013-09-25 don't generate wrong type
2013-09-25 blanchet 2013-09-25 proper handling of abstractions
2013-09-25 blanchet 2013-09-25 fixed off-by-one bug
2013-09-25 blanchet 2013-09-25 further improved 'code' helper functions
2013-09-25 blanchet 2013-09-25 removed spurious recursion
2013-09-25 blanchet 2013-09-25 robustness
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 improved massaging of case expressions
2013-09-25 blanchet 2013-09-25 filled in gap in library offering
2013-09-25 blanchet 2013-09-25 break more conjunctions
2013-09-25 blanchet 2013-09-25 move useful functions to library
2013-09-25 blanchet 2013-09-25 more powerful fold
2013-09-25 blanchet 2013-09-25 properly fold over branches
2013-09-25 blanchet 2013-09-25 removed dead code
2013-09-25 blanchet 2013-09-25 keep a database of free constructor type information
2013-09-25 blanchet 2013-09-25 generalized case-handling code a bit
2013-09-25 blanchet 2013-09-25 support cases for new-style (co)datatypes
2013-09-25 blanchet 2013-09-25 use case rather than sequence of ifs in expansion
2013-09-24 blanchet 2013-09-24 started adding support for "nat_case" as case study for all "case" constructs
2013-09-24 blanchet 2013-09-24 made SML/NJ happy
2013-09-24 blanchet 2013-09-24 tuning
2013-09-20 blanchet 2013-09-20 have "datatype_new_compat" register induction and recursion theorems in nested case
2013-09-19 blanchet 2013-09-19 killed exceptional code that is anyway no longer needed, now that the 'simp' attribute has been taken away -- this solves issues in 'primcorec'
2013-09-19 blanchet 2013-09-19 avoid infinite loop for unapplied terms + tuning
2013-09-19 blanchet 2013-09-19 give lambda abstractions a chance, as an alternative to function composition, for corecursion via "fun"
2013-09-19 blanchet 2013-09-19 added auxiliary function
2013-09-19 blanchet 2013-09-19 added helper function for code equations in primcorec
2013-09-19 blanchet 2013-09-19 split functionality into two functions to avoid redoing work over and over
2013-09-19 blanchet 2013-09-19 added massaging function for primcorec code equations
2013-09-19 blanchet 2013-09-19 simplified code
2013-09-19 blanchet 2013-09-19 no need for beta-eta contraction
2013-09-19 blanchet 2013-09-19 generalize helper function
2013-09-18 blanchet 2013-09-18 enrich data structure
2013-09-13 blanchet 2013-09-13 made non-co case more robust as well (cf. b6e2993fd0d3)
2013-09-13 blanchet 2013-09-13 don't wrongly destroy sum types in coiterators
2013-09-13 blanchet 2013-09-13 beware of multi-constructor datatypes (cf. 27c418b7b985)
2013-09-13 blanchet 2013-09-13 beware of single-constructor datatypes, with no discriminators
2013-09-09 blanchet 2013-09-09 include map theorems in datastructure for "primcorec"
2013-09-09 blanchet 2013-09-09 enriched data structure with necessary theorems
2013-09-05 panny 2013-09-05 support indirect corecursion
2013-08-30 blanchet 2013-08-30 more canonical naming
2013-08-30 blanchet 2013-08-30 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository