equal
deleted
inserted
replaced
23 "accepts A w == ? q. (start A,q) : steps A w & fin A q" |
23 "accepts A w == ? q. (start A,q) : steps A w & fin A q" |
24 |
24 |
25 (* not really used: |
25 (* not really used: |
26 consts delta :: "('a,'s)nae => 'a list => 's => 's set" |
26 consts delta :: "('a,'s)nae => 'a list => 's => 's set" |
27 primrec |
27 primrec |
28 "delta A [] s = (eps A)^* ^^ {s}" |
28 "delta A [] s = (eps A)^* ``` {s}" |
29 "delta A (a#w) s = lift(delta A w) (lift(next A (Some a)) ((eps A)^* ^^ {s}))" |
29 "delta A (a#w) s = lift(delta A w) (lift(next A (Some a)) ((eps A)^* ``` {s}))" |
30 *) |
30 *) |
31 end |
31 end |