src/HOL/Imperative_HOL/Heap_Monad.thy

--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Sun May 22 22:22:25 2011 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon May 23 10:58:21 2011 +0200
@@ -425,6 +425,10 @@
     by (simp only: Heap_ord_def Heap_lub_def)
 qed
 
+declaration {* Partial_Function.init "heap" @{term heap.fixp_fun}
+  @{term heap.mono_body} @{thm heap.fixp_rule_uc} *}
+
+
 abbreviation "mono_Heap \<equiv> monotone (fun_ord Heap_ord) Heap_ord"
 
 lemma Heap_ordI: