src/HOL/Lex/RegExp2NA.thy
changeset 12792 b344226f924c
parent 10834 a7897aebbffc
child 14440 3d6ed7eedfc8
     1.1 --- a/src/HOL/Lex/RegExp2NA.thy	Thu Jan 17 15:06:36 2002 +0100
     1.2 +++ b/src/HOL/Lex/RegExp2NA.thy	Thu Jan 17 19:32:22 2002 +0100
     1.3 @@ -20,8 +20,8 @@
     1.4              %b s. if s=[True] & b=a then {[False]} else {},
     1.5              %s. s=[False])"
     1.6  
     1.7 - union :: 'a bitsNA => 'a bitsNA => 'a bitsNA
     1.8 -"union == %(ql,dl,fl)(qr,dr,fr).
     1.9 + or :: 'a bitsNA => 'a bitsNA => 'a bitsNA
    1.10 +"or == %(ql,dl,fl)(qr,dr,fr).
    1.11     ([],
    1.12      %a s. case s of
    1.13              [] => (True ## dl a ql) Un (False ## dr a qr)
    1.14 @@ -47,14 +47,14 @@
    1.15  "plus == %(q,d,f). (q, %a s. d a s Un (if f s then d a q else {}), f)"
    1.16  
    1.17   star :: 'a bitsNA => 'a bitsNA
    1.18 -"star A == union epsilon (plus A)"
    1.19 +"star A == or epsilon (plus A)"
    1.20  
    1.21  consts rexp2na :: 'a rexp => 'a bitsNA
    1.22  primrec
    1.23  "rexp2na Empty      = ([], %a s. {}, %s. False)"
    1.24  "rexp2na(Atom a)    = atom a"
    1.25 -"rexp2na(Union r s) = union (rexp2na r) (rexp2na s)"
    1.26 -"rexp2na(Conc r s)  = conc  (rexp2na r) (rexp2na s)"
    1.27 -"rexp2na(Star r)    = star  (rexp2na r)"
    1.28 +"rexp2na(Or r s)    = or   (rexp2na r) (rexp2na s)"
    1.29 +"rexp2na(Conc r s)  = conc (rexp2na r) (rexp2na s)"
    1.30 +"rexp2na(Star r)    = star (rexp2na r)"
    1.31  
    1.32  end