author | berghofe |
Fri, 24 Jul 1998 13:19:38 +0200 | |
changeset 5184 | 9b8547a9496a |
parent 4907 | 0eb6730de30f |
child 5323 | 028e00595280 |
permissions | -rw-r--r-- |
(* Title: HOL/Lex/NA.thy ID: $Id$ Author: Tobias Nipkow Copyright 1998 TUM Nondeterministic automata *) NA = List + AutoProj + types ('a,'s)na = "'s * ('a => 's => 's set) * ('s => bool)" consts delta :: "('a,'s)na => 'a list => 's => 's set" primrec "delta A [] p = {p}" "delta A (a#w) p = Union(delta A w `` next A a p)" constdefs accepts :: ('a,'s)na => 'a list => bool "accepts A w == ? q : delta A w (start A). fin A q" end