src/HOL/IsaMakefile
changeset 2527 0ba3755ce398
parent 2473 3eb12c85846c
child 2545 d10abc8c11fb
     1.1 --- a/src/HOL/IsaMakefile	Fri Jan 17 19:26:47 1997 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Fri Jan 17 19:29:38 1997 +0100
     1.3 @@ -123,9 +123,20 @@
     1.4  	@$(ISATOOL) testdir $(OUT)/HOL Lambda
     1.5  
     1.6  
     1.7 -## Type inference for MiniML
     1.8 +## Type inference without let
     1.9 +
    1.10 +W0_NAMES = I Maybe MiniML Type W
    1.11 +
    1.12 +W0_FILES = W0/ROOT.ML \
    1.13 +	      $(W0_NAMES:%=W0/%.thy) $(W0_NAMES:%=W0/%.ML)
    1.14  
    1.15 -MINIML_NAMES = I Maybe MiniML Type W
    1.16 +W0: $(OUT)/HOL $(W0_FILES)
    1.17 +	@$(ISATOOL) testdir $(OUT)/HOL W0
    1.18 +
    1.19 +
    1.20 +## Type inference with let
    1.21 +
    1.22 +MINIML_NAMES = Generalize Instance Maybe MiniML Type W
    1.23  
    1.24  MINIML_FILES = MiniML/ROOT.ML \
    1.25  	      $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
    1.26 @@ -159,7 +170,7 @@
    1.27  
    1.28  ## Full test
    1.29  
    1.30 -test:	$(OUT)/HOL TFL IMP Hoare Lex Integ Auth Subst Lambda MiniML IOA ex
    1.31 +test:	$(OUT)/HOL TFL IMP Hoare Lex Integ Auth Subst Lambda W0 MiniML IOA ex
    1.32  	echo 'Test examples ran successfully' > test
    1.33  
    1.34