nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Disabled non-working value.

This commit is contained in:
Achim D. Brucker 2018-05-19 22:23:44 +01:00
parent 3a431c4f72
commit edbdf5fd03
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
RegExp.thy
View File

@ -1,8 +1,8 @@
theory RegExp
imports Main
begin
value "insert"
(* value "insert" *)
datatype 'a rexp = Empty ("<>")
| Atom 'a ("\<lfloor>_\<rfloor>" 65)
| Alt "('a rexp)" "('a rexp)" (infixr "||" 55)
@ -111,4 +111,4 @@ by (simp add: epsilonAlt)
no_notation Atom ("\<lfloor>_\<rfloor>")
end
end