diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index bef34e0..8d530b0 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -331,7 +331,7 @@ is currently only available in the SML API's of the kernel. symbolic evaluation using the simplifier, \nbe\ for \<^emph>\normalization by evaluation\ and \<^emph>\code\ for code generation in SML. \<^item> \upd_meta_args\ : - \<^rail>\ (obj_id ('::' class_id) ((',' attribute ('=' | '+=') HOL_term) * ))\ + \<^rail>\ (obj_id ('::' class_id) ((',' attribute (':=' | '+=') HOL_term) * ))\ \<^item> \annotated_text_element\ : \<^rail>\ ( @@{command "text*"} '[' meta_args ']' '\' formal_text '\'