pierre.derathe
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update doc_class rails to match accepts clause

This commit is contained in:
Nicolas Méric 2023-01-17 09:01:55 +01:00
parent 2b1a9d009e
commit 8513f7d267
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

@ -235,7 +235,7 @@ A document class\<^bindex>\<open>document class\<close> can be defined using the
We call document classes with an \<open>accepts_clause\<close>
\<^emph>\<open>monitor classes\<close> or \<^emph>\<open>monitors\<close> for short.
\<^rail>\<open> (@@{command "doc_class"}| @@{command "onto_class"}) class_id '=' (class_id '+')? (attribute_decl+) \<newline>
(invariant_decl *) (((rejects_clause accepts_clause) | accepts_clause) *)\<close>
(invariant_decl *) (rejects_clause accepts_clause)? \<newline> (accepts_clause *)\<close>
\<^item> \<open>attribute_decl\<close>:\<^index>\<open>attribute\_decl@\<open>attribute_decl\<close>\<close>
\<^rail>\<open> name '::' '"' type '"' default_clause? \<close>
\<^item> \<open>invariant_decl\<close>:\<^index>\<open>invariant\_decl@\<open>invariant_decl\<close>\<close>