# HG changeset patch
# User wenzelm
# Date 1711393021 -3600
# Node ID 917a9856bb3a82f406fad2ef8f3a6e42ab74841c
# Parent  c2cca97a57978a6b9579cc2070984cbb62ba34db# Parent  36e33d227bf0b815847467201c6be8658421c446
merged

diff -r 36e33d227bf0 -r 917a9856bb3a src/HOL/Data_Structures/Leftist_Heap_List.thy
--- 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" |