isabelle: src/HOL/Lex/ROOT.ML@94d2d6531c57 (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
9000 c20d58286a51 cleaned up; wenzelm parents: 8732 diff changeset	7	time_use_thy "AutoChopper";
c20d58286a51 cleaned up; wenzelm parents: 8732 diff changeset	8	time_use_thy "AutoChopper1";
c20d58286a51 cleaned up; wenzelm parents: 8732 diff changeset	9	time_use_thy "AutoMaxChop";
c20d58286a51 cleaned up; wenzelm parents: 8732 diff changeset	10	time_use_thy "RegSet_of_nat_DA";
c20d58286a51 cleaned up; wenzelm parents: 8732 diff changeset	11	time_use_thy "Scanner";