# HG changeset patch
# User wenzelm
# Date 1606411926 -3600
# Node ID 178de0e275a12252e2d5fee87b3cedd6b453ad7f
# Parent  35d1fc20df224532fb4b9d76644dcd4aa0da1b28# Parent  01c9b303303611c549ca64e86f8f67f690ab37a5
merged

diff -r 01c9b3033036 -r 178de0e275a1 src/HOL/Data_Structures/Binomial_Heap.thy
--- a/src/HOL/Data_Structures/Binomial_Heap.thy	Thu Nov 26 18:05:24 2020 +0100
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Thu Nov 26 18:32:06 2020 +0100
@@ -110,7 +110,7 @@
 using assms
 by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp
 
-lemma invar_link_otree:
+lemma invar_otree_link:
   assumes "invar_otree t\<^sub>1"
   assumes "invar_otree t\<^sub>2"
   shows "invar_otree (link t\<^sub>1 t\<^sub>2)"
@@ -152,7 +152,7 @@
   assumes "invar_oheap ts"
   shows "invar_oheap (ins_tree t ts)"
 using assms
-by (induction t ts rule: ins_tree.induct) (auto simp: invar_link_otree)
+by (induction t ts rule: ins_tree.induct) (auto simp: invar_otree_link)
 
 lemma mset_heap_ins_tree[simp]:
   "mset_heap (ins_tree t ts) = mset_tree t + mset_heap ts"
@@ -252,7 +252,7 @@
   shows "invar_oheap (merge ts\<^sub>1 ts\<^sub>2)"
 using assms
 by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct)
-   (auto simp: invar_oheap_ins_tree invar_link_otree)
+   (auto simp: invar_oheap_ins_tree invar_otree_link)
 
 lemma invar_merge[simp]: "\<lbrakk> invar ts\<^sub>1; invar ts\<^sub>2 \<rbrakk> \<Longrightarrow> invar (merge ts\<^sub>1 ts\<^sub>2)"
 by (auto simp: invar_def invar_bheap_merge invar_oheap_merge)