src/HOLCF/IsaMakefile
changeset 2571 b9f641195b48
parent 2494 5d45c2094ff6
child 2640 ee4dfce170a0
     1.1 --- a/src/HOLCF/IsaMakefile	Fri Jan 31 16:56:32 1997 +0100
     1.2 +++ b/src/HOLCF/IsaMakefile	Fri Jan 31 16:57:45 1997 +0100
     1.3 @@ -32,8 +32,10 @@
     1.4  
     1.5  ## Miscellaneous examples
     1.6  
     1.7 -EX_THYS = ex/Fix2.thy ex/Hoare.thy \
     1.8 -	  ex/Loop.thy
     1.9 +EX_THYS = ex/Classlib.thy ex/Witness.thy\
    1.10 +	  ex/Dnat.thy ex/Dlist.thy ex/Stream.thy\
    1.11 +	  ex/Dagstuhl.thy ex/Focus_ex.thy ex/Fix2.thy\
    1.12 +	  ex/Hoare.thy ex/Loop.thy
    1.13  
    1.14  EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
    1.15  
    1.16 @@ -42,17 +44,16 @@
    1.17  
    1.18  
    1.19  ## Explicit domains
    1.20 +#
    1.21 +#EXPLICIT_DOMAINS_THYS = explicit_domains/Dnat.thy explicit_domains/Dnat2.thy\
    1.22 +#		 explicit_domains/Dlist.thy \
    1.23 +#		 explicit_domains/Stream.thy explicit_domains/Stream2.thy
    1.24  
    1.25 -EXPLICIT_DOMAINS_THYS = explicit_domains/Coind.thy explicit_domains/Dlist.thy \
    1.26 -			explicit_domains/Dnat2.thy explicit_domains/Stream.thy \
    1.27 -			explicit_domains/Dagstuhl.thy explicit_domains/Dnat.thy \
    1.28 -			explicit_domains/Focus_ex.thy explicit_domains/Stream2.thy
    1.29 -
    1.30 -EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS) \
    1.31 -			 $(EXPLICIT_DOMAINS_THYS:.thy=.ML)
    1.32 -
    1.33 -test2: explicit_domains/ROOT.ML $(OUT)/HOLCF $(EXPLICIT_DOMAINS_FILES)
    1.34 -	@$(ISATOOL) testdir $(OUT)/HOLCF explicit_domains
    1.35 +#EXPLICIT_DOMAINS_FILES = explicit_domains/ROOT.ML $(EXPLICIT_DOMAINS_THYS) \
    1.36 +#			 $(EXPLICIT_DOMAINS_THYS:.thy=.ML)
    1.37 +#
    1.38 +#test2: explicit_domains/ROOT.ML $(OUT)/HOLCF $(EXPLICIT_DOMAINS_FILES)
    1.39 +#	@$(ISATOOL) testdir $(OUT)/HOLCF explicit_domains
    1.40  
    1.41  
    1.42  .PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF