author | wenzelm |
Wed, 01 Jul 1998 11:20:32 +0200 | |
changeset 5104 | 230cca8452c7 |
parent 4907 | 0eb6730de30f |
child 10797 | 028d22926a41 |
permissions | -rw-r--r-- |
(* Title: HOL/Lex/Automata.thy ID: $Id$ Author: Tobias Nipkow Copyright 1998 TUM Conversions between different kinds of automata *) Automata = DA + NAe + constdefs na2da :: ('a,'s)na => ('a,'s set)da "na2da A == ({start A}, %a Q. Union(next A a `` Q), %Q. ? q:Q. fin A q)" nae2da :: ('a,'s)nae => ('a,'s set)da "nae2da A == ({start A}, %a Q. Union(next A (Some a) `` ((eps A)^* ^^ Q)), %Q. ? p: (eps A)^* ^^ Q. fin A p)" end