| #
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
| #
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
| #
f8080d0e |
|
01-Oct-2016 |
wenzelm <none@none> |
Isar proof of Schroeder_Bernstein without using Hilbert_Choice (and metis);
|
| #
a2bc0021 |
|
25-Apr-2016 |
wenzelm <none@none> |
eliminated old 'def';
tuned comments;
|
| #
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
| #
6688eecc |
|
17-Feb-2016 |
haftmann <none@none> |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
| #
7c503729 |
|
27-Dec-2015 |
wenzelm <none@none> |
discontinued ASCII replacement syntax <*>;
|
| #
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
6f0c89b5 |
|
26-Jun-2015 |
wenzelm <none@none> |
tuned whitespace;
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
4a9ed335 |
|
07-Oct-2014 |
wenzelm <none@none> |
more bibtex entries;
more antiquotations;
|
| #
e5d78e7e |
|
01-Sep-2014 |
blanchet <none@none> |
renamed '(BNF_)Constructions_on_Wellorders' to '(BNF_)Wellorder_Constructions'
--HG--
rename : src/HOL/BNF_Constructions_on_Wellorders.thy => src/HOL/BNF_Wellorder_Constructions.thy
rename : src/HOL/Cardinals/Constructions_on_Wellorders.thy => src/HOL/Cardinals/Wellorder_Constructions.thy
|
| #
31710314 |
|
18-Mar-2014 |
traytel <none@none> |
tuned proofs; removed duplicated facts
|
| #
462f1580 |
|
13-Mar-2014 |
haftmann <none@none> |
tuned proofs
|
| #
a1a57f60 |
|
13-Mar-2014 |
haftmann <none@none> |
tuned
|
| #
c82dbd75 |
|
07-Mar-2014 |
traytel <none@none> |
made natLe{q,ss} constants (yields smaller terms in composition)
|
| #
502da60f |
|
06-Mar-2014 |
traytel <none@none> |
rationalized imports
|
| #
bbeeaf3d |
|
28-Feb-2014 |
traytel <none@none> |
load Metis a little later
|
| #
6759b6d5 |
|
20-Feb-2014 |
traytel <none@none> |
less flex-flex pairs (thanks to Lars' statistics)
|
| #
480c3c64 |
|
31-Jan-2014 |
blanchet <none@none> |
tuning
|
| #
8eddf2ab |
|
22-Jan-2014 |
blanchet <none@none> |
whitespace tuning
|
| #
9d8fa6e6 |
|
20-Jan-2014 |
blanchet <none@none> |
renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test)
|
| #
5fd16e81 |
|
20-Jan-2014 |
blanchet <none@none> |
tuned comments
|
| #
47096efc |
|
20-Jan-2014 |
blanchet <none@none> |
renamed '_FP' files to 'BNF_' files
--HG--
rename : src/HOL/Cardinal_Arithmetic_FP.thy => src/HOL/BNF_Cardinal_Arithmetic.thy
rename : src/HOL/Cardinal_Order_Relation_FP.thy => src/HOL/BNF_Cardinal_Order_Relation.thy
rename : src/HOL/Constructions_on_Wellorders_FP.thy => src/HOL/BNF_Constructions_on_Wellorders.thy
rename : src/HOL/Wellorder_Embedding_FP.thy => src/HOL/BNF_Wellorder_Embedding.thy
rename : src/HOL/Wellorder_Relation_FP.thy => src/HOL/BNF_Wellorder_Relation.thy
|