diff -r 504b129e0502 -r 028e00595280 src/HOL/Lex/NA.thy
--- a/src/HOL/Lex/NA.thy	Mon Aug 17 11:00:27 1998 +0200
+++ b/src/HOL/Lex/NA.thy	Mon Aug 17 11:00:57 1998 +0200
@@ -19,4 +19,13 @@
  accepts ::   ('a,'s)na => 'a list => bool
 "accepts A w == ? q : delta A w (start A). fin A q"
 
+constdefs
+ step :: "('a,'s)na => 'a => ('s * 's)set"
+"step A a == {(p,q) . q : next A a p}"
+
+consts steps :: "('a,'s)na => 'a list => ('s * 's)set"
+primrec
+"steps A [] = id"
+"steps A (a#w) = steps A w  O  step A a"
+
 end