src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 36176 3fe7e97ccca8
parent 36078 59f6773a7d1d
child 37591 d3daea901123
equal deleted inserted replaced
36175:5cec4ca719d1 36176:3fe7e97ccca8
   403 
   403 
   404 abbreviation "MREC == mrec.MREC"
   404 abbreviation "MREC == mrec.MREC"
   405 lemmas MREC_rule = mrec.MREC_rule
   405 lemmas MREC_rule = mrec.MREC_rule
   406 lemmas MREC_pinduct = mrec.MREC_pinduct
   406 lemmas MREC_pinduct = mrec.MREC_pinduct
   407 
   407 
   408 hide (open) const heap execute
   408 hide_const (open) heap execute
   409 
   409 
   410 
   410 
   411 subsection {* Code generator setup *}
   411 subsection {* Code generator setup *}
   412 
   412 
   413 subsubsection {* Logical intermediate layer *}
   413 subsubsection {* Logical intermediate layer *}
   424 
   424 
   425 lemma raise_raise_exc [code, code_unfold]:
   425 lemma raise_raise_exc [code, code_unfold]:
   426   "raise s = raise_exc (Fail (STR s))"
   426   "raise s = raise_exc (Fail (STR s))"
   427   unfolding Fail_def raise_exc_def raise_def ..
   427   unfolding Fail_def raise_exc_def raise_def ..
   428 
   428 
   429 hide (open) const Fail raise_exc
   429 hide_const (open) Fail raise_exc
   430 
   430 
   431 
   431 
   432 subsubsection {* SML and OCaml *}
   432 subsubsection {* SML and OCaml *}
   433 
   433 
   434 code_type Heap (SML "unit/ ->/ _")
   434 code_type Heap (SML "unit/ ->/ _")