author | berghofe |
Fri, 24 Jul 1998 13:19:38 +0200 | |
changeset 5184 | 9b8547a9496a |
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