src/HOL/Cardinals/Cardinal_Arithmetic.thy
2015-12-27 wenzelm 2015-12-27 discontinued ASCII replacement syntax <*>;
2015-06-26 wenzelm 2015-06-26 tuned whitespace;
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-03 blanchet 2014-03-03 optimize cardinal bounds involving natLeq (omega)
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 rationalized dependencies
2014-01-20 blanchet 2014-01-20 tuning
2014-01-20 blanchet 2014-01-20 compile
2014-01-20 blanchet 2014-01-20 renamed '_FP' files to 'BNF_' files
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-18 blanchet 2013-11-18 compile
2013-11-18 blanchet 2013-11-18 no need for 3-way split with GFP for a handful of theorems
2013-11-18 blanchet 2013-11-18 moved theorems out of LFP
2013-11-18 blanchet 2013-11-18 split 'Cardinal_Arithmetic' 3-way
2013-11-18 blanchet 2013-11-18 started three-way split of 'HOL-Cardinals'
2013-07-11 traytel 2013-07-11 some new lemmas towards getting rid of in_bd BNF property; tuned
2013-07-07 traytel 2013-07-07 Func -> Func_option, Ffunc -> Func (avoids dependence of codatatypes on the option type)
2013-04-29 traytel 2013-04-29 tuned operator precedence
2013-04-25 traytel 2013-04-25 removed unnecessary assumptions in some theorems about cardinal exponentiation
2012-09-12 blanchet 2012-09-12 renamed "Ordinals_and_Cardinals" to "Cardinals"