Theory ML_Eval_Antiquotation

✐‹creator "Kevin Kappelmann"›
section ‹ML Eval Antiquotation›
theory ML_Eval_Antiquotation
  imports
    ML_Unification.ML_Functor_Instances
begin

paragraph ‹Summary›
text ‹Antiquotation for ML evaluation.›

ML_file‹eval_antiquotation.ML›

ML‹
  \<^functor_instance>‹struct_name: Standard_Eval_Antiquotation
    functor_name: Eval_Antiquotation
    id: ‹""›
    more_args: ‹val init_args = {
      parser = SOME (Parse_Util.ML_string (K "eval string must be non-empty."))
    }››
›
local_setup ‹Standard_Eval_Antiquotation.setup_attribute NONE›
setup ‹Standard_Eval_Antiquotation.setup_antiquotation›

end