src/HOL/Cardinals/Cardinal_Order_Relation.thy
Tue, 18 Mar 2014 11:47:59 +0100 traytel tuned proofs; removed duplicated facts
Fri, 07 Mar 2014 23:10:27 +0100 traytel made natLe{q,ss} constants (yields smaller terms in composition)
Thu, 30 Jan 2014 12:28:05 +0100 traytel extended cardinals library
Wed, 22 Jan 2014 10:13:40 +0100 blanchet whitespace tuning
Mon, 20 Jan 2014 22:24:48 +0100 blanchet renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test)
Mon, 20 Jan 2014 18:24:55 +0100 blanchet renamed '_FP' files to 'BNF_' files
Thu, 16 Jan 2014 20:52:54 +0100 blanchet get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
Sat, 11 Jan 2014 21:03:11 +0100 haftmann shot in the dark to make LaTeX happy again
Fri, 10 Jan 2014 17:24:52 +0100 traytel basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
Tue, 17 Dec 2013 15:56:57 +0100 traytel reduced cardinals dependencies of (co)datatypes
Mon, 25 Nov 2013 13:48:00 +0100 traytel eliminated dependence of Cardinals_FP on Set_Intervals, more precise imports
Mon, 25 Nov 2013 10:14:29 +0100 traytel eliminated dependence of BNF on Infinite_Set by moving 3 theorems from the latter to Main
Mon, 18 Nov 2013 18:04:45 +0100 blanchet compile
Mon, 18 Nov 2013 18:04:45 +0100 blanchet moved theorems out of LFP
Mon, 18 Nov 2013 18:04:44 +0100 blanchet started three-way split of 'HOL-Cardinals'
Sun, 07 Jul 2013 10:24:00 +0200 traytel Func -> Func_option, Ffunc -> Func (avoids dependence of codatatypes on the option type)
Fri, 05 Jul 2013 18:10:07 +0200 traytel tuned spelling
Wed, 24 Apr 2013 16:43:19 +0200 traytel optimized proofs
Wed, 12 Sep 2012 05:29:21 +0200 blanchet renamed "Ordinals_and_Cardinals" to "Cardinals"
less more (0) tip