src/ZF/IsaMakefile
author wenzelm
Sat Oct 04 16:05:09 2008 +0200 (2008-10-04 ago)
changeset 28500 4b79e5d3d0aa
parent 28297 107ba67497a1
child 33450 4389ec600ba7
permissions -rw-r--r--
replaced ISATOOL by ISABELLE_TOOL;
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@27203
    26
ZF: FOL $(OUT)/ZF
wenzelm@4518
    27
wenzelm@4518
    28
FOL:
wenzelm@28500
    29
	@cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL
wenzelm@2500
    30
wenzelm@27203
    31
$(OUT)/ZF: $(OUT)/FOL AC.thy Arith.thy ArithSimp.thy Bin.thy Bool.thy	\
wenzelm@27203
    32
  Cardinal.thy CardinalArith.thy Cardinal_AC.thy Datatype_ZF.thy	\
wenzelm@27203
    33
  Epsilon.thy EquivClass.thy Finite.thy Fixedpt.thy Inductive_ZF.thy	\
wenzelm@27203
    34
  InfDatatype.thy Int_ZF.thy IntArith.thy IntDiv_ZF.thy List_ZF.thy	\
wenzelm@27203
    35
  Main.thy Main_ZF.thy Main_ZFC.thy Nat_ZF.thy OrdQuant.thy Order.thy	\
wenzelm@27203
    36
  OrderArith.thy OrderType.thy Ordinal.thy Perm.thy QPair.thy		\
wenzelm@27203
    37
  QUniv.thy ROOT.ML Sum.thy Tools/cartprod.ML				\
wenzelm@27203
    38
  Tools/datatype_package.ML Tools/ind_cases.ML Tools/induct_tacs.ML	\
wenzelm@27203
    39
  Tools/inductive_package.ML Tools/numeral_syntax.ML			\
wenzelm@27203
    40
  Tools/primrec_package.ML Tools/typechk.ML Trancl.thy Univ.thy WF.thy	\
wenzelm@27203
    41
  ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy ind_syntax.ML	\
wenzelm@27203
    42
  int_arith.ML pair.thy simpdata.ML upair.thy
wenzelm@28500
    43
	@$(ISABELLE_TOOL) usedir -b -g true -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@27203
    50
$(LOG)/ZF-AC.gz: $(OUT)/ZF AC/ROOT.ML AC/AC15_WO6.thy AC/AC16_WO4.thy	\
wenzelm@27203
    51
  AC/AC16_lemmas.thy AC/AC17_AC1.thy AC/AC18_AC19.thy AC/AC7_AC9.thy	\
wenzelm@27203
    52
  AC/AC_Equiv.thy AC/Cardinal_aux.thy AC/DC.thy AC/HH.thy		\
wenzelm@27203
    53
  AC/Hartog.thy AC/WO1_AC.thy AC/WO1_WO7.thy AC/WO2_AC16.thy		\
wenzelm@27203
    54
  AC/WO6_WO1.thy AC/document/root.bib AC/document/root.tex
wenzelm@28500
    55
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/ZF AC
wenzelm@2500
    56
wenzelm@2500
    57
paulson@11479
    58
## ZF-Coind
wenzelm@4518
    59
paulson@11479
    60
ZF-Coind: ZF $(LOG)/ZF-Coind.gz
wenzelm@2500
    61
wenzelm@27203
    62
$(LOG)/ZF-Coind.gz: $(OUT)/ZF Coind/Dynamic.thy Coind/ECR.thy		\
wenzelm@27203
    63
  Coind/Language.thy Coind/Map.thy Coind/ROOT.ML Coind/Static.thy	\
wenzelm@27203
    64
  Coind/Types.thy Coind/Values.thy
wenzelm@28500
    65
	@$(ISABELLE_TOOL) usedir $(OUT)/ZF Coind
wenzelm@2500
    66
wenzelm@2500
    67
paulson@13225
    68
## ZF-Constructible
paulson@13225
    69
paulson@13225
    70
ZF-Constructible: ZF $(LOG)/ZF-Constructible.gz
paulson@13225
    71
wenzelm@27203
    72
$(LOG)/ZF-Constructible.gz: $(OUT)/ZF Constructible/ROOT.ML		\
wenzelm@27203
    73
  Constructible/Datatype_absolute.thy Constructible/DPow_absolute.thy	\
wenzelm@27203
    74
  Constructible/Formula.thy Constructible/Internalize.thy		\
wenzelm@27203
    75
  Constructible/AC_in_L.thy Constructible/Relative.thy			\
wenzelm@27203
    76
  Constructible/L_axioms.thy Constructible/Wellorderings.thy		\
wenzelm@27203
    77
  Constructible/MetaExists.thy Constructible/Normal.thy			\
wenzelm@27203
    78
  Constructible/Rank.thy Constructible/Rank_Separation.thy		\
wenzelm@27203
    79
  Constructible/Rec_Separation.thy Constructible/Separation.thy		\
wenzelm@27203
    80
  Constructible/Satisfies_absolute.thy Constructible/WF_absolute.thy	\
wenzelm@27203
    81
  Constructible/Reflection.thy Constructible/WFrec.thy			\
paulson@15083
    82
  Constructible/document/root.bib Constructible/document/root.tex
wenzelm@28500
    83
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/ZF Constructible
paulson@13225
    84
paulson@13225
    85
paulson@11479
    86
## ZF-IMP
paulson@11479
    87
paulson@11479
    88
ZF-IMP: ZF $(LOG)/ZF-IMP.gz
paulson@11479
    89
wenzelm@27203
    90
$(LOG)/ZF-IMP.gz: $(OUT)/ZF IMP/Com.thy IMP/Denotation.thy	\
wenzelm@27203
    91
  IMP/Equiv.thy IMP/ROOT.ML IMP/document/root.bib		\
wenzelm@27203
    92
  IMP/document/root.tex
wenzelm@28500
    93
	@$(ISABELLE_TOOL) 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@27203
   100
$(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/ROOT.ML Resid/Confluence.thy	\
wenzelm@27203
   101
  Resid/Redex.thy Resid/Reduction.thy Resid/Residuals.thy		\
wenzelm@27203
   102
  Resid/Substitution.thy
wenzelm@28500
   103
	@$(ISABELLE_TOOL) 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@27203
   110
$(LOG)/ZF-UNITY.gz: $(OUT)/ZF UNITY/ROOT.ML UNITY/Comp.thy		\
wenzelm@27203
   111
  UNITY/Constrains.thy UNITY/FP.thy UNITY/GenPrefix.thy UNITY/Guar.thy	\
wenzelm@27203
   112
  UNITY/Mutex.thy UNITY/State.thy UNITY/SubstAx.thy UNITY/UNITY.thy	\
wenzelm@27203
   113
  UNITY/Union.thy UNITY/AllocBase.thy UNITY/AllocImpl.thy		\
wenzelm@27203
   114
  UNITY/ClientImpl.thy UNITY/Distributor.thy UNITY/Follows.thy		\
wenzelm@27203
   115
  UNITY/Increasing.thy UNITY/Merge.thy UNITY/Monotonicity.thy		\
wenzelm@27203
   116
  UNITY/MultisetSum.thy UNITY/WFair.thy
wenzelm@28500
   117
	@$(ISABELLE_TOOL) usedir $(OUT)/ZF UNITY
paulson@11479
   118
paulson@11479
   119
paulson@12088
   120
## ZF-Induct
paulson@12088
   121
paulson@12088
   122
ZF-Induct: ZF $(LOG)/ZF-Induct.gz
paulson@12088
   123
wenzelm@27203
   124
$(LOG)/ZF-Induct.gz: $(OUT)/ZF Induct/ROOT.ML Induct/Acc.thy		\
wenzelm@27203
   125
  Induct/Binary_Trees.thy Induct/Brouwer.thy Induct/Comb.thy		\
wenzelm@27203
   126
  Induct/Datatypes.thy Induct/FoldSet.thy Induct/ListN.thy		\
wenzelm@27203
   127
  Induct/Multiset.thy Induct/Mutil.thy Induct/Ntree.thy			\
wenzelm@27203
   128
  Induct/Primrec.thy Induct/PropLog.thy Induct/Rmap.thy			\
wenzelm@12207
   129
  Induct/Term.thy Induct/Tree_Forest.thy Induct/document/root.tex
wenzelm@28500
   130
	@$(ISABELLE_TOOL) usedir $(OUT)/ZF Induct
paulson@12088
   131
wenzelm@12175
   132
paulson@12088
   133
## ZF-ex
paulson@12088
   134
paulson@12088
   135
ZF-ex: ZF $(LOG)/ZF-ex.gz
paulson@12088
   136
wenzelm@27203
   137
$(LOG)/ZF-ex.gz: $(OUT)/ZF ex/ROOT.ML ex/BinEx.thy ex/CoUnit.thy	\
wenzelm@27203
   138
  ex/Commutation.thy ex/Group.thy ex/Limit.thy ex/LList.thy		\
wenzelm@27203
   139
  ex/Primes.thy ex/NatSum.thy ex/Ramsey.thy ex/Ring.thy ex/misc.thy
wenzelm@28500
   140
	@$(ISABELLE_TOOL) usedir $(OUT)/ZF ex
paulson@12088
   141
paulson@12088
   142
wenzelm@4518
   143
## clean
wenzelm@4447
   144
wenzelm@4447
   145
clean:
wenzelm@27203
   146
	@rm -f $(OUT)/ZF $(LOG)/ZF.gz $(LOG)/ZF-AC.gz $(LOG)/ZF-Coind.gz \
paulson@13225
   147
	  $(LOG)/ZF-Constructible.gz $(LOG)/ZF-ex.gz \
paulson@13225
   148
          $(LOG)/ZF-IMP.gz $(LOG)/ZF-Resid.gz \
paulson@11479
   149
	  $(LOG)/ZF-UNITY.gz