# HG changeset patch # User blanchet # Date 1604663978 -3600 # Node ID 729d45c7ff3383f4346891283efa5b5573792108 # Parent 1d0ae7e578a0c6859881943509b77d163f91e5c2 undid renaming accident diff -r 1d0ae7e578a0 -r 729d45c7ff33 src/HOL/Data_Structures/Binomial_Heap.thy --- 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\[]" 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