tuned
authornipkow
Thu Jul 11 18:37:52 2019 +0200 (11 days ago)
changeset 703636d96ee03b62e
parent 70362 421727c19b23
child 70364 b2bedb022a75
child 70365 4df0628e8545
tuned
src/HOL/Data_Structures/Leftist_Heap.thy
     1.1 --- a/src/HOL/Data_Structures/Leftist_Heap.thy	Thu Jul 04 14:20:47 2019 +0200
     1.2 +++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Thu Jul 11 18:37:52 2019 +0200
     1.3 @@ -46,7 +46,6 @@
     1.4  
     1.5  text \<open>For function \<open>merge\<close>:\<close>
     1.6  unbundle pattern_aliases
     1.7 -declare size_prod_measure[measure_function]
     1.8  
     1.9  fun merge :: "'a::ord lheap \<Rightarrow> 'a lheap \<Rightarrow> 'a lheap" where
    1.10  "merge Leaf t2 = t2" |