src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 42949 618adb3584e5
parent 41413 64cd30d6b0b8
child 43080 73a1d6a7ef1d
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Sun May 22 22:22:25 2011 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon May 23 10:58:21 2011 +0200
     1.3 @@ -425,6 +425,10 @@
     1.4      by (simp only: Heap_ord_def Heap_lub_def)
     1.5  qed
     1.6  
     1.7 +declaration {* Partial_Function.init "heap" @{term heap.fixp_fun}
     1.8 +  @{term heap.mono_body} @{thm heap.fixp_rule_uc} *}
     1.9 +
    1.10 +
    1.11  abbreviation "mono_Heap \<equiv> monotone (fun_ord Heap_ord) Heap_ord"
    1.12  
    1.13  lemma Heap_ordI: