diff -r ad0cefe1e9a9 -r ff561d9cb661 src/HOL/Data_Structures/Leftist_Heap.thy
--- a/src/HOL/Data_Structures/Leftist_Heap.thy	Wed Aug 30 22:51:44 2017 +0100
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Thu Aug 31 08:39:42 2017 +0200
@@ -136,12 +136,14 @@
 lemma heap_del_min: "heap t \<Longrightarrow> heap(del_min t)"
 by(cases t)(auto simp add: heap_merge simp del: merge.simps)
 
+text \<open>Last step of functional correctness proof: combine all the above lemmas
+to show that leftist heaps satisfy the specification of priority queues with merge.\<close>
 
-interpretation lheap: Priority_Queue
+interpretation lheap: Priority_Queue_Merge
 where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
 and insert = insert and del_min = del_min
-and get_min = get_min and invar = "\<lambda>h. heap h \<and> ltree h"
-and mset = mset_tree
+and get_min = get_min and merge = merge
+and invar = "\<lambda>h. heap h \<and> ltree h" and mset = mset_tree
 proof(standard, goal_cases)
   case 1 show ?case by simp
 next
@@ -158,6 +160,10 @@
   case 7 thus ?case by(simp add: heap_insert ltree_insert)
 next
   case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
+next
+  case 9 thus ?case by (simp add: mset_merge)
+next
+  case 10 thus ?case by (simp add: heap_merge ltree_merge)
 qed