--- a/src/HOL/Lex/Automata.thy Fri May 08 15:45:01 1998 +0200
+++ b/src/HOL/Lex/Automata.thy Fri May 08 18:33:29 1998 +0200
@@ -10,11 +10,11 @@
constdefs
na2da :: ('a,'s)na => ('a,'s set)da
-"na2da A == ({start A}, %a Q. lift(next A a) Q, %Q. ? q:Q. fin A q)"
+"na2da A == ({start A}, %a Q. Union(next A a `` Q), %Q. ? q:Q. fin A q)"
nae2da :: ('a,'s)nae => ('a,'s set)da
"nae2da A == ({start A},
- %a Q. lift (next A (Some a)) ((eps A)^* ^^ Q),
+ %a Q. Union(next A (Some a) `` ((eps A)^* ^^ Q)),
%Q. ? p: (eps A)^* ^^ Q. fin A p)"
end