#
97bce028 |
|
13-Jun-2018 |
nipkow <none@none> |
qualify interpretations to avoid clashes
|
#
83ad70a0 |
|
12-Jun-2018 |
nipkow <none@none> |
more abstract naming
|
#
93bea17d |
|
21-Apr-2018 |
nipkow <none@none> |
del_min -> split_min
|
#
116c2e29 |
|
08-Apr-2018 |
nipkow <none@none> |
more name tuning --HG-- rename : src/HOL/Data_Structures/Map_by_Ordered.thy => src/HOL/Data_Structures/Map_Specs.thy rename : src/HOL/Data_Structures/Set_Interfaces.thy => src/HOL/Data_Structures/Set_Specs.thy
|
#
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
|
#
0a3fa2e8 |
|
23-Mar-2018 |
nipkow <none@none> |
eliminated "elems"
|
#
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
|
#
1964277f |
|
14-Nov-2015 |
nipkow <none@none> |
tuned white space
|
#
4b01b32c |
|
13-Nov-2015 |
nipkow <none@none> |
unnecessary precondition
|
#
883026ef |
|
12-Nov-2015 |
nipkow <none@none> |
tuned --HG-- extra : rebase_source : a4141890da30009139e365e16c6b15d7a31f8938
|
#
f42b3257 |
|
11-Nov-2015 |
nipkow <none@none> |
no CRLF
|
#
16e9bbf5 |
|
05-Nov-2015 |
nipkow <none@none> |
tuned
|
#
efd623c1 |
|
05-Nov-2015 |
nipkow <none@none> |
Convertd to 3-way comparisons
|
#
d79f30eb |
|
02-Nov-2015 |
nipkow <none@none> |
tuned names and optimized comparison order
|
#
1bc192be |
|
13-Oct-2015 |
nipkow <none@none> |
added invar empty
|
#
72b4772b |
|
23-Sep-2015 |
nipkow <none@none> |
tuned
|
#
c4d4aaf9 |
|
22-Sep-2015 |
nipkow <none@none> |
unified isin-proofs
|
#
042abe0c |
|
21-Sep-2015 |
nipkow <none@none> |
New subdirectory for functional data structures
|