| Mon, 18 Nov 2013 18:04:45 +0100 |
blanchet |
compile
|
file |
diff |
annotate
|
| Mon, 18 Nov 2013 18:04:45 +0100 |
blanchet |
no need for 3-way split with GFP for a handful of theorems
|
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 |
split 'Cardinal_Arithmetic' 3-way
|
file |
diff |
annotate
|
| Mon, 18 Nov 2013 18:04:44 +0100 |
blanchet |
started three-way split of 'HOL-Cardinals'
|
file |
diff |
annotate
|
| Thu, 11 Jul 2013 11:16:23 +0200 |
traytel |
some new lemmas towards getting rid of in_bd BNF property; tuned
|
file |
diff |
annotate
|
| Sun, 07 Jul 2013 10:24:00 +0200 |
traytel |
Func -> Func_option, Ffunc -> Func (avoids dependence of codatatypes on the option type)
|
file |
diff |
annotate
|
| Mon, 29 Apr 2013 10:03:35 +0200 |
traytel |
tuned operator precedence
|
file |
diff |
annotate
|
| Thu, 25 Apr 2013 19:18:20 +0200 |
traytel |
removed unnecessary assumptions in some theorems about cardinal exponentiation
|
file |
diff |
annotate
|
| Wed, 12 Sep 2012 05:29:21 +0200 |
blanchet |
renamed "Ordinals_and_Cardinals" to "Cardinals"
|
file |
diff |
annotate
| base
|