From 8513f7d2677bdf01fa03cd97356cfca71ddfe580 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= <nicolasmeric@posteo.net>
Date: Tue, 17 Jan 2023 09:01:55 +0100
Subject: [PATCH] Update doc_class rails to match accepts clause

---
 examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
index 861fd9c2..1b5d30f4 100644
--- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
+++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy
@@ -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>