src/HOL/Cardinals/Cardinal_Order_Relation.thy
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"