src/ZF/IsaMakefile
author wenzelm
Thu Apr 26 15:42:04 2007 +0200 (2007-04-26)
changeset 22814 4cd25f1706bb
parent 17935 c6f1442ce949
child 23146 0bc590051d95
permissions -rw-r--r--
removed lagacy ML files;
wenzelm@2500
     1
#
wenzelm@2500
     2
# $Id$
wenzelm@2500
     3
#
wenzelm@2500
     4
# IsaMakefile for ZF
wenzelm@2500
     5
#
wenzelm@2500
     6
wenzelm@4518
     7
## targets
wenzelm@2500
     8
wenzelm@4518
     9
default: ZF
wenzelm@4518
    10
images: ZF
paulson@11479
    11
paulson@11479
    12
#Note: keep targets sorted
paulson@13225
    13
test: ZF-AC ZF-Coind ZF-Constructible ZF-IMP ZF-Induct ZF-Resid ZF-UNITY ZF-ex
wenzelm@4518
    14
all: images test
wenzelm@4518
    15
wenzelm@4518
    16
wenzelm@4518
    17
## global settings
wenzelm@4518
    18
wenzelm@4518
    19
SRC = $(ISABELLE_HOME)/src
wenzelm@3118
    20
OUT = $(ISABELLE_OUTPUT)
wenzelm@4447
    21
LOG = $(OUT)/log
wenzelm@2500
    22
wenzelm@4518
    23
wenzelm@4518
    24
## ZF
wenzelm@4518
    25
wenzelm@17821
    26
ZF: FOL $(OUT)/ZF$(ML_SUFFIX)
wenzelm@4518
    27
wenzelm@4518
    28
FOL:
wenzelm@4518
    29
	@cd $(SRC)/FOL; $(ISATOOL) make FOL
wenzelm@2500
    30
wenzelm@22814
    31
$(OUT)/ZF$(ML_SUFFIX): $(OUT)/FOL$(ML_SUFFIX) AC.thy Arith.thy			\
wenzelm@22814
    32
  ArithSimp.thy Bool.thy Cardinal.thy CardinalArith.thy Cardinal_AC.thy		\
wenzelm@22814
    33
  Datatype.thy Epsilon.thy Finite.thy Fixedpt.thy Inductive.thy			\
wenzelm@22814
    34
  InfDatatype.thy Integ/Bin.thy Integ/EquivClass.thy Integ/Int.thy		\
wenzelm@22814
    35
  Integ/IntArith.thy Integ/IntDiv.thy Integ/int_arith.ML List.thy		\
wenzelm@22814
    36
  Main.thy Main_ZFC.thy Nat.thy OrdQuant.thy Order.thy OrderArith.thy		\
wenzelm@22814
    37
  OrderType.thy Ordinal.thy Perm.thy QPair.thy QUniv.thy ROOT.ML Sum.thy	\
wenzelm@22814
    38
  Tools/cartprod.ML Tools/datatype_package.ML Tools/ind_cases.ML		\
wenzelm@22814
    39
  Tools/induct_tacs.ML Tools/inductive_package.ML				\
wenzelm@22814
    40
  Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML		\
wenzelm@22814
    41
  Trancl.thy Univ.thy WF.thy ZF.thy Zorn.thy arith_data.ML			\
wenzelm@22814
    42
  equalities.thy func.thy ind_syntax.ML pair.thy simpdata.ML upair.thy
wenzelm@6213
    43
	@$(ISATOOL) usedir -b -r $(OUT)/FOL ZF
wenzelm@2500
    44
wenzelm@2500
    45
wenzelm@4518
    46
## ZF-AC
wenzelm@2500
    47
wenzelm@4518
    48
ZF-AC: ZF $(LOG)/ZF-AC.gz
wenzelm@2500
    49
wenzelm@17821
    50
$(LOG)/ZF-AC.gz: $(OUT)/ZF$(ML_SUFFIX) \
paulson@12776
    51
  AC/ROOT.ML  AC/AC15_WO6.thy AC/AC16_WO4.thy \
paulson@12776
    52
  AC/AC16_lemmas.thy AC/AC17_AC1.thy AC/AC18_AC19.thy AC/AC7_AC9.thy \
paulson@12776
    53
  AC/AC_Equiv.thy AC/Cardinal_aux.thy \
paulson@12776
    54
  AC/DC.thy AC/HH.thy AC/Hartog.thy AC/WO1_AC.thy AC/WO1_WO7.thy \
paulson@15083
    55
  AC/WO2_AC16.thy AC/WO6_WO1.thy AC/document/root.bib AC/document/root.tex
paulson@15083
    56
	@$(ISATOOL) usedir -g true $(OUT)/ZF AC
wenzelm@2500
    57
wenzelm@2500
    58
paulson@11479
    59
## ZF-Coind
wenzelm@4518
    60
paulson@11479
    61
ZF-Coind: ZF $(LOG)/ZF-Coind.gz
wenzelm@2500
    62
wenzelm@17821
    63
$(LOG)/ZF-Coind.gz: $(OUT)/ZF$(ML_SUFFIX) Coind/Dynamic.thy \
paulson@12595
    64
  Coind/ECR.thy Coind/Language.thy Coind/Map.thy Coind/ROOT.ML \
paulson@12595
    65
  Coind/Static.thy Coind/Types.thy Coind/Values.thy
paulson@11479
    66
	@$(ISATOOL) usedir $(OUT)/ZF Coind
wenzelm@2500
    67
wenzelm@2500
    68
paulson@13225
    69
## ZF-Constructible
paulson@13225
    70
paulson@13225
    71
ZF-Constructible: ZF $(LOG)/ZF-Constructible.gz
paulson@13225
    72
wenzelm@17821
    73
$(LOG)/ZF-Constructible.gz: $(OUT)/ZF$(ML_SUFFIX)  Constructible/ROOT.ML \
paulson@13503
    74
  Constructible/Datatype_absolute.thy Constructible/DPow_absolute.thy\
paulson@13496
    75
  Constructible/Formula.thy Constructible/Internalize.thy \
paulson@13544
    76
  Constructible/AC_in_L.thy Constructible/Relative.thy \
paulson@13225
    77
  Constructible/L_axioms.thy    Constructible/Wellorderings.thy \
paulson@13318
    78
  Constructible/MetaExists.thy  Constructible/Normal.thy \
paulson@13634
    79
  Constructible/Rank.thy Constructible/Rank_Separation.thy \
paulson@13339
    80
  Constructible/Rec_Separation.thy Constructible/Separation.thy \
paulson@13494
    81
  Constructible/Satisfies_absolute.thy Constructible/WF_absolute.thy \
wenzelm@13296
    82
  Constructible/Reflection.thy  Constructible/WFrec.thy \
paulson@15083
    83
  Constructible/document/root.bib Constructible/document/root.tex
wenzelm@13427
    84
	@$(ISATOOL) usedir -g true $(OUT)/ZF Constructible
paulson@13225
    85
paulson@13225
    86
paulson@11479
    87
## ZF-IMP
paulson@11479
    88
paulson@11479
    89
ZF-IMP: ZF $(LOG)/ZF-IMP.gz
paulson@11479
    90
wenzelm@17821
    91
$(LOG)/ZF-IMP.gz: $(OUT)/ZF$(ML_SUFFIX) IMP/Com.thy IMP/Denotation.thy IMP/Equiv.thy \
wenzelm@12610
    92
  IMP/ROOT.ML IMP/document/root.bib IMP/document/root.tex
paulson@11479
    93
	@$(ISATOOL) usedir $(OUT)/ZF IMP
paulson@11479
    94
paulson@11479
    95
paulson@11479
    96
## ZF-Resid
paulson@11479
    97
paulson@11479
    98
ZF-Resid: ZF $(LOG)/ZF-Resid.gz
paulson@11479
    99
wenzelm@17821
   100
$(LOG)/ZF-Resid.gz: $(OUT)/ZF$(ML_SUFFIX) Resid/ROOT.ML \
paulson@12595
   101
  Resid/Confluence.thy  Resid/Redex.thy \
paulson@12595
   102
  Resid/Reduction.thy Resid/Residuals.thy Resid/Substitution.thy 
paulson@11479
   103
	@$(ISATOOL) usedir $(OUT)/ZF Resid
paulson@11479
   104
paulson@11479
   105
paulson@11479
   106
## ZF-UNITY
paulson@11479
   107
paulson@11479
   108
ZF-UNITY: ZF $(LOG)/ZF-UNITY.gz
paulson@11479
   109
wenzelm@17821
   110
$(LOG)/ZF-UNITY.gz: $(OUT)/ZF$(ML_SUFFIX) UNITY/ROOT.ML \
paulson@15634
   111
  UNITY/Comp.thy UNITY/Constrains.thy UNITY/FP.thy\
paulson@15634
   112
  UNITY/GenPrefix.thy UNITY/Guar.thy UNITY/Mutex.thy UNITY/State.thy \
paulson@15634
   113
  UNITY/SubstAx.thy UNITY/UNITY.thy UNITY/Union.thy \
paulson@14076
   114
  UNITY/AllocBase.thy UNITY/AllocImpl.thy\
paulson@14072
   115
  UNITY/ClientImpl.thy UNITY/Distributor.thy\
paulson@14093
   116
  UNITY/Follows.thy UNITY/Increasing.thy UNITY/Merge.thy\
paulson@15634
   117
  UNITY/Monotonicity.thy UNITY/MultisetSum.thy UNITY/WFair.thy
paulson@11479
   118
	@$(ISATOOL) usedir $(OUT)/ZF UNITY
paulson@11479
   119
paulson@11479
   120
paulson@12088
   121
## ZF-Induct
paulson@12088
   122
paulson@12088
   123
ZF-Induct: ZF $(LOG)/ZF-Induct.gz
paulson@12088
   124
wenzelm@17821
   125
$(LOG)/ZF-Induct.gz: $(OUT)/ZF$(ML_SUFFIX)  Induct/ROOT.ML Induct/Acc.thy \
paulson@12560
   126
  Induct/Binary_Trees.thy Induct/Brouwer.thy Induct/Comb.thy \
paulson@14071
   127
  Induct/Datatypes.thy Induct/FoldSet.thy \
paulson@15201
   128
  Induct/ListN.thy Induct/Multiset.thy Induct/Mutil.thy \
paulson@12560
   129
  Induct/Ntree.thy Induct/Primrec.thy Induct/PropLog.thy Induct/Rmap.thy \
wenzelm@12207
   130
  Induct/Term.thy Induct/Tree_Forest.thy Induct/document/root.tex
paulson@12088
   131
	@$(ISATOOL) usedir $(OUT)/ZF Induct
paulson@12088
   132
wenzelm@12175
   133
paulson@12088
   134
## ZF-ex
paulson@12088
   135
paulson@12088
   136
ZF-ex: ZF $(LOG)/ZF-ex.gz
paulson@12088
   137
wenzelm@17821
   138
$(LOG)/ZF-ex.gz: $(OUT)/ZF$(ML_SUFFIX) ex/ROOT.ML \
paulson@14883
   139
  ex/BinEx.thy ex/CoUnit.thy ex/Commutation.thy ex/Group.thy\
paulson@13085
   140
  ex/Limit.thy ex/LList.thy ex/Primes.thy \
paulson@14883
   141
  ex/NatSum.thy ex/Ramsey.thy ex/Ring.thy ex/misc.thy
paulson@12088
   142
	@$(ISATOOL) usedir $(OUT)/ZF ex
paulson@12088
   143
paulson@12088
   144
wenzelm@4518
   145
## clean
wenzelm@4447
   146
wenzelm@4447
   147
clean:
wenzelm@17821
   148
	@rm -f $(OUT)/ZF$(ML_SUFFIX) $(LOG)/ZF.gz $(LOG)/ZF-AC.gz $(LOG)/ZF-Coind.gz \
paulson@13225
   149
	  $(LOG)/ZF-Constructible.gz $(LOG)/ZF-ex.gz \
paulson@13225
   150
          $(LOG)/ZF-IMP.gz $(LOG)/ZF-Resid.gz \
paulson@11479
   151
	  $(LOG)/ZF-UNITY.gz