changeset 8732 | aef229ca5e77 |
parent 5608 | a82a038a3e7a |
child 10834 | a7897aebbffc |
8731:085f0e32b9d6 | 8732:aef229ca5e77 |
---|---|
4 Copyright 1998 TUM |
4 Copyright 1998 TUM |
5 |
5 |
6 Nondeterministic automata |
6 Nondeterministic automata |
7 *) |
7 *) |
8 |
8 |
9 NA = List + AutoProj + |
9 NA = AutoProj + |
10 |
10 |
11 types ('a,'s)na = "'s * ('a => 's => 's set) * ('s => bool)" |
11 types ('a,'s)na = "'s * ('a => 's => 's set) * ('s => bool)" |
12 |
12 |
13 consts delta :: "('a,'s)na => 'a list => 's => 's set" |
13 consts delta :: "('a,'s)na => 'a list => 's => 's set" |
14 primrec |
14 primrec |