isabelle: src/HOL/Lex/RegSet.thy@bc11b5b06f87 (annotated)

4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	1	(* Title: HOL/Lex/RegSet.thy
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	2	ID: $Id$
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	3	Author: Tobias Nipkow
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	4	Copyright 1998 TUM
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	5
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	6	Regular sets
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	7	*)
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	8
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	9	RegSet = List +
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	10
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	11	constdefs
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	12	conc :: 'a list set => 'a list set => 'a list set
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	13	"conc A B == {xs@ys \| xs ys. xs:A & ys:B}"
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	14
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	15	consts star :: 'a list set => 'a list set
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	16	inductive "star A"
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	17	intrs
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	18	NilI "[] : star A"
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	19	ConsI "[\| a:A; as : star A \|] ==> a@as : star A"
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	20
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: diff changeset	21	end

author	nipkow
	Mon, 27 Apr 1998 16:46:56 +0200
changeset 4832	bc11b5b06f87
child 8732	aef229ca5e77
permissions	-rw-r--r--