src/HOL/IsaMakefile
author kleing
Mon Aug 20 04:34:31 2007 +0200 (2007-08-20)
changeset 24333 e77ea0ea7f2c
parent 24332 e3a2b75b1cf9
child 24339 d929e9b2e598
permissions -rw-r--r--
* HOL-Word:
New extensive library and type for generic, fixed size machine
words, with arithemtic, bit-wise, shifting and rotating operations,
reflection into int, nat, and bool lists, automation for linear
arithmetic (by automatic reflection into nat or int), including
lemmas on overflow and monotonicity. Instantiated to all appropriate
arithmetic type classes, supporting automatic simplification of
numerals on all operations. Jointly developed by NICTA, Galois, and
PSU.

* still to do: README.html/document + moving some of the generic lemmas
to appropriate place in distribution
wenzelm@2448
     1
#
wenzelm@2448
     2
# IsaMakefile for HOL
wenzelm@2448
     3
#
wenzelm@2448
     4
wenzelm@4518
     5
## targets
wenzelm@2448
     6
wenzelm@4518
     7
default: HOL
wenzelm@17460
     8
generate: HOL-Complex-Generate-HOL HOL-Complex-Generate-HOLLight
kleing@24333
     9
images: HOL HOL-Algebra HOL-Complex HOL-Complex-Matrix HOL-Nominal \
kleing@24333
    10
        HOL-Word TLA HOL4
wenzelm@10135
    11
wenzelm@10255
    12
#Note: keep targets sorted (except for HOL-Library)
wenzelm@10157
    13
test: \
wenzelm@24325
    14
  HOL-ex \
wenzelm@10255
    15
  HOL-Library \
wenzelm@10157
    16
  HOL-Auth \
wenzelm@10157
    17
  HOL-AxClasses \
schirmer@14031
    18
  HOL-Bali \
wenzelm@17610
    19
  HOL-Complex-HahnBanach \
paulson@15771
    20
  HOL-Complex-Import \
wenzelm@17610
    21
  HOL-Complex-ex \
berghofe@13403
    22
  HOL-Extraction \
wenzelm@10157
    23
  HOL-Hoare \
prensani@13019
    24
  HOL-HoareParallel \
wenzelm@10157
    25
  HOL-IMP \
wenzelm@10157
    26
  HOL-IMPP \
wenzelm@10157
    27
  HOL-IOA \
wenzelm@10157
    28
  HOL-Induct \
wenzelm@10157
    29
  HOL-Isar_examples \
wenzelm@10157
    30
  HOL-Lambda \
wenzelm@10157
    31
  HOL-Lattice \
paulson@23449
    32
  HOL-MetisExamples \
wenzelm@10157
    33
  HOL-MicroJava \
wenzelm@10157
    34
  HOL-Modelcheck \
oheimb@11376
    35
  HOL-NanoJava \
berghofe@19497
    36
  HOL-Nominal-Examples \
wenzelm@10157
    37
  HOL-NumberTheory \
wenzelm@10157
    38
  HOL-Prolog \
paulson@14199
    39
  HOL-SET-Protocol \
wenzelm@10157
    40
  HOL-Subst \
wenzelm@10157
    41
      TLA-Buffer \
wenzelm@10157
    42
      TLA-Inc \
wenzelm@10157
    43
      TLA-Memory \
wenzelm@10157
    44
  HOL-UNITY \
wenzelm@10966
    45
  HOL-Unix \
wenzelm@10157
    46
  HOL-W0 \
wenzelm@24325
    47
  HOL-ZF
wenzelm@10157
    48
    # ^ this is the sort position
wenzelm@10614
    49
wenzelm@10157
    50
all: test images
wenzelm@4518
    51
wenzelm@4518
    52
wenzelm@4518
    53
## global settings
wenzelm@4518
    54
wenzelm@4518
    55
SRC = $(ISABELLE_HOME)/src
wenzelm@3118
    56
OUT = $(ISABELLE_OUTPUT)
wenzelm@4447
    57
LOG = $(OUT)/log
wenzelm@2448
    58
wenzelm@4518
    59
wenzelm@4518
    60
## HOL
wenzelm@2448
    61
wenzelm@4518
    62
HOL: Pure $(OUT)/HOL
wenzelm@4518
    63
wenzelm@4518
    64
Pure:
wenzelm@4518
    65
	@cd $(SRC)/Pure; $(ISATOOL) make Pure
paulson@3232
    66
webertj@23194
    67
$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML		\
webertj@23194
    68
  $(SRC)/Provers/Arith/assoc_fold.ML					\
webertj@23194
    69
  $(SRC)/Provers/Arith/cancel_div_mod.ML				\
webertj@23194
    70
  $(SRC)/Provers/Arith/cancel_numeral_factor.ML				\
webertj@23194
    71
  $(SRC)/Provers/Arith/cancel_numerals.ML				\
webertj@23194
    72
  $(SRC)/Provers/Arith/cancel_sums.ML					\
webertj@23194
    73
  $(SRC)/Provers/Arith/combine_numerals.ML				\
webertj@23194
    74
  $(SRC)/Provers/Arith/extract_common_term.ML				\
webertj@23194
    75
  $(SRC)/Provers/Arith/fast_lin_arith.ML				\
webertj@23194
    76
  $(SRC)/Tools/IsaPlanner/isand.ML					\
webertj@23194
    77
  $(SRC)/Tools/IsaPlanner/rw_inst.ML					\
webertj@23194
    78
  $(SRC)/Tools/IsaPlanner/rw_tools.ML					\
webertj@23194
    79
  $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Provers/blast.ML		\
webertj@23194
    80
  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML			\
webertj@23194
    81
  $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML			\
webertj@23194
    82
  $(SRC)/Provers/induct_method.ML $(SRC)/Provers/order.ML		\
webertj@23194
    83
  $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML		\
webertj@23194
    84
  $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML			\
wenzelm@24139
    85
  $(SRC)/Provers/trancl.ML $(SRC)/Tools/integer.ML $(SRC)/Tools/Metis/metis.ML\
haftmann@24280
    86
  $(SRC)/Pure/codegen.ML			\
haftmann@24280
    87
  $(SRC)/Tools/code/code_funcgr.ML			\
haftmann@24280
    88
  $(SRC)/Tools/code/code_name.ML $(SRC)/Tools/code/code_package.ML		\
haftmann@24280
    89
  $(SRC)/Tools/code/code_target.ML $(SRC)/Tools/code/code_thingol.ML	\
haftmann@24162
    90
  $(SRC)/Tools/nbe.ML $(SRC)/Tools/rat.ML Tools/TFL/casesplit.ML ATP_Linkup.thy	\
haftmann@24280
    91
  Accessible_Part.thy Arith_Tools.thy Code_Setup.thy Datatype.thy 			\
wenzelm@23462
    92
  Dense_Linear_Order.thy Divides.thy Equiv_Relations.thy Extraction.thy	\
wenzelm@23462
    93
  Finite_Set.thy FixedPoint.thy Fun.thy FunDef.thy HOL.thy		\
wenzelm@23462
    94
  Hilbert_Choice.thy Inductive.thy IntArith.thy IntDef.thy IntDiv.thy	\
haftmann@23882
    95
  Lattices.thy List.thy Main.thy Map.thy Nat.thy NatBin.thy	\
haftmann@24194
    96
  Numeral.thy OrderedGroup.thy Orderings.thy Power.thy PreList.thy	\
wenzelm@23462
    97
  Predicate.thy Product_Type.thy ROOT.ML Recdef.thy			\
wenzelm@23252
    98
  Record.thy Refute.thy Relation.thy Relation_Power.thy			\
wenzelm@23252
    99
  Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy Sum_Type.thy	\
paulson@24288
   100
  Groebner_Basis.thy Tools/watcher.ML	\
wenzelm@23252
   101
  Tools/Groebner_Basis/groebner.ML Tools/Groebner_Basis/misc.ML		\
wenzelm@23466
   102
  Tools/Groebner_Basis/normalizer.ML					\
wenzelm@23466
   103
  Tools/Groebner_Basis/normalizer_data.ML Tools/Qelim/cooper.ML		\
chaieb@24082
   104
  Tools/Qelim/langford_data.ML Tools/Qelim/langford.ML		\
wenzelm@23466
   105
  Tools/Qelim/cooper_data.ML Tools/Qelim/ferrante_rackoff.ML		\
wenzelm@23466
   106
  Tools/Qelim/ferrante_rackoff_data.ML Tools/Qelim/generated_cooper.ML	\
wenzelm@23466
   107
  Tools/Qelim/presburger.ML Tools/Qelim/qelim.ML			\
wenzelm@23454
   108
  Tools/TFL/dcterm.ML Tools/TFL/post.ML Tools/TFL/rules.ML		\
wenzelm@23454
   109
  Tools/TFL/tfl.ML Tools/TFL/thms.ML Tools/TFL/thry.ML			\
wenzelm@23454
   110
  Tools/TFL/usyntax.ML Tools/TFL/utils.ML Tools/cnf_funcs.ML		\
wenzelm@23454
   111
  Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML			\
wenzelm@23454
   112
  Tools/datatype_case.ML Tools/datatype_codegen.ML			\
wenzelm@23454
   113
  Tools/datatype_hooks.ML Tools/datatype_package.ML			\
wenzelm@23454
   114
  Tools/datatype_prop.ML Tools/datatype_realizer.ML			\
wenzelm@23454
   115
  Tools/datatype_rep_proofs.ML Tools/function_package/auto_term.ML	\
webertj@23194
   116
  Tools/function_package/context_tree.ML				\
webertj@23194
   117
  Tools/function_package/fundef_common.ML				\
webertj@23194
   118
  Tools/function_package/fundef_core.ML					\
webertj@23194
   119
  Tools/function_package/fundef_datatype.ML				\
webertj@23194
   120
  Tools/function_package/fundef_lib.ML					\
webertj@23194
   121
  Tools/function_package/fundef_package.ML				\
webertj@23194
   122
  Tools/function_package/inductive_wrap.ML				\
webertj@23194
   123
  Tools/function_package/lexicographic_order.ML				\
webertj@23194
   124
  Tools/function_package/mutual.ML					\
wenzelm@23574
   125
  Tools/function_package/pattern_split.ML Tools/inductive_codegen.ML	\
berghofe@23734
   126
  Tools/inductive_package.ML Tools/inductive_realizer.ML		\
wenzelm@24091
   127
  Tools/inductive_set_package.ML Tools/lin_arith.ML Tools/meson.ML	\
wenzelm@23574
   128
  Tools/metis_tools.ML Tools/numeral.ML Tools/numeral_syntax.ML		\
berghofe@23734
   129
  Tools/polyhash.ML Tools/primrec_package.ML Tools/prop_logic.ML 	\
wenzelm@23454
   130
  Tools/recdef_package.ML Tools/recfun_codegen.ML			\
wenzelm@23454
   131
  Tools/record_package.ML Tools/refute.ML Tools/refute_isar.ML		\
wenzelm@23454
   132
  Tools/res_atp.ML Tools/res_atp_methods.ML Tools/res_atp_provers.ML	\
wenzelm@24036
   133
  Tools/res_axioms.ML Tools/res_clause.ML Tools/res_hol_clause.ML	\
wenzelm@24036
   134
  Tools/res_reconstruct.ML Tools/rewrite_hol_proof.ML 			\
wenzelm@24036
   135
  Tools/sat_funcs.ML Tools/sat_solver.ML Tools/specification_package.ML	\
wenzelm@24036
   136
  Tools/split_rule.ML Tools/string_syntax.ML Tools/typecopy_package.ML	\
webertj@23194
   137
  Tools/typedef_codegen.ML Tools/typedef_package.ML			\
webertj@23194
   138
  Transitive_Closure.thy Typedef.thy Wellfounded_Recursion.thy		\
webertj@23194
   139
  Wellfounded_Relations.thy arith_data.ML document/root.tex hologic.ML	\
wenzelm@23164
   140
  int_arith1.ML int_factor_simprocs.ML nat_simprocs.ML simpdata.ML
wenzelm@16187
   141
	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
wenzelm@4518
   142
wenzelm@13029
   143
kleing@13967
   144
## HOL-Complex-HahnBanach
wenzelm@13029
   145
kleing@13967
   146
HOL-Complex-HahnBanach: HOL-Complex $(LOG)/HOL-Complex-HahnBanach.gz
wenzelm@13029
   147
wenzelm@16019
   148
$(LOG)/HOL-Complex-HahnBanach.gz: $(OUT)/HOL-Complex			\
wenzelm@16019
   149
  Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy		\
wenzelm@16019
   150
  Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy	\
wenzelm@16019
   151
  Real/HahnBanach/HahnBanachExtLemmas.thy				\
wenzelm@16019
   152
  Real/HahnBanach/HahnBanachSupLemmas.thy				\
wenzelm@16019
   153
  Real/HahnBanach/Linearform.thy Real/HahnBanach/NormedSpace.thy	\
wenzelm@16019
   154
  Real/HahnBanach/README.html Real/HahnBanach/ROOT.ML			\
wenzelm@16019
   155
  Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy		\
wenzelm@16019
   156
  Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/root.bib	\
wenzelm@13029
   157
  Real/HahnBanach/document/root.tex
paulson@13966
   158
	@cd Real; $(ISATOOL) usedir -g true $(OUT)/HOL-Complex HahnBanach
wenzelm@13029
   159
wenzelm@13029
   160
paulson@13961
   161
## HOL-Complex
paulson@10751
   162
paulson@13966
   163
HOL-Complex: HOL $(OUT)/HOL-Complex
paulson@10751
   164
haftmann@23247
   165
$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML $(SRC)/Tools/float.ML \
webertj@23194
   166
  Library/Zorn.thy							\
wenzelm@23454
   167
  Real/ContNotDenum.thy Real/float_arith.ML Real/Float.thy		\
wenzelm@24103
   168
  Real/Lubs.thy Real/PReal.thy Real/RComplete.thy 			\
wenzelm@23454
   169
  Real/Rational.thy Real/Real.thy Real/RealDef.thy Real/RealPow.thy	\
wenzelm@23454
   170
  Real/RealVector.thy Real/rat_arith.ML Real/real_arith.ML		\
webertj@23194
   171
  Hyperreal/StarDef.thy Hyperreal/StarClasses.thy			\
webertj@23194
   172
  Hyperreal/EvenOdd.thy Hyperreal/Fact.thy Hyperreal/HLog.thy		\
webertj@23194
   173
  Hyperreal/Filter.thy Hyperreal/HSeries.thy Hyperreal/transfer.ML	\
webertj@23194
   174
  Hyperreal/HLim.thy Hyperreal/HSEQ.thy Hyperreal/HTranscendental.thy	\
webertj@23194
   175
  Hyperreal/HDeriv.thy Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy	\
webertj@23194
   176
  Hyperreal/Hyperreal.thy						\
webertj@23194
   177
  Hyperreal/Integration.thy Hyperreal/Lim.thy Hyperreal/Log.thy		\
webertj@23194
   178
  Hyperreal/Ln.thy Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy	\
webertj@23194
   179
  Hyperreal/NSA.thy Hyperreal/NthRoot.thy Hyperreal/Poly.thy		\
webertj@23194
   180
  Hyperreal/SEQ.thy Hyperreal/Series.thy Hyperreal/Star.thy		\
webertj@23194
   181
  Hyperreal/Taylor.thy Hyperreal/FrechetDeriv.thy Hyperreal/Deriv.thy	\
webertj@23194
   182
  Hyperreal/Transcendental.thy Hyperreal/hypreal_arith.ML		\
webertj@23194
   183
  Complex/Complex_Main.thy Complex/CLim.thy				\
webertj@23194
   184
  Complex/CStar.thy Complex/Complex.thy Complex/NSCA.thy		\
webertj@23194
   185
  Complex/NSComplex.thy							\
wenzelm@22897
   186
  Complex/document/root.tex Library/Infinite_Set.thy Library/Parity.thy
nipkow@15057
   187
	@cd Complex; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Complex
paulson@10751
   188
wenzelm@7395
   189
paulson@13961
   190
## HOL-Complex-ex
paulson@7392
   191
paulson@13961
   192
HOL-Complex-ex: HOL-Complex $(LOG)/HOL-Complex-ex.gz
wenzelm@7535
   193
paulson@13961
   194
$(LOG)/HOL-Complex-ex.gz: $(OUT)/HOL-Complex Library/Primes.thy \
paulson@13961
   195
  Complex/ex/ROOT.ML Complex/ex/document/root.tex \
webertj@23194
   196
  Complex/ex/BigO_Complex.thy Complex/ex/BinEx.thy \
chaieb@23265
   197
  Complex/ex/NSPrimes.thy Complex/ex/Sqrt.thy Complex/ex/Sqrt_Script.thy \
chaieb@23265
   198
  Complex/ex/MIR.thy Complex/ex/mirtac.ML Complex/ex/mireif.ML \
chaieb@23265
   199
  Complex/ex/ReflectedFerrack.thy Complex/ex/linreif.ML Complex/ex/linrtac.ML
paulson@13961
   200
	@cd Complex; $(ISATOOL) usedir $(OUT)/HOL-Complex ex
wenzelm@7535
   201
wenzelm@7535
   202
wenzelm@10255
   203
## HOL-Library
wenzelm@10255
   204
wenzelm@10255
   205
HOL-Library: HOL $(LOG)/HOL-Library.gz
wenzelm@10255
   206
krauss@19564
   207
$(LOG)/HOL-Library.gz: $(OUT)/HOL \
paulson@19944
   208
  Library/SetsAndFunctions.thy Library/BigO.thy Library/Ramsey.thy \
haftmann@23854
   209
  Library/Efficient_Nat.thy Library/Executable_Set.thy \
haftmann@23854
   210
  Library/Executable_Rat.thy Library/Executable_Real.thy \
haftmann@23854
   211
  Library/ML_Int.thy Library/ML_String.thy Library/Infinite_Set.thy \
nipkow@23192
   212
  Library/FuncSet.thy Library/Library.thy \
webertj@23194
   213
  Library/List_Prefix.thy Library/State_Monad.thy Library/Multiset.thy \
webertj@23194
   214
  Library/NatPair.thy \
paulson@14265
   215
  Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \
haftmann@23005
   216
  Library/Nat_Infinity.thy Library/Word.thy \
oheimb@11349
   217
  Library/README.html Library/Continuity.thy \
paulson@14365
   218
  Library/Nested_Environment.thy Library/Zorn.thy\
wenzelm@12816
   219
  Library/Library/ROOT.ML Library/Library/document/root.tex \
nipkow@15731
   220
  Library/Library/document/root.bib Library/While_Combinator.thy \
haftmann@22799
   221
  Library/Product_ord.thy Library/Char_nat.thy Library/Char_ord.thy \
wenzelm@18397
   222
  Library/List_lexord.thy Library/Commutative_Ring.thy Library/comm_ring.ML \
wenzelm@21256
   223
  Library/Coinductive_List.thy Library/AssocList.thy \
krauss@22359
   224
  Library/Parity.thy Library/GCD.thy Library/Binomial.thy \
krauss@22359
   225
  Library/Graphs.thy Library/Kleene_Algebras.thy Library/SCT_Misc.thy \
webertj@23194
   226
  Library/SCT_Definition.thy Library/SCT_Theorem.thy \
webertj@23194
   227
  Library/SCT_Interpretation.thy \
krauss@22359
   228
  Library/SCT_Implementation.thy Library/Size_Change_Termination.thy \
haftmann@22517
   229
  Library/SCT_Examples.thy Library/sct.ML \
kleing@24332
   230
  Library/Pure_term.thy Library/Eval.thy Library/Eval_Witness.thy \
kleing@24332
   231
  Library/Pretty_Int.thy \
kleing@24332
   232
  Library/Pretty_Char.thy Library/Pretty_Char_chr.thy Library/Abstract_Rat.thy\
kleing@24332
   233
  Library/Numeral_Type.thy Library/Boolean_Algebra.thy
wenzelm@11398
   234
	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
wenzelm@10255
   235
wenzelm@10255
   236
wenzelm@4518
   237
## HOL-Subst
wenzelm@4518
   238
wenzelm@4518
   239
HOL-Subst: HOL $(LOG)/HOL-Subst.gz
wenzelm@4518
   240
paulson@15635
   241
$(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.thy \
paulson@15635
   242
  Subst/ROOT.ML Subst/Subst.thy Subst/UTerm.thy Subst/Unifier.thy \
wenzelm@4518
   243
  Subst/Unify.thy
wenzelm@4518
   244
	@$(ISATOOL) usedir $(OUT)/HOL Subst
wenzelm@2448
   245
wenzelm@2448
   246
wenzelm@4518
   247
## HOL-Induct
wenzelm@2473
   248
wenzelm@4518
   249
HOL-Induct: HOL $(LOG)/HOL-Induct.gz
paulson@3125
   250
wenzelm@10255
   251
$(LOG)/HOL-Induct.gz: $(OUT)/HOL \
paulson@13075
   252
  Induct/Com.thy Induct/Comb.thy Induct/LFilter.thy \
paulson@13075
   253
  Induct/LList.thy Induct/Mutil.thy Induct/Ordinals.thy \
paulson@15172
   254
  Induct/PropLog.thy Induct/QuoNestedDataType.thy Induct/QuoDataType.thy\
paulson@15172
   255
  Induct/ROOT.ML \
paulson@13079
   256
  Induct/Sexp.thy Induct/Sigma_Algebra.thy \
paulson@13079
   257
  Induct/SList.thy Induct/ABexp.thy Induct/Term.thy \
wenzelm@11046
   258
  Induct/Tree.thy Induct/document/root.tex
paulson@3125
   259
	@$(ISATOOL) usedir $(OUT)/HOL Induct
paulson@3125
   260
paulson@3125
   261
wenzelm@4518
   262
## HOL-IMP
wenzelm@4518
   263
wenzelm@4518
   264
HOL-IMP: HOL $(LOG)/HOL-IMP.gz
wenzelm@2448
   265
nipkow@13129
   266
$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Compiler0.thy IMP/Compiler.thy \
kleing@12432
   267
  IMP/Denotation.thy IMP/Expr.thy IMP/Hoare.thy \
kleing@12432
   268
  IMP/Natural.thy IMP/Examples.thy \
kleing@12432
   269
  IMP/Transition.thy IMP/VC.thy IMP/ROOT.ML IMP/document/root.tex \
kleing@12432
   270
  IMP/document/root.bib
wenzelm@12548
   271
	@$(ISATOOL) usedir -g true $(OUT)/HOL IMP
wenzelm@2448
   272
wenzelm@2448
   273
oheimb@8179
   274
## HOL-IMPP
oheimb@8179
   275
oheimb@8179
   276
HOL-IMPP: HOL $(LOG)/HOL-IMPP.gz
oheimb@8179
   277
wenzelm@19803
   278
$(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy \
wenzelm@19803
   279
  IMPP/Natural.thy IMPP/Hoare.thy IMPP/Misc.thy IMPP/EvenOdd.thy
oheimb@8179
   280
	@$(ISATOOL) usedir $(OUT)/HOL IMPP
oheimb@8179
   281
oheimb@8179
   282
skalberg@14516
   283
## HOL-Complex-Import
skalberg@14516
   284
wenzelm@19097
   285
IMPORTER_FILES = Import/lazy_seq.ML Import/proof_kernel.ML Import/replay.ML \
wenzelm@20610
   286
  Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \
skalberg@14516
   287
  Import/HOL4Syntax.thy Import/HOL4Compat.thy Import/import_syntax.ML \
skalberg@14516
   288
  Import/hol4rews.ML Import/import_package.ML Import/ROOT.ML
skalberg@14516
   289
obua@17323
   290
IMPORTER_HOLLIGHT_FILES = Import/proof_kernel.ML Import/replay.ML \
obua@17323
   291
  Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \
obua@17323
   292
  Import/HOL4Syntax.thy Import/HOLLightCompat.thy Import/import_syntax.ML \
obua@17323
   293
  Import/hol4rews.ML Import/import_package.ML Import/ROOT.ML
obua@17323
   294
skalberg@14516
   295
HOL-Complex-Import: HOL-Complex $(LOG)/HOL-Complex-Import.gz
skalberg@14516
   296
skalberg@14516
   297
$(LOG)/HOL-Complex-Import.gz: $(OUT)/HOL-Complex $(IMPORTER_FILES)
skalberg@14516
   298
	@$(ISATOOL) usedir $(OUT)/HOL-Complex Import
skalberg@14516
   299
skalberg@14516
   300
skalberg@14516
   301
## HOL-Complex-Generate-HOL
skalberg@14516
   302
skalberg@14516
   303
HOL-Complex-Generate-HOL: HOL-Complex $(LOG)/HOL-Complex-Generate-HOL.gz
skalberg@14516
   304
skalberg@14516
   305
$(LOG)/HOL-Complex-Generate-HOL.gz: $(OUT)/HOL-Complex $(IMPORTER_FILES)  \
skalberg@14516
   306
  Import/Generate-HOL/GenHOL4Base.thy Import/Generate-HOL/GenHOL4Prob.thy \
skalberg@14516
   307
  Import/Generate-HOL/GenHOL4Real.thy Import/Generate-HOL/GenHOL4Vec.thy  \
skalberg@14516
   308
  Import/Generate-HOL/GenHOL4Word32.thy Import/Generate-HOL/ROOT.ML
skalberg@14516
   309
	@cd Import; $(ISATOOL) usedir $(OUT)/HOL-Complex Generate-HOL
skalberg@14516
   310
wenzelm@17460
   311
wenzelm@17460
   312
## HOL-Complex-Generate-HOLLight
wenzelm@17460
   313
obua@17323
   314
HOL-Complex-Generate-HOLLight: HOL-Complex $(LOG)/HOL-Complex-Generate-HOLLight.gz
obua@17323
   315
obua@17323
   316
$(LOG)/HOL-Complex-Generate-HOLLight.gz: $(OUT)/HOL-Complex $(IMPORTER_HOLLIGHT_FILES)  \
obua@17323
   317
  Import/Generate-HOLLight/GenHOLLight.thy Import/Generate-HOLLight/ROOT.ML
obua@17323
   318
	@cd Import; $(ISATOOL) usedir $(OUT)/HOL-Complex Generate-HOLLight
skalberg@14516
   319
wenzelm@17460
   320
skalberg@14516
   321
## HOL-Import-HOL
skalberg@14516
   322
kleing@14626
   323
HOL4: HOL-Complex $(LOG)/HOL4.gz
skalberg@14516
   324
skalberg@14516
   325
HOL_IMPORT_FILES = arithmetic.imp bits.imp boolean_sequence.imp bool.imp \
skalberg@14516
   326
  bword_arith.imp bword_bitop.imp bword_num.imp combin.imp divides.imp \
skalberg@14516
   327
  hrat.imp hreal.imp ind_type.imp lim.imp list.imp marker.imp nets.imp \
skalberg@14516
   328
  numeral.imp num.imp one.imp operator.imp option.imp pair.imp poly.imp \
skalberg@14516
   329
  powser.imp pred_set.imp prime.imp prim_rec.imp prob_algebra.imp \
skalberg@14516
   330
  prob_canon.imp prob_extra.imp prob.imp prob_indep.imp prob_pseudo.imp \
webertj@23194
   331
  prob_uniform.imp realax.imp real.imp relation.imp res_quan.imp \
webertj@23194
   332
  rich_list.imp \
skalberg@14516
   333
  seq.imp state_transformer.imp sum.imp topology.imp transc.imp word32.imp \
skalberg@14516
   334
  word_base.imp word_bitop.imp word_num.imp
skalberg@14516
   335
kleing@14626
   336
$(LOG)/HOL4.gz: $(OUT)/HOL-Complex $(IMPORTER_FILES) \
skalberg@14516
   337
  $(HOL_IMPORT_FILES:%=Import/HOL/%) Import/HOL/HOL4Base.thy \
skalberg@14516
   338
  Import/HOL/HOL4Prob.thy Import/HOL/HOL4Real.thy Import/HOL/HOL4Vec.thy \
skalberg@14516
   339
  Import/HOL/HOL4Word32.thy Import/HOL/HOL4.thy Import/HOL/ROOT.ML
kleing@14626
   340
	@cd Import/HOL; $(ISATOOL) usedir -b $(OUT)/HOL-Complex HOL4
skalberg@14516
   341
obua@17645
   342
HOLLight: HOL-Complex $(LOG)/HOLLight.gz
obua@17645
   343
obua@17645
   344
$(LOG)/HOLLight.gz: $(OUT)/HOL-Complex $(IMPORTER_HOLLIGHT_FILES) \
obua@17645
   345
  Import/HOLLight/hollight.imp Import/HOLLight/HOLLight.thy \
obua@17645
   346
  Import/HOLLight/ROOT.ML
obua@17645
   347
	@cd Import/HOLLight; $(ISATOOL) usedir -b $(OUT)/HOL-Complex HOLLight
obua@17645
   348
skalberg@14516
   349
paulson@9510
   350
## HOL-NumberTheory
paulson@9510
   351
paulson@9510
   352
HOL-NumberTheory: HOL $(LOG)/HOL-NumberTheory.gz
paulson@9510
   353
paulson@9510
   354
$(LOG)/HOL-NumberTheory.gz: $(OUT)/HOL \
paulson@11363
   355
  Library/Permutation.thy Library/Primes.thy NumberTheory/Fib.thy \
wenzelm@11049
   356
  NumberTheory/Factorization.thy NumberTheory/BijectionRel.thy \
wenzelm@11049
   357
  NumberTheory/Chinese.thy NumberTheory/EulerFermat.thy \
wenzelm@11049
   358
  NumberTheory/IntFact.thy NumberTheory/IntPrimes.thy \
wenzelm@11049
   359
  NumberTheory/WilsonBij.thy NumberTheory/WilsonRuss.thy \
paulson@13873
   360
  NumberTheory/Finite2.thy NumberTheory/Int2.thy NumberTheory/EvenOdd.thy\
paulson@13873
   361
  NumberTheory/Residues.thy NumberTheory/Euler.thy NumberTheory/Gauss.thy\
wenzelm@20808
   362
  NumberTheory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy\
paulson@9510
   363
  NumberTheory/ROOT.ML
wenzelm@11850
   364
	@$(ISATOOL) usedir -g true $(OUT)/HOL NumberTheory
paulson@9510
   365
paulson@9510
   366
wenzelm@4518
   367
## HOL-Hoare
wenzelm@4518
   368
wenzelm@4518
   369
HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz
wenzelm@2448
   370
wenzelm@19802
   371
$(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.thy \
nipkow@13697
   372
  Hoare/Examples.thy Hoare/hoare.ML Hoare/Hoare.thy \
nipkow@13875
   373
  Hoare/Heap.thy Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy \
nipkow@13875
   374
  Hoare/ROOT.ML Hoare/ExamplesAbort.thy  Hoare/HeapSyntaxAbort.thy \
nipkow@14075
   375
  Hoare/hoareAbort.ML Hoare/HoareAbort.thy Hoare/SchorrWaite.thy \
nipkow@19402
   376
  Hoare/Separation.thy Hoare/SepLogHeap.thy \
nipkow@19402
   377
  Hoare/document/root.tex Hoare/document/root.bib
wenzelm@2826
   378
	@$(ISATOOL) usedir $(OUT)/HOL Hoare
wenzelm@2448
   379
wenzelm@2448
   380
prensani@12996
   381
## HOL-HoareParallel
prensani@12996
   382
prensani@12996
   383
HOL-HoareParallel: HOL $(LOG)/HOL-HoareParallel.gz
prensani@12996
   384
prensani@12996
   385
$(LOG)/HOL-HoareParallel.gz: $(OUT)/HOL HoareParallel/Gar_Coll.thy \
prensani@12996
   386
  HoareParallel/Graph.thy HoareParallel/Mul_Gar_Coll.thy	   \
prensani@12996
   387
  HoareParallel/OG_Com.thy HoareParallel/OG_Examples.thy	   \
prensani@12996
   388
  HoareParallel/OG_Hoare.thy HoareParallel/OG_Syntax.thy	   \
prensani@12996
   389
  HoareParallel/OG_Tactics.thy HoareParallel/OG_Tran.thy	   \
prensani@13019
   390
  HoareParallel/Quote_Antiquote.thy                                \
prensani@12996
   391
  HoareParallel/RG_Com.thy HoareParallel/RG_Examples.thy	   \
prensani@12996
   392
  HoareParallel/RG_Hoare.thy HoareParallel/RG_Syntax.thy	   \
prensani@12996
   393
  HoareParallel/RG_Tran.thy HoareParallel/ROOT.ML		   \
nipkow@19402
   394
  HoareParallel/document/root.tex HoareParallel/document/root.bib
wenzelm@13029
   395
	@$(ISATOOL) usedir -g true $(OUT)/HOL HoareParallel
prensani@12996
   396
prensani@12996
   397
paulson@23449
   398
## HOL-MetisExamples
paulson@23449
   399
paulson@23449
   400
HOL-MetisExamples: HOL $(LOG)/HOL-MetisExamples.gz
paulson@23449
   401
paulson@23449
   402
$(LOG)/HOL-MetisExamples.gz: $(OUT)/HOL \
paulson@23449
   403
  MetisExamples/ROOT.ML \
paulson@23449
   404
  MetisExamples/Abstraction.thy MetisExamples/BigO.thy MetisExamples/BT.thy \
paulson@23449
   405
  MetisExamples/Message.thy MetisExamples/Tarski.thy MetisExamples/TransClosure.thy \
paulson@23449
   406
  MetisExamples/set.thy
wenzelm@23454
   407
	@$(ISATOOL) usedir $(OUT)/HOL MetisExamples
paulson@23449
   408
paulson@23449
   409
paulson@7999
   410
## HOL-Algebra
paulson@7999
   411
paulson@7999
   412
HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz
paulson@7999
   413
wenzelm@21423
   414
$(LOG)/HOL-Algebra.gz: $(OUT)/HOL Algebra/ROOT.ML Library/Primes.thy	\
wenzelm@21423
   415
  Library/FuncSet.thy Algebra/AbelCoset.thy Algebra/Bij.thy		\
wenzelm@21423
   416
  Algebra/Coset.thy Algebra/Exponent.thy Algebra/FiniteProduct.thy	\
wenzelm@21423
   417
  Algebra/Group.thy Algebra/Ideal.thy Algebra/IntRing.thy		\
wenzelm@21423
   418
  Algebra/Lattice.thy Algebra/Module.thy Algebra/QuotRing.thy		\
wenzelm@21423
   419
  Algebra/Ring.thy Algebra/RingHom.thy Algebra/Sylow.thy		\
wenzelm@21423
   420
  Algebra/UnivPoly.thy Algebra/abstract/Abstract.thy			\
wenzelm@21423
   421
  Algebra/abstract/Factor.thy Algebra/abstract/Field.thy		\
wenzelm@21423
   422
  Algebra/abstract/Ideal2.thy Algebra/abstract/PID.thy			\
wenzelm@21423
   423
  Algebra/abstract/Ring2.thy Algebra/abstract/RingHomo.thy		\
wenzelm@21423
   424
  Algebra/document/root.tex Algebra/poly/LongDiv.thy			\
wenzelm@21423
   425
  Algebra/poly/PolyHomo.thy Algebra/poly/Polynomial.thy			\
wenzelm@21423
   426
  Algebra/poly/UnivPoly2.thy Algebra/ringsimp.ML
wenzelm@14578
   427
	@cd Algebra; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Algebra
paulson@7999
   428
wenzelm@4518
   429
## HOL-Auth
wenzelm@3819
   430
wenzelm@4518
   431
HOL-Auth: HOL $(LOG)/HOL-Auth.gz
wenzelm@3819
   432
paulson@14132
   433
$(LOG)/HOL-Auth.gz: $(OUT)/HOL Library/NatPair.thy \
paulson@13926
   434
  Auth/CertifiedEmail.thy Auth/Event.thy \
paulson@13926
   435
  Auth/Message.thy Auth/NS_Public.thy Auth/NS_Public_Bad.thy \
webertj@23194
   436
  Auth/NS_Shared.thy Auth/OtwayRees.thy Auth/OtwayReesBella.thy \
webertj@23194
   437
  Auth/OtwayRees_AN.thy \
paulson@13923
   438
  Auth/OtwayRees_Bad.thy Auth/Public.thy Auth/ROOT.ML \
paulson@13926
   439
  Auth/Recur.thy Auth/Shared.thy \
webertj@23194
   440
  Auth/TLS.thy Auth/WooLam.thy Auth/Kerberos_BAN.thy \
webertj@23194
   441
  Auth/Kerberos_BAN_Gets.thy \
paulson@18886
   442
  Auth/KerberosIV.thy Auth/KerberosIV_Gets.thy Auth/KerberosV.thy \
paulson@13508
   443
  Auth/Yahalom.thy Auth/Yahalom2.thy Auth/Yahalom_Bad.thy \
paulson@14145
   444
  Auth/ZhouGollmann.thy \
paulson@13508
   445
  Auth/Guard/Analz.thy Auth/Guard/Extensions.thy Auth/Guard/GuardK.thy \
paulson@13508
   446
  Auth/Guard/Guard_Public.thy Auth/Guard/Guard_Shared.thy \
paulson@13508
   447
  Auth/Guard/Guard.thy Auth/Guard/List_Msg.thy \
wenzelm@17394
   448
  Auth/Guard/Guard_NS_Public.thy Auth/Guard/Guard_OtwayRees.thy \
paulson@13508
   449
  Auth/Guard/P1.thy Auth/Guard/P2.thy \
webertj@23194
   450
  Auth/Guard/Proto.thy Auth/Guard/Guard_Yahalom.thy \
webertj@23194
   451
  Auth/Smartcard/EventSC.thy Auth/Smartcard/ShoupRubinBella.thy \
webertj@23194
   452
  Auth/Smartcard/ShoupRubin.thy Auth/Smartcard/Smartcard.thy \
wenzelm@23164
   453
  Auth/document/root.tex
kleing@13964
   454
	@$(ISATOOL) usedir -g true $(OUT)/HOL Auth
wenzelm@2448
   455
wenzelm@2448
   456
paulson@4777
   457
## HOL-UNITY
paulson@4777
   458
paulson@4777
   459
HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz
paulson@4777
   460
paulson@10787
   461
$(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \
paulson@13790
   462
  UNITY/UNITY_Main.thy UNITY/UNITY_tactics.ML \
paulson@13797
   463
  UNITY/Comp.thy UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy \
paulson@13853
   464
  UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy UNITY/Guar.thy\
paulson@13853
   465
  UNITY/Lift_prog.thy UNITY/ListOrder.thy UNITY/ProgressSets.thy\
paulson@13853
   466
  UNITY/PPROD.thy  UNITY/Project.thy UNITY/Rename.thy UNITY/Transformers.thy\
paulson@13797
   467
  UNITY/SubstAx.thy UNITY/UNITY.thy UNITY/Union.thy UNITY/WFair.thy \
paulson@13790
   468
  UNITY/Simple/Channel.thy UNITY/Simple/Common.thy  \
paulson@13790
   469
  UNITY/Simple/Deadlock.thy UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy  \
paulson@14199
   470
  UNITY/Simple/NSP_Bad.thy UNITY/Simple/Network.thy\
paulson@13790
   471
  UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy UNITY/Simple/Token.thy\
wenzelm@21632
   472
  UNITY/Comp/Alloc.thy UNITY/Comp/AllocBase.thy UNITY/Comp/AllocImpl.thy \
wenzelm@21632
   473
  UNITY/Comp/Client.thy UNITY/Comp/Counter.thy UNITY/Comp/Counterc.thy \
wenzelm@21632
   474
  UNITY/Comp/Handshake.thy UNITY/Comp/PriorityAux.thy \
paulson@14087
   475
  UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \
paulson@14150
   476
  UNITY/Comp/TimerArray.thy\
paulson@14150
   477
  UNITY/document/root.tex 
paulson@14150
   478
	@$(ISATOOL) usedir -g true $(OUT)/HOL UNITY
paulson@4777
   479
paulson@4777
   480
wenzelm@10966
   481
## HOL-Unix
wenzelm@10966
   482
wenzelm@10966
   483
HOL-Unix: HOL $(LOG)/HOL-Unix.gz
wenzelm@10966
   484
wenzelm@10966
   485
$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy \
wenzelm@10966
   486
  Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy \
wenzelm@10966
   487
  Unix/document/root.bib Unix/document/root.tex
wenzelm@10966
   488
	@$(ISATOOL) usedir $(OUT)/HOL Unix
wenzelm@10966
   489
obua@19203
   490
## HOL-ZF
obua@19203
   491
obua@19203
   492
HOL-ZF: HOL $(LOG)/HOL-ZF.gz
obua@19203
   493
obua@19203
   494
$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML  \
obua@19203
   495
  ZF/Helper.thy ZF/LProd.thy ZF/HOLZF.thy \
obua@19203
   496
  ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex
obua@19203
   497
	@$(ISATOOL) usedir $(OUT)/HOL ZF
wenzelm@10966
   498
wenzelm@4518
   499
## HOL-Modelcheck
wenzelm@4518
   500
wenzelm@4518
   501
HOL-Modelcheck: HOL $(LOG)/HOL-Modelcheck.gz
mueller@3218
   502
wenzelm@4518
   503
$(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL Modelcheck/CTL.thy \
wenzelm@22819
   504
  Modelcheck/EindhovenExample.thy Modelcheck/EindhovenSyn.thy \
wenzelm@22819
   505
  Modelcheck/MuCalculus.thy Modelcheck/MuckeExample1.thy \
wenzelm@22819
   506
  Modelcheck/MuckeExample2.thy Modelcheck/MuckeSyn.thy \
wenzelm@22819
   507
  Modelcheck/ROOT.ML Modelcheck/mucke_oracle.ML
mueller@3218
   508
	@$(ISATOOL) usedir $(OUT)/HOL Modelcheck
mueller@3218
   509
mueller@3218
   510
wenzelm@4518
   511
## HOL-Lambda
wenzelm@2448
   512
wenzelm@4518
   513
HOL-Lambda: HOL $(LOG)/HOL-Lambda.gz
wenzelm@2448
   514
krauss@19564
   515
$(LOG)/HOL-Lambda.gz: $(OUT)/HOL \
webertj@23194
   516
  Lambda/Commutation.thy Lambda/Eta.thy Lambda/InductTermi.thy \
webertj@23194
   517
  Lambda/Lambda.thy \
wenzelm@9771
   518
  Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy \
berghofe@14070
   519
  Lambda/ParRed.thy Lambda/StrongNorm.thy Lambda/Type.thy \
berghofe@14070
   520
  Lambda/WeakNorm.thy Lambda/ROOT.ML \
berghofe@14070
   521
  Lambda/document/root.bib Lambda/document/root.tex
wenzelm@22100
   522
	@$(ISATOOL) usedir -g true -m no_brackets $(OUT)/HOL Lambda
wenzelm@2448
   523
wenzelm@2448
   524
oheimb@9015
   525
## HOL-Prolog
oheimb@9015
   526
oheimb@9015
   527
HOL-Prolog: HOL $(LOG)/HOL-Prolog.gz
oheimb@9015
   528
webertj@23194
   529
$(LOG)/HOL-Prolog.gz: $(OUT)/HOL Prolog/ROOT.ML Prolog/prolog.ML \
webertj@23194
   530
  Prolog/HOHH.thy \
wenzelm@21425
   531
  Prolog/Test.thy Prolog/Func.thy Prolog/Type.thy
oheimb@9015
   532
	@$(ISATOOL) usedir $(OUT)/HOL Prolog
oheimb@9015
   533
oheimb@9015
   534
wenzelm@4518
   535
## HOL-W0
nipkow@2527
   536
wenzelm@4518
   537
HOL-W0: HOL $(LOG)/HOL-W0.gz
nipkow@2527
   538
wenzelm@12946
   539
$(LOG)/HOL-W0.gz: $(OUT)/HOL W0/ROOT.ML W0/W0.thy W0/document/root.tex
wenzelm@2826
   540
	@$(ISATOOL) usedir $(OUT)/HOL W0
nipkow@2527
   541
nipkow@2527
   542
nipkow@8012
   543
## HOL-MicroJava
nipkow@8012
   544
nipkow@8012
   545
HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
nipkow@8012
   546
haftmann@23854
   547
$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL Library/Executable_Set.thy \
berghofe@17637
   548
  MicroJava/ROOT.ML \
streckem@13672
   549
  MicroJava/Comp/AuxLemmas.thy \
streckem@13672
   550
  MicroJava/Comp/CorrComp.thy \
streckem@13672
   551
  MicroJava/Comp/CorrCompTp.thy \
streckem@13672
   552
  MicroJava/Comp/DefsComp.thy \
streckem@13672
   553
  MicroJava/Comp/Index.thy \
streckem@13672
   554
  MicroJava/Comp/LemmasComp.thy \
streckem@13672
   555
  MicroJava/Comp/NatCanonify.thy \
streckem@13672
   556
  MicroJava/Comp/TranslComp.thy \
streckem@13672
   557
  MicroJava/Comp/TranslCompTp.thy \
streckem@13672
   558
  MicroJava/Comp/TypeInf.thy \
oheimb@11026
   559
  MicroJava/J/Conform.thy MicroJava/J/Eval.thy MicroJava/J/JBasis.thy \
oheimb@11026
   560
  MicroJava/J/JTypeSafe.thy MicroJava/J/Decl.thy MicroJava/J/State.thy \
oheimb@11026
   561
  MicroJava/J/Term.thy MicroJava/J/Type.thy MicroJava/J/TypeRel.thy \
oheimb@11026
   562
  MicroJava/J/WellForm.thy MicroJava/J/Value.thy \
oheimb@11026
   563
  MicroJava/J/WellType.thy MicroJava/J/Example.thy \
berghofe@12438
   564
  MicroJava/J/JListExample.thy \
kleing@9381
   565
  MicroJava/JVM/JVMExec.thy MicroJava/JVM/JVMInstructions.thy\
kleing@9381
   566
  MicroJava/JVM/JVMState.thy MicroJava/JVM/JVMExecInstr.thy\
kleing@12521
   567
  MicroJava/JVM/JVMListExample.thy MicroJava/JVM/JVMExceptions.thy \
nipkow@11228
   568
  MicroJava/BV/BVSpec.thy MicroJava/BV/BVSpecTypeSafe.thy \
nipkow@11228
   569
  MicroJava/BV/Correct.thy MicroJava/BV/Err.thy MicroJava/BV/JType.thy \
nipkow@11228
   570
  MicroJava/BV/JVM.thy MicroJava/BV/JVMType.thy MicroJava/BV/Kildall.thy \
nipkow@11228
   571
  MicroJava/BV/LBVSpec.thy MicroJava/BV/Listn.thy MicroJava/BV/Opt.thy \
nipkow@11228
   572
  MicroJava/BV/Product.thy MicroJava/BV/Semilat.thy \
kleing@12521
   573
  MicroJava/BV/Effect.thy MicroJava/BV/EffectMono.thy \
nipkow@11228
   574
  MicroJava/BV/Typing_Framework.thy MicroJava/BV/Typing_Framework_err.thy \
kleing@13224
   575
  MicroJava/BV/Typing_Framework_JVM.thy MicroJava/BV/BVExample.thy \
kleing@13224
   576
  MicroJava/BV/LBVSpec.thy MicroJava/BV/LBVCorrect.thy \
kleing@13224
   577
  MicroJava/BV/LBVComplete.thy MicroJava/BV/LBVJVM.thy \
kleing@12915
   578
  MicroJava/document/root.bib MicroJava/document/root.tex \
kleing@12915
   579
  MicroJava/document/introduction.tex
wenzelm@11850
   580
	@$(ISATOOL) usedir -g true $(OUT)/HOL MicroJava
wenzelm@11850
   581
nipkow@8012
   582
oheimb@11376
   583
## HOL-NanoJava
oheimb@11376
   584
oheimb@11376
   585
HOL-NanoJava: HOL $(LOG)/HOL-NanoJava.gz
oheimb@11376
   586
oheimb@11376
   587
$(LOG)/HOL-NanoJava.gz: $(OUT)/HOL NanoJava/ROOT.ML \
oheimb@11376
   588
  NanoJava/Term.thy NanoJava/Decl.thy NanoJava/TypeRel.thy NanoJava/State.thy \
oheimb@11376
   589
  NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy \
oheimb@11376
   590
  NanoJava/document/root.bib NanoJava/document/root.tex
wenzelm@11850
   591
	@$(ISATOOL) usedir -g true $(OUT)/HOL NanoJava
wenzelm@11850
   592
wenzelm@8193
   593
schirmer@12855
   594
## HOL-Bali
schirmer@12855
   595
schirmer@12855
   596
HOL-Bali: HOL $(LOG)/HOL-Bali.gz
schirmer@12855
   597
schirmer@12855
   598
$(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/AxCompl.thy Bali/AxExample.thy	\
schirmer@12855
   599
  Bali/AxSem.thy Bali/AxSound.thy Bali/Basis.thy Bali/Conform.thy	\
schirmer@12855
   600
  Bali/Decl.thy Bali/DeclConcepts.thy Bali/Eval.thy Bali/Evaln.thy	\
schirmer@12855
   601
  Bali/Example.thy Bali/Name.thy Bali/ROOT.ML Bali/State.thy		\
schirmer@12855
   602
  Bali/Table.thy Bali/Term.thy Bali/Trans.thy Bali/Type.thy		\
schirmer@12855
   603
  Bali/TypeRel.thy Bali/TypeSafe.thy Bali/Value.thy Bali/WellForm.thy	\
kleing@13695
   604
  Bali/DefiniteAssignment.thy Bali/DefiniteAssignmentCorrect.thy \
schirmer@12855
   605
  Bali/WellType.thy Bali/document/root.tex
schirmer@12855
   606
	@$(ISATOOL) usedir -g true $(OUT)/HOL Bali
schirmer@12855
   607
schirmer@12855
   608
berghofe@13403
   609
## HOL-Extraction
berghofe@13403
   610
berghofe@13403
   611
HOL-Extraction: HOL $(LOG)/HOL-Extraction.gz
berghofe@13403
   612
haftmann@23854
   613
$(LOG)/HOL-Extraction.gz: $(OUT)/HOL Library/Efficient_Nat.thy \
berghofe@17023
   614
  Extraction/Higman.thy Extraction/ROOT.ML Extraction/Pigeonhole.thy \
berghofe@17023
   615
  Extraction/QuotRem.thy \
berghofe@13403
   616
  Extraction/Warshall.thy Extraction/document/root.tex \
berghofe@13403
   617
  Extraction/document/root.bib
berghofe@13403
   618
	@$(ISATOOL) usedir $(OUT)/HOL Extraction
berghofe@13403
   619
berghofe@13403
   620
wenzelm@4518
   621
## HOL-IOA
wenzelm@4518
   622
wenzelm@4518
   623
HOL-IOA: HOL $(LOG)/HOL-IOA.gz
wenzelm@2448
   624
wenzelm@19801
   625
$(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.thy IOA/IOA.thy \
wenzelm@19801
   626
  IOA/ROOT.ML IOA/Solve.thy
wenzelm@4518
   627
	@$(ISATOOL) usedir $(OUT)/HOL IOA
wenzelm@4518
   628
wenzelm@4518
   629
wenzelm@10135
   630
## HOL-AxClasses
wenzelm@4518
   631
wenzelm@10135
   632
HOL-AxClasses: HOL $(LOG)/HOL-AxClasses.gz
wenzelm@2545
   633
wenzelm@10135
   634
$(LOG)/HOL-AxClasses.gz: $(OUT)/HOL AxClasses/Group.thy \
wenzelm@10135
   635
  AxClasses/Product.thy AxClasses/ROOT.ML AxClasses/Semigroups.thy
wenzelm@10135
   636
	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
wenzelm@2545
   637
wenzelm@2545
   638
wenzelm@10157
   639
## HOL-Lattice
wenzelm@10157
   640
wenzelm@10157
   641
HOL-Lattice: HOL $(LOG)/HOL-Lattice.gz
wenzelm@10157
   642
wenzelm@10157
   643
$(LOG)/HOL-Lattice.gz: $(OUT)/HOL Lattice/Bounds.thy \
wenzelm@10157
   644
  Lattice/CompleteLattice.thy Lattice/Lattice.thy Lattice/Orders.thy \
wenzelm@10157
   645
  Lattice/ROOT.ML Lattice/document/root.tex
wenzelm@10157
   646
	@$(ISATOOL) usedir $(OUT)/HOL Lattice
wenzelm@10157
   647
wenzelm@10157
   648
wenzelm@4518
   649
## HOL-ex
wenzelm@2448
   650
wenzelm@4518
   651
HOL-ex: HOL $(LOG)/HOL-ex.gz
wenzelm@2448
   652
webertj@23194
   653
$(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy \
webertj@23194
   654
  ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy \
wenzelm@23213
   655
  ex/BT.thy ex/BinEx.thy ex/CTL.thy \
wenzelm@23454
   656
  ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy ex/Dense_Linear_Order_Ex.thy \
wenzelm@23267
   657
  ex/Eval_Examples.thy ex/Groebner_Examples.thy ex/Random.thy \
haftmann@24194
   658
  ex/Codegenerator.thy ex/Codegenerator_Pretty.thy \
webertj@23194
   659
  ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy \
webertj@23194
   660
  ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy \
webertj@23194
   661
  ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy ex/Binary.thy \
webertj@23194
   662
  ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy ex/InSort.thy \
webertj@23194
   663
  ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \
wenzelm@24326
   664
  ex/Intuitionistic.thy ex/Lagrange.thy ex/Locales.thy ex/LocaleTest2.thy \
webertj@23194
   665
  ex/MT.thy ex/MergeSort.thy ex/MonoidGroup.thy ex/Multiquote.thy \
nipkow@23502
   666
  ex/NatSum.thy ex/NBE.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
webertj@23194
   667
  ex/Puzzle.thy ex/Qsort.thy ex/Quickcheck_Examples.thy \
chaieb@23549
   668
  ex/Reflection.thy ex/reflection_data.ML ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy \
chaieb@23274
   669
  ex/Records.thy ex/Reflected_Presburger.thy ex/coopertac.ML ex/coopereif.ML \
chaieb@23274
   670
  ex/Refute_Examples.thy ex/SAT_Examples.thy ex/svc_oracle.ML ex/SVC_Oracle.thy \
webertj@23194
   671
  ex/Sudoku.thy ex/Tarski.thy ex/Unification.thy ex/document/root.bib \
wenzelm@24127
   672
  ex/document/root.tex ex/Meson_Test.thy ex/reflection.ML \
krauss@23003
   673
  ex/set.thy ex/svc_funcs.ML ex/svc_test.thy Library/Parity.thy Library/GCD.thy
wenzelm@2826
   674
	@$(ISATOOL) usedir $(OUT)/HOL ex
wenzelm@2448
   675
wenzelm@2448
   676
wenzelm@6445
   677
## HOL-Isar_examples
wenzelm@6445
   678
wenzelm@6445
   679
HOL-Isar_examples: HOL $(LOG)/HOL-Isar_examples.gz
wenzelm@6445
   680
wenzelm@6445
   681
$(LOG)/HOL-Isar_examples.gz: $(OUT)/HOL Isar_examples/BasicLogic.thy \
wenzelm@20767
   682
  Isar_examples/Cantor.thy Isar_examples/Drinker.thy \
wenzelm@8050
   683
  Isar_examples/ExprCompiler.thy Isar_examples/Fibonacci.thy \
wenzelm@10143
   684
  Isar_examples/Group.thy Isar_examples/Hoare.thy Isar_examples/HoareEx.thy \
wenzelm@10255
   685
  Isar_examples/KnasterTarski.thy Isar_examples/MutilatedCheckerboard.thy \
wenzelm@8677
   686
  Isar_examples/NestedDatatype.thy Isar_examples/Peirce.thy \
wenzelm@8050
   687
  Isar_examples/Puzzle.thy Isar_examples/Summation.thy \
wenzelm@12946
   688
  Isar_examples/ROOT.ML Isar_examples/document/proof.sty \
wenzelm@12946
   689
  Isar_examples/document/root.bib Isar_examples/document/root.tex \
kleing@13703
   690
  Isar_examples/document/style.tex Hoare/hoare.ML
wenzelm@6445
   691
	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
wenzelm@6445
   692
wenzelm@6445
   693
paulson@14199
   694
## HOL-SET-Protocol
paulson@14199
   695
paulson@14199
   696
HOL-SET-Protocol: HOL $(LOG)/HOL-SET-Protocol.gz
paulson@14199
   697
paulson@14199
   698
$(LOG)/HOL-SET-Protocol.gz: $(OUT)/HOL SET-Protocol/ROOT.ML \
paulson@14199
   699
  SET-Protocol/MessageSET.thy\
paulson@14199
   700
  SET-Protocol/EventSET.thy\
paulson@14199
   701
  SET-Protocol/PublicSET.thy\
paulson@14199
   702
  SET-Protocol/Cardholder_Registration.thy\
paulson@14199
   703
  SET-Protocol/Merchant_Registration.thy\
paulson@14199
   704
  SET-Protocol/Purchase.thy\
paulson@14199
   705
  SET-Protocol/document/root.tex 
paulson@14199
   706
	@$(ISATOOL) usedir -g true $(OUT)/HOL SET-Protocol
paulson@14199
   707
paulson@14199
   708
wenzelm@16509
   709
## HOL-Complex-Matrix
kleing@14610
   710
wenzelm@17546
   711
HOL-Complex-Matrix: HOL-Complex $(OUT)/HOL-Complex-Matrix
obua@17323
   712
obua@17323
   713
$(OUT)/HOL-Complex-Matrix: $(OUT)/HOL-Complex \
wenzelm@23172
   714
  $(SRC)/Tools/Compute_Oracle/Compute_Oracle.thy \
wenzelm@23172
   715
  $(SRC)/Tools/Compute_Oracle/am_compiler.ML \
wenzelm@23172
   716
  $(SRC)/Tools/Compute_Oracle/am_interpreter.ML \
obua@23772
   717
  $(SRC)/Tools/Compute_Oracle/am.ML \
obua@23772
   718
  $(SRC)/Tools/Compute_Oracle/linker.ML \
obua@23772
   719
  $(SRC)/Tools/Compute_Oracle/am_ghc.ML \
obua@23772
   720
  $(SRC)/Tools/Compute_Oracle/am_sml.ML \
webertj@23194
   721
  $(SRC)/Tools/Compute_Oracle/compute.ML \
wenzelm@23172
   722
  Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
wenzelm@23172
   723
  Matrix/LP.thy Matrix/document/root.tex Matrix/ROOT.ML \
obua@17489
   724
  Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
obua@16784
   725
  Matrix/cplex/Cplex_tools.ML Matrix/cplex/FloatSparseMatrix.thy \
obua@16873
   726
  Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \
wenzelm@20787
   727
  Matrix/cplex/MatrixLP.thy Matrix/cplex/matrixlp.ML
obua@17323
   728
	@cd Matrix; $(ISATOOL) usedir -b -g true $(OUT)/HOL-Complex HOL-Complex-Matrix
obua@16873
   729
paulson@14199
   730
wenzelm@4518
   731
## TLA
wenzelm@4518
   732
wenzelm@4518
   733
TLA: HOL $(OUT)/TLA
wenzelm@4518
   734
wenzelm@21624
   735
$(OUT)/TLA: $(OUT)/HOL TLA/Action.thy TLA/Init.thy TLA/Intensional.thy \
wenzelm@21624
   736
  TLA/ROOT.ML TLA/Stfun.thy TLA/TLA.thy
wenzelm@4518
   737
	@cd TLA; $(ISATOOL) usedir -b $(OUT)/HOL TLA
wenzelm@4518
   738
wenzelm@4518
   739
wenzelm@4518
   740
## TLA-Inc
wenzelm@4518
   741
wenzelm@4518
   742
TLA-Inc: TLA $(LOG)/TLA-Inc.gz
wenzelm@4518
   743
wenzelm@21624
   744
$(LOG)/TLA-Inc.gz: $(OUT)/TLA TLA/Inc/Inc.thy
wenzelm@4518
   745
	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Inc
wenzelm@4518
   746
wenzelm@4518
   747
wenzelm@4518
   748
## TLA-Buffer
wenzelm@4518
   749
wenzelm@4518
   750
TLA-Buffer: TLA $(LOG)/TLA-Buffer.gz
wenzelm@2448
   751
wenzelm@21624
   752
$(LOG)/TLA-Buffer.gz: $(OUT)/TLA TLA/Buffer/Buffer.thy TLA/Buffer/DBuffer.thy
wenzelm@4518
   753
	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Buffer
wenzelm@4518
   754
wenzelm@4518
   755
wenzelm@4518
   756
## TLA-Memory
wenzelm@4518
   757
wenzelm@4518
   758
TLA-Memory: TLA $(LOG)/TLA-Memory.gz
wenzelm@4447
   759
wenzelm@4518
   760
$(LOG)/TLA-Memory.gz: $(OUT)/TLA TLA/Memory/MIParameters.thy \
wenzelm@21624
   761
  TLA/Memory/MemClerk.thy TLA/Memory/MemClerkParameters.thy \
wenzelm@21624
   762
  TLA/Memory/Memory.thy TLA/Memory/MemoryImplementation.thy \
webertj@23194
   763
  TLA/Memory/MemoryParameters.thy TLA/Memory/ProcedureInterface.thy \
webertj@23194
   764
  TLA/Memory/RPC.thy \
wenzelm@21624
   765
  TLA/Memory/RPCMemoryParams.thy TLA/Memory/RPCParameters.thy
wenzelm@4518
   766
	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Memory
wenzelm@4518
   767
wenzelm@4518
   768
berghofe@19497
   769
## HOL-Nominal
berghofe@19497
   770
berghofe@19497
   771
HOL-Nominal: HOL $(OUT)/HOL-Nominal
berghofe@19497
   772
urbanc@22245
   773
$(OUT)/HOL-Nominal: $(OUT)/HOL Nominal/ROOT.ML \
urbanc@22245
   774
  Nominal/Nominal.thy \
urbanc@22245
   775
  Nominal/nominal_atoms.ML \
berghofe@22784
   776
  Nominal/nominal_fresh_fun.ML \
urbanc@22247
   777
  Nominal/nominal_induct.ML \
berghofe@22314
   778
  Nominal/nominal_inductive.ML \
urbanc@22245
   779
  Nominal/nominal_package.ML \
urbanc@22245
   780
  Nominal/nominal_permeq.ML \
urbanc@22245
   781
  Nominal/nominal_primrec.ML \
urbanc@22245
   782
  Nominal/nominal_thmdecls.ML \
berghofe@21542
   783
  Library/Infinite_Set.thy
berghofe@19497
   784
	@cd Nominal; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Nominal
berghofe@19497
   785
berghofe@19497
   786
berghofe@19497
   787
## HOL-Nominal-Examples
berghofe@19497
   788
berghofe@19497
   789
HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz
berghofe@19497
   790
krauss@19564
   791
$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal 	\
urbanc@22077
   792
  Nominal/Examples/ROOT.ML \
urbanc@22073
   793
  Nominal/Examples/CR.thy \
urbanc@22821
   794
  Nominal/Examples/CR_Takahashi.thy \
wenzelm@24152
   795
  Nominal/Examples/Class.thy \
urbanc@22073
   796
  Nominal/Examples/Compile.thy \
urbanc@22073
   797
  Nominal/Examples/Fsub.thy \
urbanc@22073
   798
  Nominal/Examples/Lambda_mu.thy \
urbanc@22073
   799
  Nominal/Examples/Lam_Funs.thy	\
urbanc@22073
   800
  Nominal/Examples/SN.thy \
urbanc@22073
   801
  Nominal/Examples/Weakening.thy \
urbanc@22448
   802
  Nominal/Examples/Crary.thy \
urbanc@23144
   803
  Nominal/Examples/SOS.thy \
urbanc@23144
   804
  Nominal/Examples/LocalWeakening.thy
berghofe@19497
   805
	@cd Nominal; $(ISATOOL) usedir $(OUT)/HOL-Nominal Examples
berghofe@19497
   806
berghofe@19497
   807
kleing@24333
   808
## HOL-Word
kleing@24333
   809
kleing@24333
   810
HOL-Word: HOL $(OUT)/HOL-Word
kleing@24333
   811
kleing@24333
   812
$(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML \
kleing@24333
   813
  Library/Infinite_Set.thy Library/Parity.thy \
kleing@24333
   814
  Library/Boolean_Algebra.thy Library/Numeral_Type.thy \
kleing@24333
   815
  Word/Num_Lemmas.thy \
kleing@24333
   816
  Word/TdThs.thy \
kleing@24333
   817
  Word/Size.thy \
kleing@24333
   818
  Word/BinGeneral.thy \
kleing@24333
   819
  Word/BinOperations.thy \
kleing@24333
   820
  Word/BinBoolList.thy \
kleing@24333
   821
  Word/BitSyntax.thy \
kleing@24333
   822
  Word/WordDefinition.thy \
kleing@24333
   823
  Word/WordArith.thy \
kleing@24333
   824
  Word/WordBitwise.thy \
kleing@24333
   825
  Word/WordShift.thy \
kleing@24333
   826
  Word/WordGenLib.thy \
kleing@24333
   827
  Word/WordMain.thy \
kleing@24333
   828
  Word/WordExamples.thy
kleing@24333
   829
	@cd Word; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Word
kleing@24333
   830
kleing@24333
   831
wenzelm@4518
   832
## clean
wenzelm@4447
   833
wenzelm@4447
   834
clean:
berghofe@19497
   835
	@rm -f  $(OUT)/HOL $(OUT)/HOL-Complex $(OUT)/HOL-Nominal $(OUT)/TLA \
paulson@13980
   836
		$(LOG)/HOL.gz $(LOG)/TLA.gz \
wenzelm@9481
   837
		$(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \
wenzelm@9481
   838
		$(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \
wenzelm@9481
   839
		$(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \
prensani@12996
   840
		$(LOG)/HOL-HoareParallel.gz \
wenzelm@9481
   841
		$(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
wenzelm@9481
   842
		$(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
wenzelm@9481
   843
		$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
bauerg@15871
   844
                $(LOG)/HOL-Bali.gz \
oheimb@11376
   845
		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
berghofe@19497
   846
                $(LOG)/HOL-Nominal-Examples.gz \
wenzelm@10135
   847
		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
wenzelm@16509
   848
		$(LOG)/HOL-Lattice $(LOG)/HOL-Complex-Matrix \
paulson@13980
   849
		$(LOG)/HOL-Complex.gz \
paulson@13961
   850
		$(LOG)/HOL-Complex-ex.gz \
paulson@14199
   851
		$(LOG)/HOL-Complex-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz \
paulson@14199
   852
                $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz \
wenzelm@10981
   853
		$(LOG)/HOL-Library.gz $(LOG)/HOL-Unix.gz