Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned
authornipkow
Mon, 25 Mar 2024 17:55:02 +0100
changeset 79984 c2cca97a5797
parent 79983 ee45e96eb7c5
child 79989 917a9856bb3a
child 79996 4f803ae64781
child 80036 a594d22e69d6
tuned
src/HOL/Data_Structures/Leftist_Heap_List.thy file | annotate | diff | comparison | revisions 
--- 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" |
isabelle