src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 39250 548a3e5521ab
parent 39198 f967a16dfcdd
child 39302 d7728f65b353
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Sep 09 11:10:44 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Thu Sep 09 14:38:14 2010 +0200
     1.3 @@ -402,12 +402,15 @@
     1.4  
     1.5  subsubsection {* Logical intermediate layer *}
     1.6  
     1.7 -primrec raise' :: "String.literal \<Rightarrow> 'a Heap" where
     1.8 -  [code del, code_post]: "raise' (STR s) = raise s"
     1.9 +definition raise' :: "String.literal \<Rightarrow> 'a Heap" where
    1.10 +  [code del]: "raise' s = raise (explode s)"
    1.11 +
    1.12 +lemma [code_post]: "raise' (STR s) = raise s"
    1.13 +unfolding raise'_def by (simp add: STR_inverse)
    1.14  
    1.15  lemma raise_raise' [code_inline]:
    1.16    "raise s = raise' (STR s)"
    1.17 -  by simp
    1.18 +  unfolding raise'_def by (simp add: STR_inverse)
    1.19  
    1.20  code_datatype raise' -- {* avoid @{const "Heap"} formally *}
    1.21