# HG changeset patch
# User Peter Lammich
# Date 1606405880 0
# Node ID 35d1fc20df224532fb4b9d76644dcd4aa0da1b28
# Parent  fabd29c73098bbd91870ca15883fcdf7c9f12858
renaming

diff -r fabd29c73098 -r 35d1fc20df22 src/HOL/Data_Structures/Binomial_Heap.thy
--- a/src/HOL/Data_Structures/Binomial_Heap.thy	Wed Nov 25 21:13:45 2020 +0100
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Thu Nov 26 15:51:20 2020 +0000
@@ -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)