Skip to content
Success

Changes

Summary

  1. updated proof and split it up into standard part and framework instantiation
  2. added interpretation of spec locale
Changeset 8214:83911294ce16 by nipkow:
updated proof and split it up into standard part and framework instantiation
The file was addedthys/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)
Changeset 8213:848b8e77b7ba by nipkow:
added interpretation of spec locale
The file was modified thys/Skew_Heap/Skew_Heap.thy (diff)