equal
deleted
inserted
replaced
15 Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \ |
15 Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \ |
16 Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \ |
16 Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \ |
17 Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy \ |
17 Up1.thy Up2.thy Up3.thy Fix.thy ccc1.thy \ |
18 One.thy Tr.thy\ |
18 One.thy Tr.thy\ |
19 Discrete0.thy Discrete1.thy Discrete.thy\ |
19 Discrete0.thy Discrete1.thy Discrete.thy\ |
20 Lift1.thy Lift2.thy Lift3.thy HOLCF.thy |
20 Lift1.thy Lift2.thy Lift3.thy HOLCF.thy |
21 |
21 |
22 ONLYTHYS = Lift.thy |
22 ONLYTHYS = Lift.thy |
23 |
23 |
24 FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML) |
24 FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML) \ |
|
25 ax_ops/holcflogic.ML ax_ops/thy_axioms.ML \ |
|
26 ax_ops/thy_ops.ML ax_ops/thy_syntax.ML \ |
|
27 domain/library.ML domain/syntax.ML domain/axioms.ML \ |
|
28 domain/theorems.ML domain/extender.ML domain/interface.ML |
25 |
29 |
26 $(OUT)/HOLCF: $(OUT)/HOL $(FILES) |
30 $(OUT)/HOLCF: $(OUT)/HOL $(FILES) |
27 @$(ISATOOL) usedir -b -c $(OUT)/HOL HOLCF |
31 @$(ISATOOL) usedir -b -c $(OUT)/HOL HOLCF |
28 @chmod -w $@ |
32 @chmod -w $@ |
29 |
33 |