src/HOL/BNF/Tools/bnf_fp_util.ML
2014-01-03 blanchet 2014-01-03 instantiate schematics as projections to avoid HOU trouble
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-09-18 blanchet 2013-09-18 use singular to avoid confusion
2013-09-12 traytel 2013-09-12 conceal internal bindings
2013-08-29 blanchet 2013-08-29 qualify generated constants uniformly
2013-08-29 blanchet 2013-08-29 rationalized bindings
2013-08-29 blanchet 2013-08-29 renamed an ML filed for consistency (low-level => ctor/dtor/xtor in name)
2013-08-28 blanchet 2013-08-28 natural component order
2013-08-28 blanchet 2013-08-28 better error message
2013-08-28 blanchet 2013-08-28 tuning
2013-08-26 traytel 2013-08-26 tuned
2013-08-26 traytel 2013-08-26 moved derivation of ctor_dtor_unfold to sugar (streamlines fp_result interface)
2013-08-26 blanchet 2013-08-26 export one more ML function, needed for primcorec
2013-08-22 traytel 2013-08-22 configuration option to control timing output for (co)datatypes
2013-08-22 traytel 2013-08-22 store theorem about composition of fold and map in fp_result
2013-08-20 traytel 2013-08-20 moved derivation of strong coinduction to sugar
2013-08-20 traytel 2013-08-20 simpler (forward) derivation of strong (up-to equality) coinduction properties
2013-08-16 blanchet 2013-08-16 tuning
2013-08-16 traytel 2013-08-16 tuned
2013-08-12 blanchet 2013-08-12 qualify more generated names with optional type name component
2013-08-12 blanchet 2013-08-12 reverted ill-advised naming scheme of 5a77edcdbe54
2013-08-11 blanchet 2013-08-11 made code more robust
2013-08-09 blanchet 2013-08-09 honor user type names if possible
2013-08-09 traytel 2013-08-09 tuned
2013-08-08 traytel 2013-08-08 theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map
2013-08-07 blanchet 2013-08-07 tuning
2013-08-02 traytel 2013-08-02 store relator induction in fp_result
2013-07-25 traytel 2013-07-25 transfer rule for {c,d}tor_{,un}fold
2013-07-15 traytel 2013-07-15 killed unused theorems
2013-07-03 traytel 2013-07-03 use long goal format in rel_induct theorem
2013-07-03 traytel 2013-07-03 share some code between codatatypes, datatypes and eventually prim(co)rec
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 tuning
2013-06-07 blanchet 2013-06-07 [mq]: tuning
2013-06-06 blanchet 2013-06-06 continuation of f461dca57c66
2013-06-06 blanchet 2013-06-06 tuned record field names to avoid confusion between low-level and high-level constants/theorems
2013-05-28 blanchet 2013-05-28 tuning -- avoided unreadable true/false all over the place for LFP/GFP
2013-05-16 blanchet 2013-05-16 tuning -- renamed '_from_' to '_of_' in Sledgehammer
2013-05-08 traytel 2013-05-08 relator induction for datatypes
2013-05-07 traytel 2013-05-07 got rid of the set based relator---use (binary) predicate based relator instead
2013-05-02 blanchet 2013-05-02 renamings
2013-05-02 blanchet 2013-05-02 code tuning
2013-05-02 blanchet 2013-05-02 signature tuning
2013-05-02 blanchet 2013-05-02 removed dead code
2013-05-02 blanchet 2013-05-02 tuned signature
2013-05-02 blanchet 2013-05-02 tuning names
2013-05-02 blanchet 2013-05-02 got rid of needless library function (find_minimum)
2013-05-02 blanchet 2013-05-02 rationalized data structure
2013-05-02 blanchet 2013-05-02 added and moved library functions (used in primrec code)
2013-05-01 blanchet 2013-05-01 renamed a few FP-related files, to make it clear that these are not the sum of LFP + GFP but rather shared basic libraries