Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Fix typo in upd_meta_args rail road in manual
ci/woodpecker/push/build Pipeline was successful Details

This commit is contained in:
Nicolas Méric 2022-04-08 13:04:50 +02:00
parent e3caad804b
commit 1457c1cb85
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
View File

@ -331,7 +331,7 @@ is currently only available in the SML API's of the kernel.
symbolic evaluation using the simplifier, \<open>nbe\<close> for \<^emph>\<open>normalization by
evaluation\<close> and \<^emph>\<open>code\<close> for code generation in SML.
\<^item> \<open>upd_meta_args\<close> :
\<^rail>\<open> (obj_id ('::' class_id) ((',' attribute ('=' | '+=') HOL_term) * ))\<close>
\<^rail>\<open> (obj_id ('::' class_id) ((',' attribute (':=' | '+=') HOL_term) * ))\<close>
\<^item> \<open>annotated_text_element\<close> :
\<^rail>\<open>
( @@{command "text*"} '[' meta_args ']' '\<open>' formal_text '\<close>'