isabelle: src/HOL/Lex/ROOT.ML@bc11b5b06f87 (annotated)

1465 5d7a7e439cec expanded tabs clasohm parents: 1351 diff changeset	1	(* Title: HOL/Lex/ROOT.ML
1344 f172a7f14e49 Half a lexical analyzer generator. nipkow parents: diff changeset	2	ID: $Id$
1465 5d7a7e439cec expanded tabs clasohm parents: 1351 diff changeset	3	Author: Tobias Nipkow
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: 4712 diff changeset	4	Copyright 1998 TUM
1344 f172a7f14e49 Half a lexical analyzer generator. nipkow parents: diff changeset	5	*)
f172a7f14e49 Half a lexical analyzer generator. nipkow parents: diff changeset	6
1465 5d7a7e439cec expanded tabs clasohm parents: 1351 diff changeset	7	HOL_build_completed; (Make examples fail if HOL did)
1344 f172a7f14e49 Half a lexical analyzer generator. nipkow parents: diff changeset	8
f172a7f14e49 Half a lexical analyzer generator. nipkow parents: diff changeset	9	use_thy"AutoChopper";
4137 2ce2e659c2b1 Added an alternativ version of AutoChopper and a theory for the conversion of nipkow parents: 1465 diff changeset	10	use_thy"AutoChopper1";
4712 facfbbca7242 Removed expand_split from simpset. nipkow parents: 4137 diff changeset	11	use_thy"AutoMaxChop";
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: 4712 diff changeset	12	(* Do no swap the next 2.
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: 4712 diff changeset	13	There is some interference, probably via claset() or simpset().
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: 4712 diff changeset	14	Or via ML-bound names of axioms that are overwritten?
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: 4712 diff changeset	15	*)
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: 4712 diff changeset	16	use_thy"RegSet_of_nat_DA";
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: 4712 diff changeset	17	use_thy"NAe_of_RegExp";
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: 4712 diff changeset	18	use_thy"Automata";

author	nipkow
	Mon, 27 Apr 1998 16:46:56 +0200
changeset 4832	bc11b5b06f87
parent 4712	facfbbca7242
child 4907	0eb6730de30f
permissions	-rw-r--r--