| #
087ba697 |
|
05-Oct-2016 |
fleury <Mathias.Fleury@mpi-inf.mpg.de> |
tuned proof -- much faster
|
| #
14001a0d |
|
22-Jul-2016 |
wenzelm <none@none> |
tuned proofs -- avoid unstructured calculation;
|
| #
66281660 |
|
26-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
a2bc0021 |
|
25-Apr-2016 |
wenzelm <none@none> |
eliminated old 'def';
tuned comments;
|
| #
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
| #
be9ace2b |
|
09-Nov-2015 |
wenzelm <none@none> |
qualifier is mandatory by default;
|
| #
372a4c7a |
|
31-Aug-2015 |
wenzelm <none@none> |
proper qualified naming;
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
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
|
| #
8f53ef93 |
|
06-Mar-2014 |
blanchet <none@none> |
renamed 'map_pair' to 'map_prod'
|
| #
433b1b70 |
|
06-Mar-2014 |
blanchet <none@none> |
renamed 'map_sum' to 'sum_map'
|
| #
447c00c8 |
|
13-Feb-2014 |
blanchet <none@none> |
merged 'Option.map' and 'Option.map_option'
|
| #
63970edd |
|
12-Feb-2014 |
blanchet <none@none> |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
| #
adfa85c2 |
|
22-Jan-2014 |
blanchet <none@none> |
whitespace tuning
|
| #
1bfa84bf |
|
16-Jan-2014 |
blanchet <none@none> |
get rid of 'rel' locale, to facilitate inclusion of 'Order_Relation_More_FP' into 'Order_Relation'
|
| #
0c8751df |
|
10-Jan-2014 |
traytel <none@none> |
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
|