Changes

Summary

Changeset 6309:c2b9c6421008 by max haslbeck _haslbema@in.tum.de_: merge
Changeset 6308:dd93e94abcb9 by max haslbeck _haslbema@in.tum.de_: added wf predicate to On_Off and adjusted coresponding theorems
The file was modified	`thys/Amortized_Complexity/BIT.thy` (diff)
The file was modified	`thys/Amortized_Complexity/BIT_2comp_on2.thy` (diff)
The file was modified	`thys/Amortized_Complexity/BIT_pairwise.thy` (diff)
The file was modified	`thys/Amortized_Complexity/Comb.thy` (diff)
The file was modified	`thys/Amortized_Complexity/Competitive_Analysis.thy` (diff)
The file was modified	`thys/Amortized_Complexity/List_Factoring.thy` (diff)
The file was modified	`thys/Amortized_Complexity/Move_to_Front.thy` (diff)
The file was modified	`thys/Amortized_Complexity/On_Off.thy` (diff)
The file was modified	`thys/Amortized_Complexity/Partial_Cost_Model.thy` (diff)
The file was modified	`thys/Amortized_Complexity/TS.thy` (diff)