src/HOL/Cardinals/Ordinal_Arithmetic.thy
2016-10-05 fleury 2016-10-05 tuned proof -- much faster
2016-07-22 wenzelm 2016-07-22 tuned proofs -- avoid unstructured calculation;
2016-05-26 wenzelm 2016-05-26 isabelle update_cartouches -c -t;
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-02-23 nipkow 2016-02-23 more canonical names
2015-11-09 wenzelm 2015-11-09 qualifier is mandatory by default;
2015-08-31 wenzelm 2015-08-31 proper qualified naming;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-01 blanchet 2014-09-01 renamed '(BNF_)Constructions_on_Wellorders' to '(BNF_)Wellorder_Constructions'
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-02-14 blanchet 2014-02-14 merged 'Option.map' and 'Option.map_option'
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-01-22 blanchet 2014-01-22 whitespace tuning
2014-01-16 blanchet 2014-01-16 get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
2014-01-10 traytel 2014-01-10 basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)