| Mon, 27 Jun 2022 15:54:18 +0200 |
traytel |
strict bounds for BNFs (by Jan van Brügge)
|
file |
diff |
annotate
|
| Sun, 09 Aug 2020 15:18:19 +0100 |
paulson |
adjustments for fewer WO assumptions
|
file |
diff |
annotate
|
| Thu, 24 Jan 2019 14:44:52 +0000 |
paulson |
the theory of Equipollence, and moving Fpow from Cardinals into Main
|
file |
diff |
annotate
|
| Tue, 22 Jan 2019 12:00:16 +0000 |
paulson |
renamings and new material
|
file |
diff |
annotate
|
| Thu, 19 Jul 2018 09:10:22 +0100 |
traytel |
normalize imports
|
file |
diff |
annotate
|
| Thu, 15 Feb 2018 12:11:00 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Fri, 18 Aug 2017 20:47:47 +0200 |
wenzelm |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
file |
diff |
annotate
|
| Thu, 26 May 2016 17:51:22 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Fri, 13 May 2016 20:24:10 +0200 |
wenzelm |
eliminated use of empty "assms";
|
file |
diff |
annotate
|
| Mon, 25 Apr 2016 16:09:26 +0200 |
wenzelm |
eliminated old 'def';
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 17:43:30 +0100 |
wenzelm |
prefer symbols for "Union", "Inter";
|
file |
diff |
annotate
|
| Sun, 27 Dec 2015 22:07:17 +0100 |
wenzelm |
discontinued ASCII replacement syntax <*>;
|
file |
diff |
annotate
|
| Fri, 26 Jun 2015 10:20:33 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sun, 21 Dec 2014 15:59:19 +0100 |
wenzelm |
recovered metis proof after 115965966e15 (Odd clash of type variables!?);
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:34:39 +0200 |
blanchet |
renamed '(BNF_)Constructions_on_Wellorders' to '(BNF_)Wellorder_Constructions'
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 11:47:59 +0100 |
traytel |
tuned proofs; removed duplicated facts
|
file |
diff |
annotate
|
| Fri, 07 Mar 2014 23:10:27 +0100 |
traytel |
made natLe{q,ss} constants (yields smaller terms in composition)
|
file |
diff |
annotate
|
| Thu, 30 Jan 2014 12:28:05 +0100 |
traytel |
extended cardinals library
|
file |
diff |
annotate
|
| Wed, 22 Jan 2014 10:13:40 +0100 |
blanchet |
whitespace tuning
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 22:24:48 +0100 |
blanchet |
renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test)
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:55 +0100 |
blanchet |
renamed '_FP' files to 'BNF_' files
|
file |
diff |
annotate
|
| 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'
|
file |
diff |
annotate
|
| Sat, 11 Jan 2014 21:03:11 +0100 |
haftmann |
shot in the dark to make LaTeX happy again
|
file |
diff |
annotate
|
| Fri, 10 Jan 2014 17:24:52 +0100 |
traytel |
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
|
file |
diff |
annotate
|
| Tue, 17 Dec 2013 15:56:57 +0100 |
traytel |
reduced cardinals dependencies of (co)datatypes
|
file |
diff |
annotate
|
| Mon, 25 Nov 2013 13:48:00 +0100 |
traytel |
eliminated dependence of Cardinals_FP on Set_Intervals, more precise imports
|
file |
diff |
annotate
|
| 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
|
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
|
| 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
|
| Fri, 05 Jul 2013 18:10:07 +0200 |
traytel |
tuned spelling
|
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
|