isabelle: src/HOL/Lex/ROOT.ML@2ce2e659c2b1 (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
1344 f172a7f14e49 Half a lexical analyzer generator. nipkow parents: diff changeset	4	Copyright 1995 TUM
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";
2ce2e659c2b1 Added an alternativ version of AutoChopper and a theory for the conversion of nipkow parents: 1465 diff changeset	11	use_thy"Regset_of_auto";