441 $(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML \ |
441 $(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML \ |
442 Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy \ |
442 Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy \ |
443 Library/AssocList.thy Library/BigO.thy Library/Binomial.thy \ |
443 Library/AssocList.thy Library/BigO.thy Library/Binomial.thy \ |
444 Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy \ |
444 Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy \ |
445 Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy \ |
445 Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy \ |
446 Library/Code_Char_ord.thy Library/Code_Integer.thy Library/Code_Natural.thy \ |
446 Library/Code_Char_ord.thy Library/Code_Integer.thy \ |
447 Library/Code_Prolog.thy Tools/Predicate_Compile/code_prolog.ML \ |
447 Library/Code_Natural.thy Library/Code_Prolog.thy \ |
448 Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy \ |
448 Tools/Predicate_Compile/code_prolog.ML Library/ContNotDenum.thy \ |
449 Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy \ |
449 Library/Continuity.thy Library/Convex.thy Library/Countable.thy \ |
450 Library/Dlist_Cset.thy \ |
450 Library/Diagonalize.thy Library/Dlist.thy Library/Dlist_Cset.thy \ |
451 Library/Efficient_Nat.thy Library/Eval_Witness.thy \ |
451 Library/Efficient_Nat.thy Library/Eval_Witness.thy \ |
452 Library/Executable_Set.thy Library/Extended_Reals.thy \ |
452 Library/Executable_Set.thy Library/Extended_Real.thy \ |
453 Library/Float.thy Library/Formal_Power_Series.thy \ |
453 Library/Extended_Nat.thy Library/Float.thy \ |
454 Library/Fraction_Field.thy Library/FrechetDeriv.thy Library/Cset.thy \ |
454 Library/Formal_Power_Series.thy Library/Fraction_Field.thy \ |
455 Library/FuncSet.thy Library/Function_Algebras.thy \ |
455 Library/FrechetDeriv.thy Library/Cset.thy Library/FuncSet.thy \ |
456 Library/Fundamental_Theorem_Algebra.thy Library/Glbs.thy \ |
456 Library/Function_Algebras.thy Library/Fundamental_Theorem_Algebra.thy \ |
457 Library/Indicator_Function.thy Library/Infinite_Set.thy \ |
457 Library/Glbs.thy Library/Indicator_Function.thy \ |
458 Library/Inner_Product.thy Library/Kleene_Algebra.thy \ |
458 Library/Infinite_Set.thy Library/Inner_Product.thy \ |
459 Library/LaTeXsugar.thy Library/Lattice_Algebras.thy \ |
459 Library/Kleene_Algebra.thy Library/LaTeXsugar.thy \ |
460 Library/Lattice_Syntax.thy Library/Library.thy Library/List_Cset.thy \ |
460 Library/Lattice_Algebras.thy Library/Lattice_Syntax.thy \ |
461 Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy \ |
461 Library/Library.thy Library/List_Cset.thy Library/List_Prefix.thy \ |
462 Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy \ |
462 Library/List_lexord.thy Library/Mapping.thy Library/Monad_Syntax.thy \ |
463 Library/Multiset.thy Library/Nat_Bijection.thy \ |
463 Library/More_List.thy Library/More_Set.thy Library/Multiset.thy \ |
464 Library/Nat_Infinity.thy Library/Nested_Environment.thy \ |
464 Library/Nat_Bijection.thy Library/Nested_Environment.thy \ |
465 Library/Numeral_Type.thy Library/OptionalSugar.thy \ |
465 Library/Numeral_Type.thy Library/OptionalSugar.thy \ |
466 Library/Order_Relation.thy Library/Permutation.thy \ |
466 Library/Order_Relation.thy Library/Permutation.thy \ |
467 Library/Permutations.thy Library/Poly_Deriv.thy \ |
467 Library/Permutations.thy Library/Poly_Deriv.thy \ |
468 Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy \ |
468 Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy \ |
469 Library/Preorder.thy Library/Product_Vector.thy \ |
469 Library/Preorder.thy Library/Product_Vector.thy \ |
478 Library/Reflection.thy Library/SML_Quickcheck.thy \ |
478 Library/Reflection.thy Library/SML_Quickcheck.thy \ |
479 Library/Sublist_Order.thy Library/Sum_of_Squares.thy \ |
479 Library/Sublist_Order.thy Library/Sum_of_Squares.thy \ |
480 Library/Sum_of_Squares/sos_wrapper.ML \ |
480 Library/Sum_of_Squares/sos_wrapper.ML \ |
481 Library/Sum_of_Squares/sum_of_squares.ML \ |
481 Library/Sum_of_Squares/sum_of_squares.ML \ |
482 Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy \ |
482 Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy \ |
483 Library/While_Combinator.thy Library/Zorn.thy \ |
483 Library/While_Combinator.thy Library/Zorn.thy \ |
484 $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML \ |
484 $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML \ |
485 Library/reflection.ML Library/reify_data.ML \ |
485 Library/reflection.ML Library/reify_data.ML \ |
486 Library/document/root.bib Library/document/root.tex |
486 Library/document/root.bib Library/document/root.tex |
487 @cd Library; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL-Library |
487 @cd Library; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL-Library |
488 |
488 |
552 |
552 |
553 |
553 |
554 ## HOL-Import |
554 ## HOL-Import |
555 |
555 |
556 IMPORTER_FILES = \ |
556 IMPORTER_FILES = \ |
557 Import/ImportRecorder.thy Import/HOL4Compat.thy \ |
557 Import/HOL4Compat.thy \ |
558 Import/HOLLightCompat.thy Import/HOL4Setup.thy Import/HOL4Syntax.thy \ |
558 Import/HOLLightCompat.thy Import/HOL4Setup.thy Import/HOL4Syntax.thy \ |
559 Import/MakeEqual.thy Import/ROOT.ML Import/hol4rews.ML \ |
559 Import/MakeEqual.thy Import/ROOT.ML Import/hol4rews.ML \ |
560 Import/import.ML Import/importrecorder.ML Import/import_syntax.ML \ |
560 Import/import.ML Import/import_syntax.ML \ |
561 Import/lazy_seq.ML Import/mono_scan.ML Import/mono_seq.ML \ |
561 Import/proof_kernel.ML Import/replay.ML Import/shuffler.ML \ |
562 Import/proof_kernel.ML Import/replay.ML Import/scan.ML Import/seq.ML \ |
|
563 Import/shuffler.ML Import/xml.ML Import/xmlconv.ML \ |
|
564 Library/ContNotDenum.thy Old_Number_Theory/Primes.thy |
562 Library/ContNotDenum.thy Old_Number_Theory/Primes.thy |
565 |
563 |
566 HOL-Import: HOL $(LOG)/HOL-Import.gz |
564 HOL-Import: HOL $(LOG)/HOL-Import.gz |
567 |
565 |
568 $(LOG)/HOL-Import.gz: $(OUT)/HOL $(IMPORTER_FILES) |
566 $(LOG)/HOL-Import.gz: $(OUT)/HOL $(IMPORTER_FILES) |
1200 Multivariate_Analysis/ROOT.ML \ |
1198 Multivariate_Analysis/ROOT.ML \ |
1201 Multivariate_Analysis/Real_Integration.thy \ |
1199 Multivariate_Analysis/Real_Integration.thy \ |
1202 Multivariate_Analysis/Topology_Euclidean_Space.thy \ |
1200 Multivariate_Analysis/Topology_Euclidean_Space.thy \ |
1203 Multivariate_Analysis/document/root.tex \ |
1201 Multivariate_Analysis/document/root.tex \ |
1204 Multivariate_Analysis/normarith.ML Library/Glbs.thy \ |
1202 Multivariate_Analysis/normarith.ML Library/Glbs.thy \ |
1205 Library/Extended_Reals.thy Library/Indicator_Function.thy \ |
1203 Library/Extended_Real.thy Library/Indicator_Function.thy \ |
1206 Library/Inner_Product.thy Library/Numeral_Type.thy Library/Convex.thy \ |
1204 Library/Inner_Product.thy Library/Numeral_Type.thy Library/Convex.thy \ |
1207 Library/FrechetDeriv.thy Library/Product_Vector.thy \ |
1205 Library/FrechetDeriv.thy Library/Product_Vector.thy \ |
1208 Library/Product_plus.thy |
1206 Library/Product_plus.thy |
1209 @cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Multivariate_Analysis |
1207 @cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Multivariate_Analysis |
1210 |
1208 |
1573 ## HOLCF-Library |
1571 ## HOLCF-Library |
1574 |
1572 |
1575 HOLCF-Library: HOLCF $(LOG)/HOLCF-Library.gz |
1573 HOLCF-Library: HOLCF $(LOG)/HOLCF-Library.gz |
1576 |
1574 |
1577 $(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \ |
1575 $(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \ |
1578 Library/Nat_Infinity.thy \ |
1576 Library/Extended_Nat.thy \ |
1579 HOLCF/Library/Defl_Bifinite.thy \ |
1577 HOLCF/Library/Defl_Bifinite.thy \ |
1580 HOLCF/Library/Bool_Discrete.thy \ |
1578 HOLCF/Library/Bool_Discrete.thy \ |
1581 HOLCF/Library/Char_Discrete.thy \ |
1579 HOLCF/Library/Char_Discrete.thy \ |
1582 HOLCF/Library/HOL_Cpo.thy \ |
1580 HOLCF/Library/HOL_Cpo.thy \ |
1583 HOLCF/Library/Int_Discrete.thy \ |
1581 HOLCF/Library/Int_Discrete.thy \ |
1627 ## HOLCF-FOCUS |
1625 ## HOLCF-FOCUS |
1628 |
1626 |
1629 HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz |
1627 HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz |
1630 |
1628 |
1631 $(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF HOLCF/FOCUS/ROOT.ML \ |
1629 $(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF HOLCF/FOCUS/ROOT.ML \ |
1632 Library/Nat_Infinity.thy \ |
1630 Library/Extended_Nat.thy \ |
1633 HOLCF/Library/Stream.thy \ |
1631 HOLCF/Library/Stream.thy \ |
1634 HOLCF/FOCUS/Fstreams.thy \ |
1632 HOLCF/FOCUS/Fstreams.thy \ |
1635 HOLCF/FOCUS/Fstream.thy \ |
1633 HOLCF/FOCUS/Fstream.thy \ |
1636 HOLCF/FOCUS/FOCUS.thy \ |
1634 HOLCF/FOCUS/FOCUS.thy \ |
1637 HOLCF/FOCUS/Stream_adm.thy \ |
1635 HOLCF/FOCUS/Stream_adm.thy \ |