equal
deleted
inserted
replaced
25 HOLCF: HOL $(OUT)/HOLCF |
25 HOLCF: HOL $(OUT)/HOLCF |
26 |
26 |
27 HOL: |
27 HOL: |
28 @cd $(SRC)/HOL; $(ISATOOL) make HOL |
28 @cd $(SRC)/HOL; $(ISATOOL) make HOL |
29 |
29 |
30 $(OUT)/HOLCF: $(OUT)/HOL Adm.thy Cfun.ML Cfun.thy \ |
30 $(OUT)/HOLCF: $(OUT)/HOL Adm.thy Cfun.ML Cfun.thy Cont.ML Cont.thy \ |
31 Cont.ML Cont.thy Cprod.ML Cprod.thy \ |
31 Cprod.ML Cprod.thy Discrete.thy Domain.thy Fix.ML Fix.thy Fixrec.thy \ |
32 Discrete.thy Domain.thy Fix.ML Fix.thy Fixrec.thy \ |
32 Ffun.ML Ffun.thy HOLCF.ML HOLCF.thy Lift.ML Lift.thy One.ML One.thy \ |
33 Ffun.ML Ffun.thy HOLCF.ML HOLCF.thy Lift.ML \ |
33 Pcpo.ML Pcpo.thy Porder.ML Porder.thy ROOT.ML Sprod.ML Sprod.thy \ |
34 Lift.thy One.ML One.thy Pcpo.ML Pcpo.thy Porder.ML Porder.thy \ |
34 Ssum.ML Ssum.thy Tr.ML Tr.thy Up.ML Pcpodef.thy pcpodef_package.ML \ |
35 ROOT.ML Sprod.ML Sprod.thy \ |
35 Up.thy adm_tac.ML cont_consts.ML cont_proc.ML fixrec_package.ML \ |
36 Ssum.ML Ssum.thy \ |
36 domain/axioms.ML domain/extender.ML domain/library.ML \ |
37 Tr.ML Tr.thy Up.ML \ |
37 domain/syntax.ML domain/theorems.ML holcf_logic.ML ex/Stream.thy \ |
38 Pcpodef.thy pcpodef_package.ML \ |
38 document/root.tex |
39 Up.thy adm_tac.ML cont_consts.ML cont_proc.ML fixrec_package.ML \ |
|
40 domain/axioms.ML domain/extender.ML domain/interface.ML \ |
|
41 domain/library.ML domain/syntax.ML domain/theorems.ML holcf_logic.ML \ |
|
42 ex/Stream.thy document/root.tex |
|
43 @$(ISATOOL) usedir -b -g true -r $(OUT)/HOL HOLCF |
39 @$(ISATOOL) usedir -b -g true -r $(OUT)/HOL HOLCF |
44 |
40 |
45 |
41 |
46 ## HOLCF-IMP |
42 ## HOLCF-IMP |
47 |
43 |
97 IOA/meta_theory/TLS.ML IOA/meta_theory/LiveIOA.thy IOA/meta_theory/LiveIOA.ML \ |
93 IOA/meta_theory/TLS.ML IOA/meta_theory/LiveIOA.thy IOA/meta_theory/LiveIOA.ML \ |
98 IOA/meta_theory/Pred.thy IOA/meta_theory/Abstraction.thy \ |
94 IOA/meta_theory/Pred.thy IOA/meta_theory/Abstraction.thy \ |
99 IOA/meta_theory/Abstraction.ML \ |
95 IOA/meta_theory/Abstraction.ML \ |
100 IOA/meta_theory/Simulations.thy IOA/meta_theory/Simulations.ML \ |
96 IOA/meta_theory/Simulations.thy IOA/meta_theory/Simulations.ML \ |
101 IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/SimCorrectness.ML \ |
97 IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/SimCorrectness.ML \ |
102 IOA/meta_theory/ioa_syn.ML IOA/meta_theory/ioa_package.ML |
98 IOA/meta_theory/ioa_package.ML |
103 @cd IOA; $(ISATOOL) usedir -b $(OUT)/HOLCF IOA |
99 @cd IOA; $(ISATOOL) usedir -b $(OUT)/HOLCF IOA |
104 |
100 |
105 |
101 |
106 ## IOA-ABP |
102 ## IOA-ABP |
107 |
103 |