src/HOL/Import/HOL_Light_Maps.thy
2015-06-12 haftmann 2015-06-12 uniform _ div _ as infix syntax for ring division
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-23 haftmann 2014-10-23 explicit definition restores HOL Light import after cb9d84d3e7f2
2014-03-24 wenzelm 2014-03-24 formal check of user input, avoiding direct references of interal names;
2014-02-16 blanchet 2014-02-16 folded 'list_all2' with the relator generated by 'datatype_new'
2014-02-14 blanchet 2014-02-14 merged 'Option.map' and 'Option.map_option'
2014-02-12 blanchet 2014-02-12 adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-02-12 blanchet 2014-02-12 adapted theories to '{case,rec}_{list,option}' names
2014-02-12 blanchet 2014-02-12 se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors * * * cleaner simp/iff sets
2013-12-25 haftmann 2013-12-25 prefer more canonical names for lemmas on min/max
2012-04-04 Cezary Kaliszyk 2012-04-04 HOL/Import more precise map types
2012-04-01 Cezary Kaliszyk 2012-04-01 Modernized HOL-Import for HOL Light