| changeset 61566 | c3d6e570ccef |
| parent 59104 | a14475f044b2 |
| child 61605 | 1bf7b186542e |
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Nov 04 08:13:49 2015 +0100 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Nov 04 08:13:52 2015 +0100 @@ -405,7 +405,7 @@ qed interpretation heap!: partial_function_definitions Heap_ord Heap_lub - where "Heap_lub {} \<equiv> Heap Map.empty" + rewrites "Heap_lub {} \<equiv> Heap Map.empty" by (fact heap_interpretation)(simp add: Heap_lub_empty) lemma heap_step_admissible: