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