Changes

Summary

moved and renamed lemmas
Added binary set operations with join-based implementation
more name tuning
better name; added binary operations

Changeset 67967:5a4280946a25 by nipkow: moved and renamed lemmas
The file was modified	`src/HOL/Data_Structures/AA_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/AVL_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Isin2.thy` (diff)
The file was modified	`src/HOL/Data_Structures/RBT_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Set2_BST2_Join.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Tree2.thy` (diff)
Changeset 67966:f13796496e82 by nipkow: Added binary set operations with join-based implementation
The file was added	`src/HOL/Data_Structures/Set2_BST2_Join.thy`
The file was added	`src/HOL/Data_Structures/Set2_BST2_Join_RBT.thy`
The file was added	`src/HOL/Data_Structures/Set2_BST_Join.thy`
The file was modified	`src/HOL/Data_Structures/document/root.bib` (diff)
The file was modified	`src/HOL/Data_Structures/document/root.tex` (diff)
Changeset 67965:aaa31cd0caef by nipkow: more name tuning
The file was added	`src/HOL/Data_Structures/Map_Specs.thy`
The file was added	`src/HOL/Data_Structures/Set_Specs.thy`
The file was modified	`src/HOL/Data_Structures/Brother12_Map.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Brother12_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Isin2.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Lookup2.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Tree234_Map.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Tree234_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Tree23_Map.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Tree23_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Tree_Map.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Tree_Set.thy` (diff)
The file was modified	`src/HOL/ROOT` (diff)
The file was removed	`src/HOL/Data_Structures/Map_by_Ordered.thy`
The file was removed	`src/HOL/Data_Structures/Set_Interfaces.thy`
Changeset 67964:08cc5ab18c84 by nipkow: better name; added binary operations
The file was added	`src/HOL/Data_Structures/Set_Interfaces.thy`
The file was modified	`src/HOL/Data_Structures/AVL_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Brother12_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Isin2.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Tree234_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Tree23_Set.thy` (diff)
The file was modified	`src/HOL/Data_Structures/Tree_Set.thy` (diff)
The file was removed	`src/HOL/Data_Structures/Set_by_Ordered.thy`