# 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 \<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" |