equal
deleted
inserted
replaced
264 subsubsection {* Logical intermediate layer *} |
264 subsubsection {* Logical intermediate layer *} |
265 |
265 |
266 definition |
266 definition |
267 Fail :: "message_string \<Rightarrow> exception" |
267 Fail :: "message_string \<Rightarrow> exception" |
268 where |
268 where |
269 [code func del]: "Fail s = Exn" |
269 [code del]: "Fail s = Exn" |
270 |
270 |
271 definition |
271 definition |
272 raise_exc :: "exception \<Rightarrow> 'a Heap" |
272 raise_exc :: "exception \<Rightarrow> 'a Heap" |
273 where |
273 where |
274 [code func del]: "raise_exc e = raise []" |
274 [code del]: "raise_exc e = raise []" |
275 |
275 |
276 lemma raise_raise_exc [code func, code inline]: |
276 lemma raise_raise_exc [code, code inline]: |
277 "raise s = raise_exc (Fail (STR s))" |
277 "raise s = raise_exc (Fail (STR s))" |
278 unfolding Fail_def raise_exc_def raise_def .. |
278 unfolding Fail_def raise_exc_def raise_def .. |
279 |
279 |
280 hide (open) const Fail raise_exc |
280 hide (open) const Fail raise_exc |
281 |
281 |