isabelle: src/HOL/Lex/RegSet.thy@b03a0b219139 (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
8732 aef229ca5e77 fixed theory deps; wenzelm parents: 4832 diff changeset	9	RegSet = Main +
4832 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	paulson
	Fri, 21 Apr 2000 11:28:18 +0200
changeset 8756	b03a0b219139
parent 8732	aef229ca5e77
child 14431	ade3d26e0caf
permissions	-rw-r--r--