Summary
- updated proof and split it up into standard part and framework instantiation
- added interpretation of spec locale
The file was added | thys/Amortized_Complexity/Skew_Heap_Analysis2.thy |
The file was modified | thys/Amortized_Complexity/ROOT (diff) |
The file was modified | thys/Amortized_Complexity/Skew_Heap_Analysis.thy (diff) |
The file was modified | thys/Skew_Heap/Skew_Heap.thy (diff) |