7 ## targets |
7 ## targets |
8 |
8 |
9 default: HOL |
9 default: HOL |
10 images: HOL HOL-Real TLA |
10 images: HOL HOL-Real TLA |
11 test: HOL-Isar_examples HOL-Induct HOL-ex HOL-Subst HOL-IMP HOL-IMPP \ |
11 test: HOL-Isar_examples HOL-Induct HOL-ex HOL-Subst HOL-IMP HOL-IMPP \ |
12 HOL-Hoare HOL-Lex HOL-Algebra HOL-Auth HOL-UNITY HOL-Modelcheck \ |
12 HOL-NumberTheory HOL-Hoare HOL-Lex HOL-Algebra \ |
|
13 HOL-Auth HOL-UNITY HOL-Modelcheck \ |
13 HOL-Lambda HOL-Prolog HOL-W0 HOL-MiniML HOL-BCV HOL-MicroJava \ |
14 HOL-Lambda HOL-Prolog HOL-W0 HOL-MiniML HOL-BCV HOL-MicroJava \ |
14 HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \ |
15 HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \ |
15 HOL-AxClasses-Tutorial HOL-Real-ex \ |
16 HOL-AxClasses-Tutorial HOL-Real-ex \ |
16 HOL-Real-HahnBanach TLA-Inc TLA-Buffer TLA-Memory |
17 HOL-Real-HahnBanach TLA-Inc TLA-Buffer TLA-Memory |
17 |
18 |
46 $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml \ |
47 $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml \ |
47 $(SRC)/TFL/thry.sig $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig \ |
48 $(SRC)/TFL/thry.sig $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig \ |
48 $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml \ |
49 $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml \ |
49 Arith.ML Arith.thy Calculation.thy Datatype.thy Divides.ML \ |
50 Arith.ML Arith.thy Calculation.thy Datatype.thy Divides.ML \ |
50 Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy \ |
51 Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy \ |
51 HOL.ML HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML \ |
52 HOL.ML HOL.thy HOL_lemmas.ML Inductive.thy \ |
52 Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML \ |
53 Integ/Bin.ML Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy \ |
53 Integ/IntArith.thy Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML \ |
54 Integ/IntArith.ML Integ/IntArith.thy \ |
|
55 Integ/IntPower.ML Integ/IntPower.thy \ |
|
56 Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML \ |
54 Integ/Int.thy Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML \ |
57 Integ/Int.thy Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML \ |
55 Integ/NatBin.thy Integ/NatSimprocs.thy Integ/NatSimprocs.ML \ |
58 Integ/NatBin.thy Integ/NatSimprocs.thy Integ/NatSimprocs.ML \ |
56 Integ/int_arith1.ML Integ/int_arith2.ML Integ/nat_simprocs.ML \ |
59 Integ/int_arith1.ML Integ/int_arith2.ML Integ/nat_simprocs.ML \ |
57 Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML Map.thy Nat.ML \ |
60 Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML Map.thy Nat.ML \ |
58 Nat.thy NatDef.ML NatDef.thy Numeral.thy Option.ML Option.thy Ord.ML \ |
61 Nat.thy NatDef.ML NatDef.thy Numeral.thy Option.ML Option.thy Ord.ML \ |
163 |
166 |
164 $(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy IMPP/Com.ML \ |
167 $(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy IMPP/Com.ML \ |
165 IMPP/Natural.thy IMPP/Natural.ML IMPP/Hoare.thy IMPP/Hoare.ML \ |
168 IMPP/Natural.thy IMPP/Natural.ML IMPP/Hoare.thy IMPP/Hoare.ML \ |
166 IMPP/Misc.thy IMPP/Misc.ML IMPP/EvenOdd.thy IMPP/EvenOdd.ML |
169 IMPP/Misc.thy IMPP/Misc.ML IMPP/EvenOdd.thy IMPP/EvenOdd.ML |
167 @$(ISATOOL) usedir $(OUT)/HOL IMPP |
170 @$(ISATOOL) usedir $(OUT)/HOL IMPP |
|
171 |
|
172 |
|
173 ## HOL-NumberTheory |
|
174 |
|
175 HOL-NumberTheory: HOL $(LOG)/HOL-NumberTheory.gz |
|
176 |
|
177 $(LOG)/HOL-NumberTheory.gz: $(OUT)/HOL \ |
|
178 NumberTheory/BijectionRel.ML NumberTheory/BijectionRel.thy \ |
|
179 NumberTheory/Chinese.ML NumberTheory/Chinese.thy \ |
|
180 NumberTheory/EulerFermat.ML NumberTheory/EulerFermat.thy \ |
|
181 NumberTheory/IntFact.ML NumberTheory/IntFact.thy \ |
|
182 NumberTheory/IntPrimes.ML NumberTheory/IntPrimes.thy \ |
|
183 NumberTheory/WilsonBij.ML NumberTheory/WilsonBij.thy \ |
|
184 NumberTheory/WilsonRuss.ML NumberTheory/WilsonRuss.thy \ |
|
185 NumberTheory/ROOT.ML |
|
186 @$(ISATOOL) usedir $(OUT)/HOL NumberTheory |
168 |
187 |
169 |
188 |
170 ## HOL-Hoare |
189 ## HOL-Hoare |
171 |
190 |
172 HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz |
191 HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz |