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

Merge branch 'master' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
Isabelle_DOF/Isabelle_DOF/master This commit looks good Details

This commit is contained in:
Achim D. Brucker 2019-07-19 23:33:18 +01:00
parent b547d0cae8 00877b728e
commit 2b92d5d258
1 changed files with 5 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
examples/technical_report/IsaDof_Manual/04_RefMan.thy
View File

@ -346,8 +346,11 @@ text\<open>
\<^item> \<open>default_clause\<close> : \<^item> \<open>default_clause\<close> :
\<^rail>\<open> '<=' '"' expr '"' \<close> \<^rail>\<open> '<=' '"' expr '"' \<close>
\<^item> \<open>regexpr\<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> \<close>