From 00877b728eb9a9a80cc0d20ad9fff7cc6bd96ae1 Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Fri, 19 Jul 2019 16:24:47 +0200
Subject: [PATCH] regexps

---
 examples/technical_report/IsaDof_Manual/04_RefMan.thy | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/examples/technical_report/IsaDof_Manual/04_RefMan.thy b/examples/technical_report/IsaDof_Manual/04_RefMan.thy
index 1555da1..5a00b5b 100644
--- a/examples/technical_report/IsaDof_Manual/04_RefMan.thy
+++ b/examples/technical_report/IsaDof_Manual/04_RefMan.thy
@@ -346,8 +346,11 @@ text\<open>
 \<^item> \<open>default_clause\<close> :
      \<^rail>\<open> '<=' '"' expr '"' \<close>
 \<^item> \<open>regexpr\<close> :
-     \<^rail>\<open> class_id | '(' regexpr ')' | (regexpr '||' regexpr) | (regexpr '~~' regexpr)\<close>
-           
+     \<^rail>\<open> '\<lfloor>' class_id '\<rfloor>' | '(' regexpr ')' | (regexpr '||' regexpr) | (regexpr '~~' regexpr)
+            | ('\<lbrace>' regexpr '\<rbrace>') | ( '\<lbrace>' regexpr '\<rbrace>\<^sup>*')  \<close>
+     regular expressions describe sequences of \<open>class_id\<close>s (and indirect sequences of document
+     items corresponding to the \<open>class_id\<close>s). The constructors for alternative, sequence, 
+     repetitions and non-empty sequence follow in the top-down order of the above diagram. 
 \<close>