src/HOL/Lex/RegExp.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/RegExp.thy	Mon Apr 27 16:46:56 1998 +0200
@@ -0,0 +1,25 @@
+(*  Title:      HOL/Lex/RegExp.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+
+Regular expressions
+*)
+
+RegExp = RegSet +
+
+datatype 'a rexp = Empty
+                 | Atom 'a
+                 | Union ('a rexp) ('a rexp)
+                 | Conc ('a rexp) ('a rexp)
+                 | Star ('a rexp)
+
+consts lang :: 'a rexp => 'a list set
+primrec lang rexp
+lang_Emp  "lang Empty = {}"
+lang_Atom "lang (Atom a) = {[a]}"
+lang_Un   "lang (Union el er) = (lang el) Un (lang er)"
+lang_Conc "lang (Conc el er) = RegSet.conc (lang el) (lang er)"
+lang_Star "lang (Star e) = RegSet.star(lang e)"
+
+end