equal
deleted
inserted
replaced
178 |
178 |
179 HOL-Library: HOL $(LOG)/HOL-Library.gz |
179 HOL-Library: HOL $(LOG)/HOL-Library.gz |
180 |
180 |
181 $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \ |
181 $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \ |
182 Library/Library.thy Library/List_Prefix.thy Library/Multiset.thy \ |
182 Library/Library.thy Library/List_Prefix.thy Library/Multiset.thy \ |
183 Library/Quotient.thy Library/Ring_and_Field.thy \ |
183 Library/Permutation.thy Library/Quotient.thy Library/Ring_and_Field.thy \ |
184 Library/Ring_and_Field_Example.thy Library/README.html \ |
184 Library/Ring_and_Field_Example.thy Library/README.html \ |
185 Library/Nested_Environment.thy Library/Rational_Numbers.thy Library/ROOT.ML \ |
185 Library/Nested_Environment.thy Library/Rational_Numbers.thy Library/ROOT.ML \ |
186 Library/While_Combinator.thy |
186 Library/While_Combinator.thy |
187 @$(ISATOOL) usedir $(OUT)/HOL Library |
187 @$(ISATOOL) usedir $(OUT)/HOL Library |
188 |
188 |
203 HOL-Induct: HOL $(LOG)/HOL-Induct.gz |
203 HOL-Induct: HOL $(LOG)/HOL-Induct.gz |
204 |
204 |
205 $(LOG)/HOL-Induct.gz: $(OUT)/HOL \ |
205 $(LOG)/HOL-Induct.gz: $(OUT)/HOL \ |
206 Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \ |
206 Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \ |
207 Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \ |
207 Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \ |
208 Induct/LList.ML Induct/LList.thy Induct/Mutil.thy Induct/Perm.ML \ |
208 Induct/LList.ML Induct/LList.thy Induct/Mutil.thy \ |
209 Induct/Perm.thy Induct/PropLog.ML Induct/PropLog.thy Induct/ROOT.ML \ |
209 Induct/PropLog.ML Induct/PropLog.thy Induct/ROOT.ML \ |
210 Induct/Sexp.ML Induct/Sexp.thy Induct/Sigma_Algebra.thy \ |
210 Induct/Sexp.ML Induct/Sexp.thy Induct/Sigma_Algebra.thy \ |
211 Induct/SList.ML Induct/SList.thy Induct/ABexp.thy Induct/Term.thy \ |
211 Induct/SList.ML Induct/SList.thy Induct/ABexp.thy Induct/Term.thy \ |
212 Induct/Tree.thy Induct/document/root.tex |
212 Induct/Tree.thy Induct/document/root.tex |
213 @$(ISATOOL) usedir $(OUT)/HOL Induct |
213 @$(ISATOOL) usedir $(OUT)/HOL Induct |
214 |
214 |
237 ## HOL-NumberTheory |
237 ## HOL-NumberTheory |
238 |
238 |
239 HOL-NumberTheory: HOL $(LOG)/HOL-NumberTheory.gz |
239 HOL-NumberTheory: HOL $(LOG)/HOL-NumberTheory.gz |
240 |
240 |
241 $(LOG)/HOL-NumberTheory.gz: $(OUT)/HOL \ |
241 $(LOG)/HOL-NumberTheory.gz: $(OUT)/HOL \ |
242 NumberTheory/Fib.ML NumberTheory/Fib.thy NumberTheory/Primes.thy \ |
242 Library/Permutation.thy NumberTheory/Fib.thy NumberTheory/Primes.thy \ |
243 NumberTheory/Factorization.ML NumberTheory/Factorization.thy \ |
243 NumberTheory/Factorization.thy NumberTheory/BijectionRel.thy \ |
244 NumberTheory/BijectionRel.ML NumberTheory/BijectionRel.thy \ |
244 NumberTheory/Chinese.thy NumberTheory/EulerFermat.thy \ |
245 NumberTheory/Chinese.ML NumberTheory/Chinese.thy \ |
245 NumberTheory/IntFact.thy NumberTheory/IntPrimes.thy \ |
246 NumberTheory/EulerFermat.ML NumberTheory/EulerFermat.thy \ |
246 NumberTheory/WilsonBij.thy NumberTheory/WilsonRuss.thy \ |
247 NumberTheory/IntFact.ML NumberTheory/IntFact.thy \ |
|
248 NumberTheory/IntPrimes.ML NumberTheory/IntPrimes.thy \ |
|
249 NumberTheory/WilsonBij.ML NumberTheory/WilsonBij.thy \ |
|
250 NumberTheory/WilsonRuss.ML NumberTheory/WilsonRuss.thy \ |
|
251 NumberTheory/ROOT.ML |
247 NumberTheory/ROOT.ML |
252 @$(ISATOOL) usedir $(OUT)/HOL NumberTheory |
248 @$(ISATOOL) usedir $(OUT)/HOL NumberTheory |
253 |
249 |
254 |
250 |
255 ## HOL-Hoare |
251 ## HOL-Hoare |