# HG changeset patch
# User nipkow
# Date 1485931931 -3600
# Node ID 44108f90e54e6cd7bdd9b70e117675b5904c2a78
# Parent  9f579a18c136e76c5019300252c0efc43faa3419# Parent  a7597a58d7d364490fa8b26967ba1f54269a4490
merged

diff -r 9f579a18c136 -r 44108f90e54e src/HOL/Data_Structures/Leftist_Heap.thy
--- a/src/HOL/Data_Structures/Leftist_Heap.thy	Tue Jan 31 17:36:51 2017 +0100
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Wed Feb 01 07:52:11 2017 +0100
@@ -82,19 +82,19 @@
 subsection "Functional Correctness"
 
 locale Priority_Queue =
-fixes empty :: "'pq"
-and insert :: "'a::linorder \<Rightarrow> 'pq \<Rightarrow> 'pq"
-and get_min :: "'pq \<Rightarrow> 'a"
-and del_min :: "'pq \<Rightarrow> 'pq"
-and invar :: "'pq \<Rightarrow> bool"
-and mset :: "'pq \<Rightarrow> 'a multiset"
+fixes empty :: "'q"
+and insert :: "'a::linorder \<Rightarrow> 'q \<Rightarrow> 'q"
+and get_min :: "'q \<Rightarrow> 'a"
+and del_min :: "'q \<Rightarrow> 'q"
+and invar :: "'q \<Rightarrow> bool"
+and mset :: "'q \<Rightarrow> 'a multiset"
 assumes mset_empty: "mset empty = {#}"
-and mset_insert: "invar pq \<Longrightarrow> mset (insert x pq) = mset pq + {#x#}"
-and mset_del_min: "invar pq \<Longrightarrow> mset (del_min pq) = mset pq - {#get_min pq#}"
-and get_min: "invar pq \<Longrightarrow> pq \<noteq> empty \<Longrightarrow>
-   get_min pq \<in> set_mset(mset pq) \<and> (\<forall>x \<in># mset pq. get_min pq \<le> x)"
-and invar_insert: "invar pq \<Longrightarrow> invar (insert x pq)"
-and invar_del_min: "invar pq \<Longrightarrow> invar (del_min pq)"
+and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
+and mset_del_min: "invar q \<Longrightarrow> mset (del_min q) = mset q - {#get_min q#}"
+and get_min: "invar q \<Longrightarrow> q \<noteq> empty \<Longrightarrow>
+   get_min q \<in> set_mset(mset q) \<and> (\<forall>x \<in># mset q. get_min q \<le> x)"
+and invar_insert: "invar q \<Longrightarrow> invar (insert x q)"
+and invar_del_min: "invar q \<Longrightarrow> invar (del_min q)"
 
 
 lemma mset_meld: "mset_tree (meld h1 h2) = mset_tree h1 + mset_tree h2"