author | wenzelm |
Mon, 25 Mar 2024 19:57:01 +0100 | |
changeset 79989 | 917a9856bb3a |
parent 79984 | c2cca97a5797 (diff) |
parent 79988 | 36e33d227bf0 (current diff) |
child 79990 | 34420f5f2e92 |
--- 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" |