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
Thu, 11 Jul 2019 18:37:52 +0200
changeset 70363 6d96ee03b62e
parent 70362 421727c19b23
child 70364 b2bedb022a75
child 70365 4df0628e8545
tuned
src/HOL/Data_Structures/Leftist_Heap.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Data_Structures/Leftist_Heap.thy	Thu Jul 04 14:20:47 2019 +0200
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Thu Jul 11 18:37:52 2019 +0200
@@ -46,7 +46,6 @@
 
 text \<open>For function \<open>merge\<close>:\<close>
 unbundle pattern_aliases
-declare size_prod_measure[measure_function]
 
 fun merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
 "merge Leaf t2 = t2" |
isabelle