--- a/src/HOL/Lex/NA.thy Fri May 08 15:45:01 1998 +0200
+++ b/src/HOL/Lex/NA.thy Fri May 08 18:33:29 1998 +0200
@@ -10,13 +10,10 @@
types ('a,'s)na = "'s * ('a => 's => 's set) * ('s => bool)"
-syntax lift :: ('a => 'b set) => 'a set => 'b set
-translations "lift f A" == "Union(f `` A)"
-
consts delta :: "('a,'s)na => 'a list => 's => 's set"
primrec delta list
"delta A [] p = {p}"
-"delta A (a#w) p = lift (delta A w) (next A a p)"
+"delta A (a#w) p = Union(delta A w `` next A a p)"
constdefs
accepts :: ('a,'s)na => 'a list => bool