| Fri, 10 Jan 2014 17:24:52 +0100 |
traytel |
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
|
file |
diff |
annotate
|
| Wed, 20 Nov 2013 23:14:06 +0100 |
blanchet |
effectively reverted d25fc4c0ff62, to avoid quasi-cyclic dependencies with HOL-Cardinals and minimize BNF dependencies
|
file |
diff |
annotate
|
| Mon, 18 Nov 2013 18:04:45 +0100 |
blanchet |
compile
|
file |
diff |
annotate
|
| Mon, 18 Nov 2013 18:04:45 +0100 |
blanchet |
moved theorems out of LFP
|
file |
diff |
annotate
|
| Mon, 18 Nov 2013 18:04:44 +0100 |
blanchet |
started three-way split of 'HOL-Cardinals'
|
file |
diff |
annotate
|
| Tue, 28 May 2013 16:56:49 +0200 |
popescua |
fixed broken Cardinals and BNF due to Order_Union
|
file |
diff |
annotate
|
| Fri, 24 May 2013 19:09:56 +0200 |
popescua |
fixed files broken due to Zorn changes (cf. 59e5dd7b8f9a)
|
file |
diff |
annotate
|
| Wed, 24 Apr 2013 16:43:19 +0200 |
traytel |
optimized proofs
|
file |
diff |
annotate
|
| Wed, 12 Sep 2012 05:29:21 +0200 |
blanchet |
renamed "Ordinals_and_Cardinals" to "Cardinals"
|
file |
diff |
annotate
| base
|