1.1 --- a/src/HOL/Lex/RegExp2NAe.thy	Thu Jan 17 15:06:36 2002 +0100
     1.2 +++ b/src/HOL/Lex/RegExp2NAe.thy	Thu Jan 17 19:32:22 2002 +0100
     1.3 @@ -20,8 +20,8 @@
     1.4              %b s. if s=[True] & b=Some a then {[False]} else {},
     1.5              %s. s=[False])"
     1.6  
     1.7 - union :: 'a bitsNAe => 'a bitsNAe => 'a bitsNAe
     1.8 -"union == %(ql,dl,fl)(qr,dr,fr).
     1.9 + or :: 'a bitsNAe => 'a bitsNAe => 'a bitsNAe
    1.10 +"or == %(ql,dl,fl)(qr,dr,fr).
    1.11     ([],
    1.12      %a s. case s of
    1.13              [] => if a=None then {True#ql,False#qr} else {}
    1.14 @@ -53,8 +53,8 @@
    1.15  primrec
    1.16  "rexp2nae Empty      = ([], %a s. {}, %s. False)"
    1.17  "rexp2nae(Atom a)    = atom a"
    1.18 -"rexp2nae(Union r s) = union (rexp2nae r) (rexp2nae s)"
    1.19 -"rexp2nae(Conc r s)  = conc  (rexp2nae r) (rexp2nae s)"
    1.20 -"rexp2nae(Star r)    = star  (rexp2nae r)"
    1.21 +"rexp2nae(Or r s)    = or   (rexp2nae r) (rexp2nae s)"
    1.22 +"rexp2nae(Conc r s)  = conc (rexp2nae r) (rexp2nae s)"
    1.23 +"rexp2nae(Star r)    = star (rexp2nae r)"
    1.24  
    1.25  end