# HG changeset patch
# User nipkow
# Date 853525778 -3600
# Node ID 0ba3755ce39800870f024a8e73d57dfec9703fd6
# Parent  43650141d67d0cd36312f4c72d2a9003d59d7671
Added W0 and modified MiniML.

diff -r 43650141d67d -r 0ba3755ce398 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Jan 17 19:26:47 1997 +0100
+++ b/src/HOL/IsaMakefile	Fri Jan 17 19:29:38 1997 +0100
@@ -123,9 +123,20 @@
 	@$(ISATOOL) testdir $(OUT)/HOL Lambda
 
 
-## Type inference for MiniML
+## Type inference without let
+
+W0_NAMES = I Maybe MiniML Type W
+
+W0_FILES = W0/ROOT.ML \
+	      $(W0_NAMES:%=W0/%.thy) $(W0_NAMES:%=W0/%.ML)
 
-MINIML_NAMES = I Maybe MiniML Type W
+W0: $(OUT)/HOL $(W0_FILES)
+	@$(ISATOOL) testdir $(OUT)/HOL W0
+
+
+## Type inference with let
+
+MINIML_NAMES = Generalize Instance Maybe MiniML Type W
 
 MINIML_FILES = MiniML/ROOT.ML \
 	      $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
@@ -159,7 +170,7 @@
 
 ## Full test
 
-test:	$(OUT)/HOL TFL IMP Hoare Lex Integ Auth Subst Lambda MiniML IOA ex
+test:	$(OUT)/HOL TFL IMP Hoare Lex Integ Auth Subst Lambda W0 MiniML IOA ex
 	echo 'Test examples ran successfully' > test