src/HOL/BNF/Tools/bnf_fp_util.ML
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