src/HOL/Lex/NA.thy
changeset 8732 aef229ca5e77
parent 5608 a82a038a3e7a
child 10834 a7897aebbffc
equal deleted inserted replaced
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