nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Add comment for term_ and value_ ML antiquoatations

This commit is contained in:
Nicolas Méric 2023-01-11 14:49:29 +01:00
parent 72d8000f7b
commit 8496963fec
1 changed files with 2 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/DOF/Isa_DOF.thy
View File

@ -1898,7 +1898,8 @@ val _ =
(opt_attributes -- (opt_evaluator -- opt_modes -- Parse.term)
>> (fn (meta_args_opt, eval_args ) => pass_trans_to_assert_value_cmd meta_args_opt eval_args));
(* setup ontology - aware text antiquotations. Due to lexical restrictions, we can not
(* setup ontology - aware text and ML antiquotations. Due to lexical restrictions, we can not
declare them as value* or term*, although we will refer to them this way in papers. *)
local
fun pretty_term_style ctxt (style: term -> term, t) =