# HG changeset patch
# User nipkow
# Date 1080723720 -7200
# Node ID 0c135fa75626f185afab79707dd82d9bd38a52c3
# Parent  8d5c551a9260b13442e59549777efea0e7e7f26e
Lex now in AFP

diff -r 8d5c551a9260 -r 0c135fa75626 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Mar 31 11:00:25 2004 +0200
+++ b/src/HOL/IsaMakefile	Wed Mar 31 11:02:00 2004 +0200
@@ -28,7 +28,6 @@
   HOL-Isar_examples \
   HOL-Lambda \
   HOL-Lattice \
-  HOL-Lex \
   HOL-MicroJava \
   HOL-Modelcheck \
   HOL-NanoJava \
@@ -283,19 +282,6 @@
 	@$(ISATOOL) usedir -g true $(OUT)/HOL HoareParallel
 
 
-## HOL-Lex
-
-HOL-Lex: HOL $(LOG)/HOL-Lex.gz
-
-$(LOG)/HOL-Lex.gz: $(OUT)/HOL \
-  Lex/AutoChopper.thy Lex/AutoChopper1.thy Lex/AutoMaxChop.thy \
-  Lex/AutoProj.thy Lex/Automata.thy Lex/Chopper.thy Lex/DA.thy \
-  Lex/MaxChop.thy Lex/MaxPrefix.thy Lex/NA.thy Lex/NAe.thy Lex/RegExp2NAe.thy \
-  Lex/Scanner.thy Lex/RegExp2NA.thy Lex/ROOT.ML Lex/RegExp.thy Lex/RegSet.thy \
-  Lex/RegSet_of_nat_DA.thy Library/List_Prefix.thy
-	@$(ISATOOL) usedir $(OUT)/HOL Lex
-
-
 ## HOL-Algebra
 
 HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz