--- a/src/HOL/Data_Structures/Binomial_Heap.thy Fri Nov 06 12:48:31 2020 +0100
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy Fri Nov 06 12:59:38 2020 +0100
@@ -326,7 +326,7 @@
using assms
by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto split: prod.splits if_splits)
-lemma seT_get_min_rest:
+lemma set_get_min_rest:
assumes "get_min_rest ts = (t', ts')"
assumes "ts\<noteq>[]"
shows "set ts = Set.insert t' (set ts')"
@@ -345,7 +345,7 @@
case (2 t v va)
then show ?case
apply (clarsimp split: prod.splits if_splits)
- apply (drule seT_get_min_rest; fastforce)
+ apply (drule set_get_min_rest; fastforce)
done
qed auto
thus "invar_btree t'" and "invar_bheap ts'" by auto