src/HOL/BNF_FP_Base.thy
2014-03-07 blanchet 2014-03-07 balance tuples that represent curried functions
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-03-06 traytel 2014-03-06 rationalized imports
2014-03-06 blanchet 2014-03-06 renamed 'map_pair' to 'map_prod'
2014-03-06 blanchet 2014-03-06 renamed 'map_sum' to 'sum_map'
2014-03-06 traytel 2014-03-06 more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms
2014-03-04 blanchet 2014-03-04 simplify sets in BNF composition
2014-03-03 blanchet 2014-03-03 make 'typedef' optional, depending on size of original type
2014-02-28 traytel 2014-02-28 load Metis a little later
2014-02-25 traytel 2014-02-25 joint work with blanchet: intermediate typedef for the input to fp-operations
2014-02-23 blanchet 2014-02-23 improved accounting for dead variables when naming set functions (refines d71c2737ee21)
2014-02-23 blanchet 2014-02-23 more precise error message
2014-02-21 blanchet 2014-02-21 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
2014-02-19 blanchet 2014-02-19 moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
2014-02-18 blanchet 2014-02-18 prepare two-stage 'primrec' setup
2014-02-17 blanchet 2014-02-17 tuning * * * moved 'primrec' up to displace the few remaining uses of 'old_primrec'
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-01-20 blanchet 2014-01-20 move BNF_LFP up the dependency chain
2014-01-20 blanchet 2014-01-20 removed dependency of BNF package on Nitpick
2014-01-20 blanchet 2014-01-20 tuning
2014-01-20 blanchet 2014-01-20 made BNF compile after move to HOL
2014-01-20 blanchet 2014-01-20 tuned comments
2014-01-20 blanchet 2014-01-20 moved BNF files to 'HOL'