src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
2013-11-04 blanchet 2013-11-04 tuning
2013-10-20 blanchet 2013-10-20 tuning
2013-10-18 blanchet 2013-10-18 set stage for more flexible 'primrec' syntax for recursion through functions
2013-10-18 blanchet 2013-10-18 make sure that registered code equations are actually equations
2013-10-14 blanchet 2013-10-14 more defensive Nitpick setup -- exotic types of recursion are not supported yet in the model finder
2013-10-02 blanchet 2013-10-02 don't register equations of the form 'f x = ...' as simp rules, even if they are safe (noncorecursive), because they unfold too aggresively concepts users are likely to want to stay folded
2013-10-01 blanchet 2013-10-01 renamed theory file
2013-09-28 wenzelm 2013-09-28 make SML/NJ more happy;
2013-09-26 blanchet 2013-09-26 added data query function
2013-09-26 blanchet 2013-09-26 tuning
2013-09-25 blanchet 2013-09-25 improved massaging of case expressions
2013-09-24 blanchet 2013-09-24 register codatatypes with Nitpick
2013-09-23 blanchet 2013-09-23 register codatatypes with Nitpick
2013-09-23 blanchet 2013-09-23 tuning
2013-09-23 blanchet 2013-09-23 don't generate empty theorem collections
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-18 blanchet 2013-09-18 removed spurious "simp"
2013-09-18 blanchet 2013-09-18 use singular to avoid confusion
2013-09-15 blanchet 2013-09-15 added missing theorems to "simps" collection
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-12 traytel 2013-09-12 conceal definitions of high-level constructors and (co)iterators
2013-09-12 blanchet 2013-09-12 avoid a keyword
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-08-30 blanchet 2013-08-30 more canonical naming
2013-08-29 blanchet 2013-08-29 renamed BNF fact
2013-08-29 blanchet 2013-08-29 renamed BNF fact
2013-08-29 blanchet 2013-08-29 renamed BNF axiom
2013-08-29 blanchet 2013-08-29 merge
2013-08-29 blanchet 2013-08-29 handle type class annotations on (co)datatype parameters gracefully
2013-08-29 traytel 2013-08-29 store nesting_bnfs in fp_sugar (required in "nested to mutual" reduction)
2013-08-29 blanchet 2013-08-29 cleaner handling of bootstrapping "fake" context, with fewer (no?) obscure bugs
2013-08-29 blanchet 2013-08-29 qualify generated constants uniformly
2013-08-29 blanchet 2013-08-29 rationalize message generation + added a warning
2013-08-29 traytel 2013-08-29 build relator term for compound type (generalized build_map)
2013-08-29 blanchet 2013-08-29 documentation ideas
2013-08-29 blanchet 2013-08-29 more
2013-08-28 blanchet 2013-08-28 better error message
2013-08-28 blanchet 2013-08-28 tuning
2013-08-26 blanchet 2013-08-26 simplify code (now that ctr_sugar uses the same type variables as fp_sugar)
2013-08-26 traytel 2013-08-26 moved derivation of ctor_dtor_unfold to sugar (streamlines fp_result interface)
2013-08-22 traytel 2013-08-22 configuration option to control timing output for (co)datatypes
2013-08-21 traytel 2013-08-21 transfer stored fp_sugar theorems into the "current" theory when retrieving an fp_sugar (avoids non-trivial merges)
2013-08-20 traytel 2013-08-20 moved derivation of strong coinduction to sugar
2013-08-16 blanchet 2013-08-16 tuning
2013-08-16 blanchet 2013-08-16 moved function to where it seems to belong
2013-08-16 blanchet 2013-08-16 moved library function where it belongs, and used Dmitriy's inside-out implementation
2013-08-16 blanchet 2013-08-16 added useful library function
2013-08-16 traytel 2013-08-16 tuned
2013-08-16 blanchet 2013-08-16 moved useful library functions upstream
2013-08-14 blanchet 2013-08-14 added fixme
2013-08-12 blanchet 2013-08-12 clarified option name (since case/fold/rec are also destructors)
2013-08-12 blanchet 2013-08-12 define case constant from other 'free constructor' axioms
2013-08-12 blanchet 2013-08-12 qualify map and rel names
2013-08-11 blanchet 2013-08-11 made (hopefully temporary) hack more robust
2013-08-11 blanchet 2013-08-11 added warning
2013-08-11 blanchet 2013-08-11 gracefully handle one more error condition
2013-08-11 blanchet 2013-08-11 gracefully fail to define polymorphic (co)datatypes in local context