src/HOL/IsaMakefile
changeset 43930 cb7914f6e9b3
parent 43927 3a87cb597832
parent 43925 f651cb053927
child 43931 c92df8144681
equal deleted inserted replaced
43929:61d432e51aff 43930:cb7914f6e9b3
   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 \