src/HOLCF/Makefile
changeset 346 216bc2ea1294
parent 338 e3489bc1f857
child 468 3dd1dcb509ac
equal deleted inserted replaced
345:7007562172b1 346:216bc2ea1294
    14 #Makes HOL Isabelle if this file is ABSENT -- but not 
    14 #Makes HOL Isabelle if this file is ABSENT -- but not 
    15 #if it is out of date, since this Makefile does not know its dependencies!
    15 #if it is out of date, since this Makefile does not know its dependencies!
    16 
    16 
    17 BIN = $(ISABELLEBIN)
    17 BIN = $(ISABELLEBIN)
    18 COMP = $(ISABELLECOMP)
    18 COMP = $(ISABELLECOMP)
    19 FILES = ROOT.ML Void.thy Void.ML Porder.thy Porder.ML Pcpo.thy \
    19 FILES = ROOT.ML Holcfb.thy Holcfb.ML Void.thy Void.ML \
       
    20 	Porder0.thy Porder.thy Porder.ML  Pcpo.thy \
    20 	Pcpo.ML Fun1.thy Fun1.ML Fun2.thy Fun2.ML Fun3.thy Fun3.ML \
    21 	Pcpo.ML Fun1.thy Fun1.ML Fun2.thy Fun2.ML Fun3.thy Fun3.ML \
    21 	Cfun1.thy Cfun1.ML Cfun2.thy Cfun2.ML Cfun3.thy Cfun3.ML \
    22 	Cfun1.thy Cfun1.ML Cfun2.thy Cfun2.ML Cfun3.thy Cfun3.ML \
    22 	cinfix.ML\
    23 	Cont.thy Cont.ML cinfix.ML\
       
    24 	Cprod1.thy Cprod1.ML Cprod2.thy Cprod2.ML Cprod3.thy Cprod3.ML \
    23 	Sprod0.thy Sprod0.ML Sprod1.thy Sprod1.ML Sprod2.thy Sprod2.ML\
    25 	Sprod0.thy Sprod0.ML Sprod1.thy Sprod1.ML Sprod2.thy Sprod2.ML\
    24 	Sprod3.thy Sprod3.ML
    26 	Sprod3.thy Sprod3.ML\
       
    27 	Ssum0.thy Ssum0.ML Ssum1.thy Ssum1.ML Ssum2.thy Ssum2.ML\
       
    28 	Ssum3.thy Ssum3.ML\
       
    29 	Lift1.thy Lift1.ML Lift2.thy Lift2.ML Lift3.thy Lift3.ML \
       
    30 	Fix.thy Fix.ML ccc1.thy ccc1.ML One.thy One.ML \
       
    31 	Tr1.thy Tr1.ML Tr2.thy Tr2.ML HOLCF.thy HOLCF.ML \
       
    32 	Dnat.thy Dnat.ML Dnat2.thy Dnat2.ML \
       
    33 	Stream.thy Stream.ML Stream2.thy Stream2.ML Dlist.thy Dlist.ML 
    25 
    34 
    26 EX_FILES = ex/Coind.thy ex/Coind.ML \
    35 EX_FILES = ex/Coind.thy ex/Coind.ML ex/Hoare.thy ex/Hoare.ML \
    27            ex/Hoare.thy ex/Hoare.ML ex/Loop.thy ex/Loop.ML
    36            ex/Loop.thy ex/Loop.ML ex/Dagstuhl.thy ex/Dagstuhl.ML 
    28 
    37 
    29 $(BIN)/HOLCF:   $(BIN)/HOL  $(FILES) 
    38 $(BIN)/HOLCF:   $(BIN)/HOL  $(FILES) 
    30 	case "$(COMP)" in \
    39 	case "$(COMP)" in \
    31 	poly*)  echo 'make_database"$(BIN)/HOLCF"; quit();'  \
    40 	poly*)  echo 'make_database"$(BIN)/HOLCF"; quit();'  \
    32 		     | $(COMP) $(BIN)/HOL ;\
    41 		     | $(COMP) $(BIN)/HOL ;\