src/HOL/Cardinals/Cardinal_Order_Relation.thy
2017-08-18 wenzelm 2017-08-18 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2016-05-26 wenzelm 2016-05-26 isabelle update_cartouches -c -t;
2016-05-13 wenzelm 2016-05-13 eliminated use of empty "assms";
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2015-12-28 wenzelm 2015-12-28 prefer symbols for "Union", "Inter";
2015-12-27 wenzelm 2015-12-27 discontinued ASCII replacement syntax <*>;
2015-06-26 wenzelm 2015-06-26 tuned whitespace;
2014-12-21 wenzelm 2014-12-21 recovered metis proof after 115965966e15 (Odd clash of type variables!?);
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-18 traytel 2014-03-18 tuned proofs; removed duplicated facts
2014-03-07 traytel 2014-03-07 made natLe{q,ss} constants (yields smaller terms in composition)
2014-01-30 traytel 2014-01-30 extended cardinals library
2014-01-22 blanchet 2014-01-22 whitespace tuning
2014-01-20 blanchet 2014-01-20 renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test)
2014-01-20 blanchet 2014-01-20 renamed '_FP' files to 'BNF_' files
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-11 haftmann 2014-01-11 shot in the dark to make LaTeX happy again
2014-01-10 traytel 2014-01-10 basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
2013-12-17 traytel 2013-12-17 reduced cardinals dependencies of (co)datatypes
2013-11-25 traytel 2013-11-25 eliminated dependence of Cardinals_FP on Set_Intervals, more precise imports
2013-11-25 traytel 2013-11-25 eliminated dependence of BNF on Infinite_Set by moving 3 theorems from the latter to Main
2013-11-18 blanchet 2013-11-18 compile
2013-11-18 blanchet 2013-11-18 moved theorems out of LFP
2013-11-18 blanchet 2013-11-18 started three-way split of 'HOL-Cardinals'
2013-07-07 traytel 2013-07-07 Func -> Func_option, Ffunc -> Func (avoids dependence of codatatypes on the option type)
2013-07-05 traytel 2013-07-05 tuned spelling
2013-04-24 traytel 2013-04-24 optimized proofs
2012-09-12 blanchet 2012-09-12 renamed "Ordinals_and_Cardinals" to "Cardinals"