22 func.ML AC.thy AC.ML simpdata.ML Bool.thy Bool.ML \ |
22 func.ML AC.thy AC.ML simpdata.ML Bool.thy Bool.ML \ |
23 Sum.thy Sum.ML QPair.thy QPair.ML mono.ML Fixedpt.thy Fixedpt.ML \ |
23 Sum.thy Sum.ML QPair.thy QPair.ML mono.ML Fixedpt.thy Fixedpt.ML \ |
24 ind_syntax.ML intr_elim.ML indrule.ML inductive.ML coinductive.ML \ |
24 ind_syntax.ML intr_elim.ML indrule.ML inductive.ML coinductive.ML \ |
25 equalities.ML Perm.thy Perm.ML Rel.thy Rel.ML Trancl.thy Trancl.ML \ |
25 equalities.ML Perm.thy Perm.ML Rel.thy Rel.ML Trancl.thy Trancl.ML \ |
26 WF.thy WF.ML Order.thy Order.ML Ordinal.thy Ordinal.ML \ |
26 WF.thy WF.ML Order.thy Order.ML Ordinal.thy Ordinal.ML \ |
|
27 Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \ |
|
28 QUniv.thy QUniv.ML constructor.ML Datatype.thy Datatype.ML \ |
27 OrderArith.thy OrderArith.ML OrderType.thy OrderType.ML \ |
29 OrderArith.thy OrderArith.ML OrderType.thy OrderType.ML \ |
28 Cardinal.thy Cardinal.ML CardinalArith.thy CardinalArith.ML \ |
30 Cardinal.thy Cardinal.ML CardinalArith.thy CardinalArith.ML \ |
29 Cardinal_AC.thy Cardinal_AC.ML \ |
31 Cardinal_AC.thy Cardinal_AC.ML InfDatatype.thy InfDatatype.ML \ |
30 Zorn0.thy Zorn0.ML Zorn.thy Zorn.ML Nat.thy Nat.ML Fin.ML \ |
32 Zorn0.thy Zorn0.ML Zorn.thy Zorn.ML Nat.thy Nat.ML Fin.ML \ |
31 Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \ |
|
32 QUniv.thy QUniv.ML constructor.ML Datatype.ML \ |
|
33 List.ML ListFn.thy ListFn.ML |
33 List.ML ListFn.thy ListFn.ML |
34 |
34 |
35 IMP_FILES = IMP/ROOT.ML IMP/Aexp.ML IMP/Aexp.thy IMP/Assign.ML IMP/Assign.thy\ |
35 IMP_FILES = IMP/ROOT.ML IMP/Aexp.ML IMP/Aexp.thy IMP/Assign.ML IMP/Assign.thy\ |
36 IMP/Bexp.ML IMP/Bexp.thy IMP/Com.ML IMP/Com.thy IMP/Denotation.ML\ |
36 IMP/Bexp.ML IMP/Bexp.thy IMP/Com.ML IMP/Com.thy IMP/Denotation.ML\ |
37 IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy IMP/Evala0.thy\ |
37 IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy IMP/Evala0.thy\ |
44 ex/Enum.ML ex/Equiv.ML ex/Equiv.thy ex/Integ.ML ex/Integ.thy\ |
44 ex/Enum.ML ex/Equiv.ML ex/Equiv.thy ex/Integ.ML ex/Integ.thy\ |
45 ex/ListN.ML ex/LList.ML ex/LList_Eq.ML ex/LListFn.ML ex/LListFn.thy\ |
45 ex/ListN.ML ex/LList.ML ex/LList_Eq.ML ex/LListFn.ML ex/LListFn.thy\ |
46 ex/misc.ML ex/ParContract.ML ex/Primrec0.ML ex/Primrec0.thy\ |
46 ex/misc.ML ex/ParContract.ML ex/Primrec0.ML ex/Primrec0.thy\ |
47 ex/Prop.ML ex/PropLog.ML ex/PropLog.thy ex/Ramsey.ML ex/Ramsey.thy\ |
47 ex/Prop.ML ex/PropLog.ML ex/PropLog.thy ex/Ramsey.ML ex/Ramsey.thy\ |
48 ex/Rmap.ML ex/Term.ML ex/TermFn.ML ex/TermFn.thy \ |
48 ex/Rmap.ML ex/Term.ML ex/TermFn.ML ex/TermFn.thy \ |
49 ex/Ntree.ML ex/Ntree.thy \ |
49 ex/Ntree.ML ex/Brouwer.ML \ |
50 ex/TF.ML ex/TF_Fn.ML ex/TF_Fn.thy ex/twos_compl.ML |
50 ex/TF.ML ex/TF_Fn.ML ex/TF_Fn.thy ex/twos_compl.ML |
51 |
51 |
52 #Uses cp rather than make_database because Poly/ML allows only 3 levels |
52 #Uses cp rather than make_database because Poly/ML allows only 3 levels |
53 $(BIN)/ZF: $(BIN)/FOL $(FILES) |
53 $(BIN)/ZF: $(BIN)/FOL $(FILES) |
54 case "$(COMP)" in \ |
54 case "$(COMP)" in \ |
60 esac |
60 esac |
61 |
61 |
62 $(BIN)/FOL: |
62 $(BIN)/FOL: |
63 cd ../FOL; $(MAKE) |
63 cd ../FOL; $(MAKE) |
64 |
64 |
65 test: ex/ROOT.ML $(BIN)/ZF $(IMP_FILES) $(EX_FILES) |
65 #Directory IMP also tests the system |
|
66 #Load ex/ROOT.ML last since it creates the file "test" |
|
67 test: $(BIN)/ZF $(IMP_FILES) $(EX_FILES) |
66 case "$(COMP)" in \ |
68 case "$(COMP)" in \ |
67 poly*) echo 'use"IMP/ROOT.ML"; use"ex/ROOT.ML"; quit();' | \ |
69 poly*) echo 'use"IMP/ROOT.ML"; use"ex/ROOT.ML"; quit();' | \ |
68 $(COMP) $(BIN)/ZF ;;\ |
70 $(COMP) $(BIN)/ZF ;;\ |
69 sml*) echo 'use"IMP/ROOT.ML"; use"ex/ROOT.ML";' | $(BIN)/ZF;;\ |
71 sml*) echo 'use"IMP/ROOT.ML"; use"ex/ROOT.ML";' | $(BIN)/ZF;;\ |
70 *) echo Bad value for ISABELLECOMP: \ |
72 *) echo Bad value for ISABELLECOMP: \ |