Summary
- merged
- tuned names
- tuned back: cost Empty := 1 unformaly and make cost Del and exec Del agree in their structure
The file was modified | thys/Splay_Tree/Splay_Tree.thy (diff) |
The file was modified | thys/Amortized_Complexity/Amortized_Examples.thy (diff) |