isabelle: src/HOL/Lex/ROOT.ML@06ae685ca5a3 (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
f172a7f14e49 Half a lexical analyzer generator. nipkow parents: diff changeset	7	use_thy"AutoChopper";
4137 2ce2e659c2b1 Added an alternativ version of AutoChopper and a theory for the conversion of nipkow parents: 1465 diff changeset	8	use_thy"AutoChopper1";
4712 facfbbca7242 Removed expand_split from simpset. nipkow parents: 4137 diff changeset	9	use_thy"AutoMaxChop";
4907 0eb6730de30f Reshuffeling, renaming and a few simple corollaries. nipkow parents: 4832 diff changeset	10	(* Do not swap the next two use_thy's.
4832 bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: 4712 diff changeset	11	There is some interference, probably via claset() or simpset().
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: 4712 diff changeset	12	Or via ML-bound names of axioms that are overwritten?
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: 4712 diff changeset	13	*)
bc11b5b06f87 Added conversion of reg.expr. to automata. nipkow parents: 4712 diff changeset	14	use_thy"RegSet_of_nat_DA";
5323 028e00595280 Direct translation RegExp -> NA! nipkow parents: 4907 diff changeset	15	use_thy"RegExp2NA";
4907 0eb6730de30f Reshuffeling, renaming and a few simple corollaries. nipkow parents: 4832 diff changeset	16	use_thy"RegExp2NAe";
0eb6730de30f Reshuffeling, renaming and a few simple corollaries. nipkow parents: 4832 diff changeset	17	use_thy"Scanner";

author	wenzelm
	Thu, 22 Jul 1999 20:53:54 +0200
changeset 7063	06ae685ca5a3
parent 6349	f7750d816c21
child 8732	aef229ca5e77
permissions	-rw-r--r--