81 $(SRC)/Provers/splitter.ML $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \ |
81 $(SRC)/Provers/splitter.ML $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML \ |
82 $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \ |
82 $(SRC)/TFL/rules.ML $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \ |
83 $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \ |
83 $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \ |
84 Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides_lemmas.ML \ |
84 Datatype.thy Datatype_Universe.ML Datatype_Universe.thy Divides_lemmas.ML \ |
85 Divides.thy Extraction.thy Finite_Set.ML Finite_Set.thy \ |
85 Divides.thy Extraction.thy Finite_Set.ML Finite_Set.thy \ |
86 Fun.ML Fun.thy Gfp.ML Gfp.thy \ |
86 Fun.thy Gfp.ML Gfp.thy \ |
87 Hilbert_Choice.thy Hilbert_Choice_lemmas.ML HOL.ML \ |
87 Hilbert_Choice.thy Hilbert_Choice_lemmas.ML HOL.ML \ |
88 HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \ |
88 HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \ |
89 Integ/Equiv.ML Integ/Equiv.thy Integ/int.ML Integ/Int.thy \ |
89 Integ/Equiv.ML Integ/Equiv.thy Integ/int.ML Integ/Int.thy \ |
90 Integ/IntArith.ML Integ/IntArith.thy Integ/IntDef.ML Integ/IntDef.thy \ |
90 Integ/IntArith.ML Integ/IntArith.thy Integ/IntDef.ML Integ/IntDef.thy \ |
91 Integ/IntDiv.thy Integ/IntPower.ML Integ/IntPower.thy \ |
91 Integ/IntDiv.thy Integ/IntPower.ML Integ/IntPower.thy \ |
195 ## HOL-Library |
195 ## HOL-Library |
196 |
196 |
197 HOL-Library: HOL $(LOG)/HOL-Library.gz |
197 HOL-Library: HOL $(LOG)/HOL-Library.gz |
198 |
198 |
199 $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \ |
199 $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \ |
200 Library/Library.thy Library/List_Prefix.thy Library/Multiset.thy \ |
200 Library/FuncSet.thy Library/Library.thy \ |
|
201 Library/List_Prefix.thy Library/Multiset.thy \ |
201 Library/Permutation.thy Library/Primes.thy \ |
202 Library/Permutation.thy Library/Primes.thy \ |
202 Library/Quotient.thy Library/Ring_and_Field.thy \ |
203 Library/Quotient.thy Library/Ring_and_Field.thy \ |
203 Library/Ring_and_Field_Example.thy Library/Nat_Infinity.thy \ |
204 Library/Ring_and_Field_Example.thy Library/Nat_Infinity.thy \ |
204 Library/README.html Library/Continuity.thy \ |
205 Library/README.html Library/Continuity.thy \ |
205 Library/Nested_Environment.thy Library/Rational_Numbers.thy \ |
206 Library/Nested_Environment.thy Library/Rational_Numbers.thy \ |
273 ## HOL-GroupTheory |
274 ## HOL-GroupTheory |
274 |
275 |
275 HOL-GroupTheory: HOL $(LOG)/HOL-GroupTheory.gz |
276 HOL-GroupTheory: HOL $(LOG)/HOL-GroupTheory.gz |
276 |
277 |
277 $(LOG)/HOL-GroupTheory.gz: $(OUT)/HOL \ |
278 $(LOG)/HOL-GroupTheory.gz: $(OUT)/HOL \ |
278 Library/Primes.thy \ |
279 Library/Primes.thy Library/FuncSet.thy \ |
279 GroupTheory/Bij.thy GroupTheory/Bij.ML\ |
280 GroupTheory/Bij.thy \ |
280 GroupTheory/Coset.thy GroupTheory/Coset.ML\ |
281 GroupTheory/Coset.thy \ |
281 GroupTheory/DirProd.thy GroupTheory/DirProd.ML\ |
282 GroupTheory/Exponent.thy \ |
282 GroupTheory/Exponent.thy GroupTheory/Exponent.ML\ |
283 GroupTheory/Group.thy \ |
283 GroupTheory/FactGroup.thy GroupTheory/FactGroup.ML\ |
284 GroupTheory/Ring.thy \ |
284 GroupTheory/Group.thy GroupTheory/Group.ML\ |
285 GroupTheory/Sylow.thy \ |
285 GroupTheory/Homomorphism.thy GroupTheory/Homomorphism.ML\ |
286 GroupTheory/ROOT.ML \ |
286 GroupTheory/PiSets.ML GroupTheory/PiSets.thy \ |
287 GroupTheory/document/root.tex |
287 GroupTheory/Ring.thy GroupTheory/Ring.ML\ |
288 @$(ISATOOL) usedir -g true $(OUT)/HOL GroupTheory |
288 GroupTheory/RingConstr.thy GroupTheory/RingConstr.ML\ |
|
289 GroupTheory/Sylow.thy GroupTheory/Sylow.ML\ |
|
290 GroupTheory/ROOT.ML |
|
291 @$(ISATOOL) usedir $(OUT)/HOL GroupTheory |
|
292 |
289 |
293 |
290 |
294 ## HOL-Hoare |
291 ## HOL-Hoare |
295 |
292 |
296 HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz |
293 HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz |