src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 40266 d72f1f734e5a
parent 40173 0ffdd6baec03
child 40267 a03e288d7902
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Oct 29 11:35:28 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Oct 29 13:49:49 2010 +0200
     1.3 @@ -16,6 +16,10 @@
     1.4    and transform the heap, or fail *}
     1.5  datatype 'a Heap = Heap "heap \<Rightarrow> ('a \<times> heap) option"
     1.6  
     1.7 +lemma [code, code del]:
     1.8 +  "(Code_Evaluation.term_of :: 'a::typerep Heap \<Rightarrow> Code_Evaluation.term) = Code_Evaluation.term_of"
     1.9 +  ..
    1.10 +
    1.11  primrec execute :: "'a Heap \<Rightarrow> heap \<Rightarrow> ('a \<times> heap) option" where
    1.12    [code del]: "execute (Heap f) = f"
    1.13