Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/IsaMakefile
changeset 9436 62bb04ab4b01
parent 9381 a0491eed2270
child 9456 880794f48ce6
equal deleted inserted replaced
9435:c3a13a7d4424 9436:62bb04ab4b01 
     6 
     6 
     7 ## targets
 
     7 ## targets
 
     8 
     8 
     9 default: HOL
 
     9 default: HOL
 
    10 images: HOL HOL-Real TLA
 
    10 images: HOL HOL-Real TLA
 
    11 test: HOL-Subst HOL-Induct HOL-IMP HOL-IMPP HOL-Hoare HOL-Lex HOL-Algebra \
 
    11 test: HOL-Isar_examples HOL-Induct HOL-ex HOL-Subst HOL-IMP HOL-IMPP \
 
    12   HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-Prolog HOL-W0 HOL-MiniML \
 
    12   HOL-Hoare HOL-Lex HOL-Algebra HOL-Auth HOL-UNITY HOL-Modelcheck \
 
    13   HOL-BCV HOL-MicroJava HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
 
    13   HOL-Lambda HOL-Prolog HOL-W0 HOL-MiniML HOL-BCV HOL-MicroJava \
 
    14   HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples HOL-Real-ex \
 
    14   HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
 
       
    15   HOL-AxClasses-Tutorial HOL-Quot HOL-Real-ex \
 
    15   HOL-Real-HahnBanach TLA-Inc TLA-Buffer TLA-Memory
 
    16   HOL-Real-HahnBanach TLA-Inc TLA-Buffer TLA-Memory
 
    16 
    17 
    17 all: images test
 
    18 all: images test
 
    18 
    19 
    19 
    20 
    29 HOL: Pure $(OUT)/HOL
 
    30 HOL: Pure $(OUT)/HOL
 
    30 
    31 
    31 Pure:
 
    32 Pure:
 
    32 	@cd $(SRC)/Pure; $(ISATOOL) make Pure
 
    33 	@cd $(SRC)/Pure; $(ISATOOL) make Pure
 
    33 
    34 
    34 $(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \
 
    35 $(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML		\
 
    35   $(SRC)/Provers/Arith/cancel_sums.ML		\
 
    36   $(SRC)/Provers/Arith/cancel_sums.ML					\
 
    36   $(SRC)/Provers/Arith/assoc_fold.ML		\
 
    37   $(SRC)/Provers/Arith/assoc_fold.ML					\
 
    37   $(SRC)/Provers/Arith/combine_numerals.ML	\
 
    38   $(SRC)/Provers/Arith/combine_numerals.ML				\
 
    38   $(SRC)/Provers/Arith/cancel_numerals.ML	\
 
    39   $(SRC)/Provers/Arith/cancel_numerals.ML				\
 
    39   $(SRC)/Provers/Arith/fast_lin_arith.ML \
 
    40   $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML	\
 
    40   $(SRC)/Provers/blast.ML $(SRC)/Provers/make_elim.ML \
 
    41   $(SRC)/Provers/make_elim.ML $(SRC)/Provers/clasimp.ML			\
 
    41   $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
 
    42   $(SRC)/Provers/classical.ML $(SRC)/Provers/hypsubst.ML		\
 
    42   $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
 
    43   $(SRC)/Provers/simplifier.ML $(SRC)/Provers/split_paired_all.ML	\
 
    43   $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \
 
    44   $(SRC)/Provers/splitter.ML $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml	\
 
    44   $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml $(SRC)/TFL/rules.sml \
 
    45   $(SRC)/TFL/rules.sml $(SRC)/TFL/rules.sig $(SRC)/TFL/tfl.sig		\
 
    45   $(SRC)/TFL/rules.sig $(SRC)/TFL/tfl.sig $(SRC)/TFL/tfl.sml \
 
    46   $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml		\
 
    46   $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sig \
 
    47   $(SRC)/TFL/thry.sig $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig	\
 
    47   $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig $(SRC)/TFL/usyntax.sml \
 
    48   $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml	\
 
    48   $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml Arith.ML Arith.thy \
 
    49   Arith.ML Arith.thy Calculation.thy Datatype.thy Divides.ML		\
 
    49   Calculation.thy Datatype.thy Divides.ML Divides.thy Finite.ML \
 
    50   Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy	\
 
    50   Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \
 
    51   HOL.ML HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML		\
 
    51   HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
 
    52   Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML	\
 
    52   Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML Integ/IntArith.thy \
 
    53   Integ/IntArith.thy Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML	\
 
    53   Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML Integ/Int.thy \
 
    54   Integ/Int.thy Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML	\
 
    54   Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML Integ/NatBin.thy \
 
    55   Integ/NatBin.thy Integ/NatSimprocs.thy Integ/NatSimprocs.ML		\
 
    55   Integ/NatSimprocs.thy Integ/NatSimprocs.ML \
 
    56   Integ/int_arith1.ML Integ/int_arith2.ML Integ/nat_simprocs.ML         \
 
    56   Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML \
 
    57   Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML Map.thy Nat.ML        \
 
    57   Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy Numeral.thy Option.ML \
 
    58   Nat.thy NatDef.ML NatDef.thy Numeral.thy Option.ML Option.thy Ord.ML  \
 
    58   Option.thy Ord.ML Ord.thy Power.ML Power.thy PreList.thy Prod.ML \
 
    59   Ord.thy Power.ML Power.thy PreList.thy Prod.ML Prod.thy ROOT.ML       \
 
    59   Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \
 
    60   Recdef.thy Record.thy RelPow.ML RelPow.thy Relation.ML Relation.thy   \
 
    60   Relation.ML Relation.thy Set.ML Set.thy SetInterval.ML SetInterval.thy \
 
    61   Set.ML Set.thy SetInterval.ML	SetInterval.thy String.thy              \
 
    61   String.thy SVC_Oracle.ML \
 
    62   SVC_Oracle.ML SVC_Oracle.thy Sum.ML Sum.thy Tools/datatype_aux.ML     \
 
    62   SVC_Oracle.thy Sum.ML Sum.thy Tools/datatype_aux.ML \
 
    63   Tools/datatype_abs_proofs.ML Tools/datatype_package.ML Tools/datatype_prop.ML	\
 
    63   Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
 
    64   Tools/datatype_rep_proofs.ML Tools/induct_method.ML			\
 
    64   Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
 
    65   Tools/inductive_package.ML Tools/numeral_syntax.ML			\
 
    65   Tools/induct_method.ML Tools/inductive_package.ML \
 
    66   Tools/primrec_package.ML Tools/recdef_package.ML			\
 
    66   Tools/numeral_syntax.ML Tools/primrec_package.ML \
 
    67   Tools/record_package.ML Tools/svc_funcs.ML Tools/typedef_package.ML	\
 
    67   Tools/recdef_package.ML Tools/record_package.ML Tools/svc_funcs.ML \
 
    68   Trancl.ML Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML	\
 
    68   Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
 
    69   WF.thy WF_Rel.ML WF_Rel.thy arith_data.ML blastdata.ML cladata.ML	\
 
    69   Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy blastdata.ML \
 
    70   equalities.ML equalities.thy hologic.ML mono.ML mono.thy simpdata.ML	\
 
    70   cladata.ML equalities.ML equalities.thy hologic.ML mono.ML mono.thy \
 
    71   subset.ML subset.thy thy_syntax.ML
 
    71   simpdata.ML subset.ML subset.thy thy_syntax.ML
 
       
    72 	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
 
    72 	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
 
    73 
    73 
    74 
    74 
    75 ## HOL-Real
 
    75 ## HOL-Real
 
    76 
    76 
    77 HOL-Real: HOL $(OUT)/HOL-Real
 
    77 HOL-Real: HOL $(OUT)/HOL-Real
 
    78 
    78 
    79 $(OUT)/HOL-Real: $(OUT)/HOL Real/Lubs.ML Real/Lubs.thy Real/PNat.ML \
 
    79 $(OUT)/HOL-Real: $(OUT)/HOL Real/Hyperreal/Filter.ML			\
 
    80   Real/PNat.thy Real/PRat.ML Real/PRat.thy Real/PReal.ML \
 
    80   Real/Hyperreal/Filter.thy Real/Hyperreal/HyperDef.ML			\
 
    81   Real/PReal.thy Real/RComplete.ML Real/RComplete.thy Real/Real.thy \
 
    81   Real/Hyperreal/HyperDef.thy Real/Hyperreal/Zorn.ML			\
 
    82   Real/RealDef.ML Real/RealDef.thy Real/RealOrd.ML Real/RealOrd.thy \
 
    82   Real/Hyperreal/Zorn.thy Real/Hyperreal/fuf.ML Real/Lubs.ML		\
 
    83   Real/RealAbs.ML Real/RealAbs.thy Real/ROOT.ML \
 
    83   Real/Lubs.thy Real/PNat.ML Real/PNat.thy Real/PRat.ML Real/PRat.thy	\
 
    84   Real/RealBin.ML Real/RealBin.thy Real/RealInt.ML Real/RealInt.thy \
 
    84   Real/PReal.ML Real/PReal.thy Real/RComplete.ML Real/RComplete.thy	\
 
    85   Real/RealPow.ML Real/RealPow.thy Real/Hyperreal/Filter.ML \
 
    85   Real/ROOT.ML Real/Real.thy Real/RealAbs.ML Real/RealAbs.thy		\
 
    86   Real/Hyperreal/Filter.thy Real/Hyperreal/fuf.ML \
 
    86   Real/RealArith.ML Real/RealArith.thy Real/RealBin.ML			\
 
    87   Real/Hyperreal/HyperDef.ML Real/Hyperreal/HyperDef.thy \
 
    87   Real/RealBin.thy Real/RealDef.ML Real/RealDef.thy Real/RealInt.ML	\
 
    88   Real/Hyperreal/Zorn.ML Real/Hyperreal/Zorn.thy
 
    88   Real/RealInt.thy Real/RealOrd.ML Real/RealOrd.thy Real/RealPow.ML	\
 
       
    89   Real/RealPow.thy Real/real_arith.ML
 
    89 	@cd Real; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Real
 
    90 	@cd Real; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Real
 
    90 
    91 
    91 
    92 
    92 ## HOL-Real-ex
 
    93 ## HOL-Real-ex
 
    93 
    94
isabelle