src/HOL/Lex/NAe.thy

 
 syntax eps :: "('a,'s)nae => ('s * 's)set"
 translations "eps A" == "step A None"
 
 consts steps :: "('a,'s)nae => 'a list =>   ('s * 's)set"
-primrec steps list
+primrec
 "steps A [] = (eps A)^*"
 "steps A (a#w) = steps A w  O  step A (Some a)  O  (eps A)^*"
 
 constdefs
  accepts :: ('a,'s)nae => 'a list => bool
 "accepts A w == ? q. (start A,q) : steps A w & fin A q"
 
 (* not really used:
 consts delta :: "('a,'s)nae => 'a list => 's => 's set"
-primrec delta list
+primrec
 "delta A [] s = (eps A)^* ^^ {s}"
 "delta A (a#w) s = lift(delta A w) (lift(next A (Some a)) ((eps A)^* ^^ {s}))"
 *)
 end