author | haftmann |
Mon, 25 Sep 2006 17:04:14 +0200 | |
changeset 20698 | cb910529d49d |
parent 20697 | 12952535fc2c |
child 20699 | 0cc77abb185a |
src/HOL/HOL.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/HOL.thy Mon Sep 25 17:04:12 2006 +0200 +++ b/src/HOL/HOL.thy Mon Sep 25 17:04:14 2006 +0200 @@ -1389,4 +1389,12 @@ in add_itself end; *} +text {* code generation for arbitrary as exception *} + +setup {* + CodegenSerializer.add_undefined "SML" "arbitrary" "raise Fail \"arbitrary\"" +*} +code_const arbitrary + (Haskell target_atom "(error \"arbitrary\")") + end