| changeset 5608 | a82a038a3e7a |
| parent 5323 | 028e00595280 |
| child 8732 | aef229ca5e77 |
| 5607:5db9e2343ade | 5608:a82a038a3e7a |
|---|---|
23 step :: "('a,'s)na => 'a => ('s * 's)set" |
23 step :: "('a,'s)na => 'a => ('s * 's)set" |
24 "step A a == {(p,q) . q : next A a p}" |
24 "step A a == {(p,q) . q : next A a p}" |
25 |
25 |
26 consts steps :: "('a,'s)na => 'a list => ('s * 's)set" |
26 consts steps :: "('a,'s)na => 'a list => ('s * 's)set" |
27 primrec |
27 primrec |
28 "steps A [] = id" |
28 "steps A [] = Id" |
29 "steps A (a#w) = steps A w O step A a" |
29 "steps A (a#w) = steps A w O step A a" |
30 |
30 |
31 end |
31 end |