# HG changeset patch # User nipkow # Date 1711385702 -3600 # Node ID c2cca97a57978a6b9579cc2070984cbb62ba34db # Parent ee45e96eb7c5c1c551dbb4237eaf6ef4f9481aaf tuned diff -r ee45e96eb7c5 -r c2cca97a5797 src/HOL/Data_Structures/Leftist_Heap_List.thy --- a/src/HOL/Data_Structures/Leftist_Heap_List.thy Mon Mar 25 15:11:48 2024 +0100 +++ b/src/HOL/Data_Structures/Leftist_Heap_List.thy Mon Mar 25 17:55:02 2024 +0100 @@ -66,6 +66,8 @@ subsubsection \Running time\ +text \Not defined automatically because we only count the time for @{const merge}.\ + fun T_merge_adj :: "('a::ord) lheap list \ nat" where "T_merge_adj [] = 0" | "T_merge_adj [t] = 0" |