isabelle: src/HOL/Lex/ROOT.ML@b279a84ac11c (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";
4907 0eb6730de30f Reshuffeling, renaming and a few simple corollaries. nipkow parents: 4832 diff changeset	12	(* Do not swap the next two use_thy's.
4832 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";
5323 028e00595280 Direct translation RegExp -> NA! nipkow parents: 4907 diff changeset	17	use_thy"RegExp2NA";
4907 0eb6730de30f Reshuffeling, renaming and a few simple corollaries. nipkow parents: 4832 diff changeset	18	use_thy"RegExp2NAe";
0eb6730de30f Reshuffeling, renaming and a few simple corollaries. nipkow parents: 4832 diff changeset	19	use_thy"Scanner";

author	wenzelm
	Mon, 16 Nov 1998 10:41:08 +0100
changeset 5869	b279a84ac11c
parent 5323	028e00595280
child 6349	f7750d816c21
permissions	-rw-r--r--