--- a/src/HOL/Lex/RegExp2NAe.thy Thu Jan 17 15:06:36 2002 +0100
+++ b/src/HOL/Lex/RegExp2NAe.thy Thu Jan 17 19:32:22 2002 +0100
@@ -20,8 +20,8 @@
%b s. if s=[True] & b=Some a then {[False]} else {},
%s. s=[False])"
- union :: 'a bitsNAe => 'a bitsNAe => 'a bitsNAe
-"union == %(ql,dl,fl)(qr,dr,fr).
+ or :: 'a bitsNAe => 'a bitsNAe => 'a bitsNAe
+"or == %(ql,dl,fl)(qr,dr,fr).
([],
%a s. case s of
[] => if a=None then {True#ql,False#qr} else {}
@@ -53,8 +53,8 @@
primrec
"rexp2nae Empty = ([], %a s. {}, %s. False)"
"rexp2nae(Atom a) = atom a"
-"rexp2nae(Union r s) = union (rexp2nae r) (rexp2nae s)"
-"rexp2nae(Conc r s) = conc (rexp2nae r) (rexp2nae s)"
-"rexp2nae(Star r) = star (rexp2nae r)"
+"rexp2nae(Or r s) = or (rexp2nae r) (rexp2nae s)"
+"rexp2nae(Conc r s) = conc (rexp2nae r) (rexp2nae s)"
+"rexp2nae(Star r) = star (rexp2nae r)"
end