author | nipkow |
Tue, 09 Jan 2001 15:32:27 +0100 | |
changeset 10834 | a7897aebbffc |
parent 10797 | 028d22926a41 |
child 14428 | bb2b0e10d9be |
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