merged
authorwenzelm
Mon, 25 Mar 2024 19:57:01 +0100
changeset 79989 917a9856bb3a
parent 79984 c2cca97a5797 (diff)
parent 79988 36e33d227bf0 (current diff)
child 79990 34420f5f2e92
merged
--- a/src/HOL/Data_Structures/Leftist_Heap_List.thy	Mon Mar 25 19:56:12 2024 +0100
+++ b/src/HOL/Data_Structures/Leftist_Heap_List.thy	Mon Mar 25 19:57:01 2024 +0100
@@ -66,6 +66,8 @@
 
 subsubsection \<open>Running time\<close>
 
+text \<open>Not defined automatically because we only count the time for @{const merge}.\<close>
+
 fun T_merge_adj :: "('a::ord) lheap list \<Rightarrow> nat" where
 "T_merge_adj [] = 0" |
 "T_merge_adj [t] = 0" |