History log of /seL4-l4v-10.1.1/isabelle/src/HOL/Data_Structures/Isin2.thy
Revision Date Author Comments
# 5fde6c5f 11-Jun-2018 nipkow <none@none>

tuned order of arguments
# 99ffcf66 07-Apr-2018 nipkow <none@none>

moved and renamed lemmas
# 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"
# 4fd0cb28 07-Jul-2016 nipkow <none@none>

got rid of class cmp; added height-size proofs by Daniel Stuewe
# 35f7dccd 23-Feb-2016 nipkow <none@none>

more canonical names
# 263870f4 17-Nov-2015 nipkow <none@none>

removed lemmas that were only needed for old version of isin.
# c4d4aaf9 22-Sep-2015 nipkow <none@none>

unified isin-proofs
# 6fc2a136 22-Sep-2015 nipkow <none@none>

added red black trees

--HG--
extra : rebase_source : 28e43c87d5eb14090fa401987d8131c2067f6ab7