diff -r dae4d63a1318 -r bc11b5b06f87 src/HOL/Lex/NAe.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lex/NAe.thy	Mon Apr 27 16:46:56 1998 +0200
@@ -0,0 +1,34 @@
+(*  Title:      HOL/Lex/NAe.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TUM
+
+Nondeterministic automata with epsilon transitions
+*)
+
+NAe = List + Option + NA +
+
+types ('a,'s)nae = ('a option,'s)na
+
+constdefs
+ step :: "('a,'s)nae => 'a option => ('s * 's)set"
+"step A a == {(p,q) . q : next A a p}"
+
+syntax eps :: "('a,'s)nae => ('s * 's)set"
+translations "eps A" == "step A None"
+
+consts steps :: "('a,'s)nae => 'a list =>   ('s * 's)set"
+primrec steps list
+"steps A [] = (eps A)^*"
+"steps A (a#w) = steps A w  O  step A (Some a)  O  (eps A)^*"
+
+consts delta :: "('a,'s)nae => 'a list => 's => 's set"
+primrec delta list
+"delta A [] s = (eps A)^* ^^ {s}"
+"delta A (a#w) s = lift(delta A w) (lift(next A (Some a)) ((eps A)^* ^^ {s}))"
+
+constdefs
+ accepts :: ('a,'s)nae => 'a list => bool
+"accepts A w == ? q. (start A,q) : steps A w & fin A q"
+
+end