src/HOL/Lex/RegSet.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/RegSet.thy	Mon Apr 27 16:46:56 1998 +0200
@@ -0,0 +1,21 @@
+(*  Title:      HOL/Lex/RegSet.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+
+Regular sets
+*)
+
+RegSet = List +
+
+constdefs
+ conc :: 'a list set => 'a list set => 'a list set
+"conc A B == {xs@ys | xs ys. xs:A & ys:B}"
+
+consts star :: 'a list set => 'a list set
+inductive "star A"
+intrs
+  NilI   "[] : star A"
+  ConsI  "[| a:A; as : star A |] ==> a@as : star A"
+
+end