equal
deleted
inserted
replaced
423 setup {* Sign.map_naming (Name_Space.mandatory_path "Code") *} |
423 setup {* Sign.map_naming (Name_Space.mandatory_path "Code") *} |
424 |
424 |
425 definition abort :: "literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a" |
425 definition abort :: "literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a" |
426 where [simp, code del]: "abort _ f = f ()" |
426 where [simp, code del]: "abort _ f = f ()" |
427 |
427 |
|
428 lemma abort_cong: "msg = msg' ==> Code.abort msg f = Code.abort msg' f" |
|
429 by simp |
|
430 |
428 setup {* Sign.map_naming Name_Space.parent_path *} |
431 setup {* Sign.map_naming Name_Space.parent_path *} |
|
432 |
|
433 setup {* Code_Simp.map_ss (Simplifier.add_cong @{thm Code.abort_cong}) *} |
429 |
434 |
430 code_printing constant Code.abort \<rightharpoonup> |
435 code_printing constant Code.abort \<rightharpoonup> |
431 (SML) "!(raise/ Fail/ _)" |
436 (SML) "!(raise/ Fail/ _)" |
432 and (OCaml) "failwith" |
437 and (OCaml) "failwith" |
433 and (Haskell) "error" |
438 and (Haskell) "error" |