src/HOL/BNF_Cardinal_Order_Relation.thy
2016-10-01 wenzelm 2016-10-01 Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-02-23 nipkow 2016-02-23 more canonical names
2016-02-17 haftmann 2016-02-17 prefer abbreviations for compound operators INFIMUM and SUPREMUM
2015-12-27 wenzelm 2015-12-27 discontinued ASCII replacement syntax <*>;
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-07-18 wenzelm 2015-07-18 isabelle update_cartouches;
2015-06-26 wenzelm 2015-06-26 tuned whitespace;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-07 wenzelm 2014-10-07 more bibtex entries; more antiquotations;
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-13 haftmann 2014-03-13 tuned proofs
2014-03-13 haftmann 2014-03-13 tuned
2014-03-07 traytel 2014-03-07 made natLe{q,ss} constants (yields smaller terms in composition)
2014-03-06 traytel 2014-03-06 rationalized imports
2014-02-28 traytel 2014-02-28 load Metis a little later
2014-02-20 traytel 2014-02-20 less flex-flex pairs (thanks to Lars' statistics)
2014-01-31 blanchet 2014-01-31 tuning
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 tuned comments
2014-01-20 blanchet 2014-01-20 renamed '_FP' files to 'BNF_' files