118 Tools/typedef_package.ML Transitive_Closure.ML Transitive_Closure.thy \ |
118 Tools/typedef_package.ML Transitive_Closure.ML Transitive_Closure.thy \ |
119 Typedef.thy Wellfounded_Recursion.thy Wellfounded_Relations.thy \ |
119 Typedef.thy Wellfounded_Recursion.thy Wellfounded_Relations.thy \ |
120 antisym_setup.ML arith_data.ML blastdata.ML cladata.ML \ |
120 antisym_setup.ML arith_data.ML blastdata.ML cladata.ML \ |
121 document/root.tex hologic.ML simpdata.ML ResAtpMethods.thy \ |
121 document/root.tex hologic.ML simpdata.ML ResAtpMethods.thy \ |
122 Tools/res_atp_provers.ML Tools/res_atp_methods.ML \ |
122 Tools/res_atp_provers.ML Tools/res_atp_methods.ML \ |
123 Tools/res_hol_clause.ML |
123 Tools/res_hol_clause.ML \ |
|
124 Tools/function_package/fundef_common.ML \ |
|
125 Tools/function_package/fundef_lib.ML \ |
|
126 Tools/function_package/context_tree.ML \ |
|
127 Tools/function_package/fundef_prep.ML \ |
|
128 Tools/function_package/fundef_proof.ML \ |
|
129 Tools/function_package/termination.ML \ |
|
130 Tools/function_package/fundef_package.ML \ |
|
131 Tools/function_package/auto_term.ML \ |
|
132 Tools/function_package/fundef_datatype.ML \ |
|
133 FunDef.thy Accessible_Part.thy |
124 @$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL |
134 @$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL |
125 |
135 |
126 |
136 |
127 ## HOL-Complex-HahnBanach |
137 ## HOL-Complex-HahnBanach |
128 |
138 |
182 |
192 |
183 ## HOL-Library |
193 ## HOL-Library |
184 |
194 |
185 HOL-Library: HOL $(LOG)/HOL-Library.gz |
195 HOL-Library: HOL $(LOG)/HOL-Library.gz |
186 |
196 |
187 $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \ |
197 $(LOG)/HOL-Library.gz: $(OUT)/HOL \ |
188 Library/SetsAndFunctions.thy Library/BigO.thy \ |
198 Library/SetsAndFunctions.thy Library/BigO.thy \ |
189 Library/EfficientNat.thy Library/ExecutableSet.thy Library/ExecutableRat.thy \ |
199 Library/EfficientNat.thy Library/ExecutableSet.thy Library/ExecutableRat.thy \ |
190 Library/FuncSet.thy Library/Library.thy \ |
200 Library/FuncSet.thy Library/Library.thy \ |
191 Library/List_Prefix.thy Library/Multiset.thy Library/NatPair.thy \ |
201 Library/List_Prefix.thy Library/Multiset.thy Library/NatPair.thy \ |
192 Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \ |
202 Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \ |
478 |
488 |
479 ## HOL-Lambda |
489 ## HOL-Lambda |
480 |
490 |
481 HOL-Lambda: HOL $(LOG)/HOL-Lambda.gz |
491 HOL-Lambda: HOL $(LOG)/HOL-Lambda.gz |
482 |
492 |
483 $(LOG)/HOL-Lambda.gz: $(OUT)/HOL Library/Accessible_Part.thy \ |
493 $(LOG)/HOL-Lambda.gz: $(OUT)/HOL \ |
484 Lambda/Commutation.thy Lambda/Eta.thy Lambda/InductTermi.thy Lambda/Lambda.thy \ |
494 Lambda/Commutation.thy Lambda/Eta.thy Lambda/InductTermi.thy Lambda/Lambda.thy \ |
485 Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy \ |
495 Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy \ |
486 Lambda/ParRed.thy Lambda/StrongNorm.thy Lambda/Type.thy \ |
496 Lambda/ParRed.thy Lambda/StrongNorm.thy Lambda/Type.thy \ |
487 Lambda/WeakNorm.thy Lambda/ROOT.ML \ |
497 Lambda/WeakNorm.thy Lambda/ROOT.ML \ |
488 Lambda/document/root.bib Lambda/document/root.tex |
498 Lambda/document/root.bib Lambda/document/root.tex |
738 |
748 |
739 ## HOL-Nominal-Examples |
749 ## HOL-Nominal-Examples |
740 |
750 |
741 HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz |
751 HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz |
742 |
752 |
743 $(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal Library/Accessible_Part.thy \ |
753 $(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal \ |
744 Nominal/Examples/ROOT.ML Nominal/Examples/CR.thy Nominal/Examples/Class.thy \ |
754 Nominal/Examples/ROOT.ML Nominal/Examples/CR.thy Nominal/Examples/Class.thy \ |
745 Nominal/Examples/Fsub.thy Nominal/Examples/Lambda_mu.thy \ |
755 Nominal/Examples/Fsub.thy Nominal/Examples/Lambda_mu.thy \ |
746 Nominal/Examples/Iteration.thy Nominal/Examples/Lam_substs.thy \ |
756 Nominal/Examples/Iteration.thy Nominal/Examples/Lam_substs.thy \ |
747 Nominal/Examples/Recursion.thy Nominal/Examples/SN.thy \ |
757 Nominal/Examples/Recursion.thy Nominal/Examples/SN.thy \ |
748 Nominal/Examples/Weakening.thy |
758 Nominal/Examples/Weakening.thy |