src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 43080 73a1d6a7ef1d
parent 42949 618adb3584e5
child 43324 2b47822868e4
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon May 30 17:55:34 2011 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon May 23 21:34:37 2011 +0200
     1.3 @@ -426,7 +426,7 @@
     1.4  qed
     1.5  
     1.6  declaration {* Partial_Function.init "heap" @{term heap.fixp_fun}
     1.7 -  @{term heap.mono_body} @{thm heap.fixp_rule_uc} *}
     1.8 +  @{term heap.mono_body} @{thm heap.fixp_rule_uc} NONE *}
     1.9  
    1.10  
    1.11  abbreviation "mono_Heap \<equiv> monotone (fun_ord Heap_ord) Heap_ord"