| #
97bce028 |
|
13-Jun-2018 |
nipkow <none@none> |
qualify interpretations to avoid clashes
|
| #
83ad70a0 |
|
12-Jun-2018 |
nipkow <none@none> |
more abstract naming
|
| #
d6960dd1 |
|
11-Jun-2018 |
nipkow <none@none> |
proved avl for map (finally); tuned
|
| #
5fde6c5f |
|
11-Jun-2018 |
nipkow <none@none> |
tuned order of arguments
|
| #
ccc2bd69 |
|
01-Jun-2018 |
nipkow <none@none> |
added lemma
|
| #
ccc9ea3f |
|
29-May-2018 |
nipkow <none@none> |
slicker proof
|
| #
87aaaee7 |
|
23-Apr-2018 |
nipkow <none@none> |
del_max -> split_max
|
| #
99ffcf66 |
|
07-Apr-2018 |
nipkow <none@none> |
moved and renamed lemmas
|
| #
83292697 |
|
08-Apr-2018 |
nipkow <none@none> |
better name; added binary operations
--HG--
rename : src/HOL/Data_Structures/Set_by_Ordered.thy => src/HOL/Data_Structures/Set_Interfaces.thy
|
| #
5589896c |
|
12-Jan-2018 |
wenzelm <none@none> |
isabelle update_cartouches -c;
|
| #
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
| #
4fd0cb28 |
|
07-Jul-2016 |
nipkow <none@none> |
got rid of class cmp; added height-size proofs by Daniel Stuewe
|
| #
315f2fe3 |
|
06-Mar-2016 |
nipkow <none@none> |
tuned
|
| #
1964277f |
|
14-Nov-2015 |
nipkow <none@none> |
tuned white space
|
| #
883026ef |
|
12-Nov-2015 |
nipkow <none@none> |
tuned
--HG--
extra : rebase_source : a4141890da30009139e365e16c6b15d7a31f8938
|
| #
16e9bbf5 |
|
05-Nov-2015 |
nipkow <none@none> |
tuned
|
| #
efd623c1 |
|
05-Nov-2015 |
nipkow <none@none> |
Convertd to 3-way comparisons
|
| #
1bc192be |
|
13-Oct-2015 |
nipkow <none@none> |
added invar empty
|
| #
c87cf195 |
|
23-Sep-2015 |
nipkow <none@none> |
added AVL and lookup function
|