[isabelle-dev] user errors

Christian Sternagel c-sterna at jaist.ac.jp
Wed Oct 31 07:36:20 CET 2012

Maybe this is for Florian or Lukas,

Routinely checking all the TODOs and FIXMEs in our IsaFoR sources I 
found the following fragment:

   subsection {* User exceptions in generated code *}
   (* FIXME:  will be moved to Main. update: did not happen for 
Isabelle2012. *)

   definition error :: "String.literal => 'a => 'a"
   where [code del]: "error msg x = x"

   code_const error
     (Eval "(fn msg =>/ fn x =>/ error msg)")

   code_reserved Eval error

Would it make sense to make this part of Main as indicated in the comment?



More information about the isabelle-dev mailing list