src/HOL/IsaMakefile
author hoelzl
Mon Aug 23 19:35:57 2010 +0200 (2010-08-23)
changeset 38656 d5d342611edb
parent 38622 86fc906dcd86
child 38730 5bbdd9a9df62
permissions -rw-r--r--
Rewrite the Probability theory.

Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.
haftmann@36147
     1
wenzelm@2448
     2
#
wenzelm@2448
     3
# IsaMakefile for HOL
wenzelm@2448
     4
#
wenzelm@2448
     5
wenzelm@4518
     6
## targets
wenzelm@2448
     7
wenzelm@4518
     8
default: HOL
haftmann@27421
     9
generate: HOL-Generate-HOL HOL-Generate-HOLLight
wenzelm@33210
    10
wenzelm@33210
    11
images: \
wenzelm@33210
    12
  HOL \
haftmann@37691
    13
  HOL-Library \
wenzelm@33210
    14
  HOL-Algebra \
boehmes@33419
    15
  HOL-Boogie \
wenzelm@33210
    16
  HOL-Multivariate_Analysis \
wenzelm@33210
    17
  HOL-NSA \
wenzelm@33210
    18
  HOL-Nominal \
wenzelm@35931
    19
  HOL-Probability \
wenzelm@34205
    20
  HOL-Proofs \
wenzelm@33210
    21
  HOL-Word \
wenzelm@33210
    22
  HOL4 \
haftmann@37691
    23
  TLA \
haftmann@37691
    24
  HOL-Base \
haftmann@37691
    25
  HOL-Main \
haftmann@37691
    26
  HOL-Plain
wenzelm@10135
    27
haftmann@37691
    28
#Note: keep targets sorted (except for HOL-ex)
wenzelm@10157
    29
test: \
wenzelm@24325
    30
  HOL-ex \
wenzelm@10157
    31
  HOL-Auth \
schirmer@14031
    32
  HOL-Bali \
wenzelm@33439
    33
  HOL-Boogie-Examples \
haftmann@29823
    34
  HOL-Decision_Procs \
wenzelm@31795
    35
  HOL-Hahn_Banach \
wenzelm@10157
    36
  HOL-Hoare \
haftmann@32621
    37
  HOL-Hoare_Parallel \
wenzelm@10157
    38
  HOL-IMP \
wenzelm@10157
    39
  HOL-IMPP \
wenzelm@10157
    40
  HOL-IOA \
haftmann@29399
    41
  HOL-Imperative_HOL \
wenzelm@33210
    42
  HOL-Import \
wenzelm@10157
    43
  HOL-Induct \
wenzelm@33026
    44
  HOL-Isar_Examples \
wenzelm@10157
    45
  HOL-Lattice \
haftmann@37747
    46
  HOL-Library-Codegenerator_Test \
wenzelm@28637
    47
  HOL-Matrix \
wenzelm@33027
    48
  HOL-Metis_Examples \
wenzelm@10157
    49
  HOL-MicroJava \
boehmes@32496
    50
  HOL-Mirabelle \
bulwahn@35536
    51
  HOL-Mutabelle \
oheimb@11376
    52
  HOL-NanoJava \
blanchet@33197
    53
  HOL-Nitpick_Examples \
berghofe@19497
    54
  HOL-Nominal-Examples \
haftmann@32479
    55
  HOL-Number_Theory \
haftmann@32479
    56
  HOL-Old_Number_Theory \
kaliszyk@35222
    57
  HOL-Quotient_Examples \
bulwahn@35950
    58
  HOL-Predicate_Compile_Examples \
wenzelm@10157
    59
  HOL-Prolog \
wenzelm@34205
    60
  HOL-Proofs-Extraction \
wenzelm@34205
    61
  HOL-Proofs-Lambda \
wenzelm@33028
    62
  HOL-SET_Protocol \
wenzelm@36933
    63
  HOL-Word-SMT_Examples \
schirmer@25171
    64
  HOL-Statespace \
wenzelm@10157
    65
  HOL-Subst \
wenzelm@33210
    66
      TLA-Buffer \
wenzelm@33210
    67
      TLA-Inc \
wenzelm@33210
    68
      TLA-Memory \
wenzelm@10157
    69
  HOL-UNITY \
wenzelm@10966
    70
  HOL-Unix \
huffman@24442
    71
  HOL-Word-Examples \
wenzelm@24325
    72
  HOL-ZF
wenzelm@10157
    73
    # ^ this is the sort position
wenzelm@10614
    74
wenzelm@10157
    75
all: test images
wenzelm@4518
    76
wenzelm@4518
    77
wenzelm@4518
    78
## global settings
wenzelm@4518
    79
wenzelm@4518
    80
SRC = $(ISABELLE_HOME)/src
wenzelm@3118
    81
OUT = $(ISABELLE_OUTPUT)
wenzelm@4447
    82
LOG = $(OUT)/log
wenzelm@2448
    83
wenzelm@4518
    84
wenzelm@4518
    85
## HOL
wenzelm@2448
    86
wenzelm@28393
    87
HOL: Pure $(OUT)/HOL
haftmann@27368
    88
haftmann@29505
    89
HOL-Base: Pure $(OUT)/HOL-Base
haftmann@29505
    90
haftmann@27368
    91
HOL-Plain: Pure $(OUT)/HOL-Plain
wenzelm@4518
    92
haftmann@28401
    93
HOL-Main: Pure $(OUT)/HOL-Main
haftmann@28401
    94
wenzelm@34205
    95
HOL-Proofs: Pure $(OUT)/HOL-Proofs
wenzelm@34205
    96
wenzelm@4518
    97
Pure:
wenzelm@28500
    98
	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
paulson@3232
    99
haftmann@27694
   100
$(OUT)/Pure: Pure
haftmann@27694
   101
wenzelm@36073
   102
BASE_DEPENDENCIES = $(OUT)/Pure \
wenzelm@30160
   103
  $(SRC)/Provers/blast.ML \
wenzelm@30160
   104
  $(SRC)/Provers/clasimp.ML \
wenzelm@30160
   105
  $(SRC)/Provers/classical.ML \
wenzelm@30160
   106
  $(SRC)/Provers/hypsubst.ML \
wenzelm@30160
   107
  $(SRC)/Provers/quantifier1.ML \
wenzelm@30160
   108
  $(SRC)/Provers/splitter.ML \
haftmann@37818
   109
  $(SRC)/Tools/cache_io.ML \
haftmann@34028
   110
  $(SRC)/Tools/Code/code_eval.ML \
haftmann@31771
   111
  $(SRC)/Tools/Code/code_haskell.ML \
haftmann@31771
   112
  $(SRC)/Tools/Code/code_ml.ML \
haftmann@31771
   113
  $(SRC)/Tools/Code/code_preproc.ML \
haftmann@31771
   114
  $(SRC)/Tools/Code/code_printer.ML \
haftmann@34945
   115
  $(SRC)/Tools/Code/code_scala.ML \
haftmann@37442
   116
  $(SRC)/Tools/Code/code_simp.ML \
haftmann@31771
   117
  $(SRC)/Tools/Code/code_target.ML \
haftmann@31771
   118
  $(SRC)/Tools/Code/code_thingol.ML \
wenzelm@32733
   119
  $(SRC)/Tools/Code_Generator.thy \
wenzelm@32733
   120
  $(SRC)/Tools/IsaPlanner/isand.ML \
wenzelm@32733
   121
  $(SRC)/Tools/IsaPlanner/rw_inst.ML \
wenzelm@32733
   122
  $(SRC)/Tools/IsaPlanner/rw_tools.ML \
wenzelm@32733
   123
  $(SRC)/Tools/IsaPlanner/zipper.ML \
wenzelm@32733
   124
  $(SRC)/Tools/atomize_elim.ML \
blanchet@33561
   125
  $(SRC)/Tools/auto_counterexample.ML \
wenzelm@32733
   126
  $(SRC)/Tools/auto_solve.ML \
wenzelm@30160
   127
  $(SRC)/Tools/coherent.ML \
wenzelm@32733
   128
  $(SRC)/Tools/cong_tac.ML \
wenzelm@30160
   129
  $(SRC)/Tools/eqsubst.ML \
wenzelm@30160
   130
  $(SRC)/Tools/induct.ML \
wenzelm@32733
   131
  $(SRC)/Tools/induct_tacs.ML \
wenzelm@30165
   132
  $(SRC)/Tools/intuitionistic.ML \
wenzelm@37781
   133
  $(SRC)/Tools/misc_legacy.ML \
wenzelm@30160
   134
  $(SRC)/Tools/nbe.ML \
wenzelm@32733
   135
  $(SRC)/Tools/project_rule.ML \
haftmann@30973
   136
  $(SRC)/Tools/quickcheck.ML \
wenzelm@30160
   137
  $(SRC)/Tools/random_word.ML \
wenzelm@30160
   138
  $(SRC)/Tools/value.ML \
haftmann@29505
   139
  HOL.thy \
haftmann@29505
   140
  Tools/hologic.ML \
haftmann@29505
   141
  Tools/recfun_codegen.ML \
wenzelm@36073
   142
  Tools/simpdata.ML
haftmann@29505
   143
haftmann@29505
   144
$(OUT)/HOL-Base: base.ML $(BASE_DEPENDENCIES)
haftmann@29523
   145
	@$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base
haftmann@29505
   146
haftmann@29505
   147
PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES)\
haftmann@32139
   148
  Complete_Lattice.thy \
haftmann@27368
   149
  Datatype.thy \
haftmann@27368
   150
  Extraction.thy \
haftmann@35050
   151
  Fields.thy \
haftmann@27368
   152
  Finite_Set.thy \
haftmann@27368
   153
  Fun.thy \
haftmann@27368
   154
  FunDef.thy \
haftmann@35050
   155
  Groups.thy \
haftmann@27368
   156
  Inductive.thy \
haftmann@27368
   157
  Lattices.thy \
haftmann@27368
   158
  Nat.thy \
wenzelm@32733
   159
  Option.thy \
haftmann@27368
   160
  Orderings.thy \
haftmann@27368
   161
  Plain.thy \
haftmann@27368
   162
  Power.thy \
haftmann@27368
   163
  Predicate.thy \
haftmann@27368
   164
  Product_Type.thy \
haftmann@27368
   165
  Record.thy \
haftmann@27368
   166
  Relation.thy \
haftmann@35050
   167
  Rings.thy \
haftmann@27368
   168
  SAT.thy \
haftmann@27368
   169
  Set.thy \
haftmann@27368
   170
  Sum_Type.thy \
haftmann@37884
   171
  Tools/abel_cancel.ML \
haftmann@28952
   172
  Tools/arith_data.ML \
haftmann@27368
   173
  Tools/cnf_funcs.ML \
haftmann@31771
   174
  Tools/Datatype/datatype_abs_proofs.ML \
haftmann@31771
   175
  Tools/Datatype/datatype_aux.ML \
haftmann@31771
   176
  Tools/Datatype/datatype_case.ML \
haftmann@31771
   177
  Tools/Datatype/datatype_codegen.ML \
haftmann@33963
   178
  Tools/Datatype/datatype_data.ML \
haftmann@31771
   179
  Tools/Datatype/datatype_prop.ML \
haftmann@31771
   180
  Tools/Datatype/datatype_realizer.ML \
haftmann@33963
   181
  Tools/Datatype/datatype.ML \
haftmann@27368
   182
  Tools/dseq.ML \
haftmann@31771
   183
  Tools/Function/context_tree.ML \
krauss@33099
   184
  Tools/Function/function_common.ML \
krauss@33099
   185
  Tools/Function/function_core.ML \
krauss@33099
   186
  Tools/Function/function_lib.ML \
krauss@33099
   187
  Tools/Function/function.ML \
krauss@33098
   188
  Tools/Function/fun.ML \
krauss@33471
   189
  Tools/Function/induction_schema.ML \
haftmann@31771
   190
  Tools/Function/lexicographic_order.ML \
haftmann@31771
   191
  Tools/Function/measure_functions.ML \
haftmann@31771
   192
  Tools/Function/mutual.ML \
krauss@33083
   193
  Tools/Function/pat_completeness.ML \
haftmann@31771
   194
  Tools/Function/pattern_split.ML \
krauss@33100
   195
  Tools/Function/relation.ML \
haftmann@31771
   196
  Tools/Function/scnp_reconstruct.ML \
haftmann@31771
   197
  Tools/Function/scnp_solve.ML \
haftmann@31771
   198
  Tools/Function/size.ML \
haftmann@31771
   199
  Tools/Function/sum_tree.ML \
haftmann@31771
   200
  Tools/Function/termination.ML \
haftmann@27368
   201
  Tools/inductive_codegen.ML \
haftmann@31723
   202
  Tools/inductive.ML \
haftmann@27368
   203
  Tools/inductive_realizer.ML \
haftmann@31723
   204
  Tools/inductive_set.ML \
haftmann@27368
   205
  Tools/lin_arith.ML \
haftmann@30496
   206
  Tools/nat_arith.ML \
haftmann@31723
   207
  Tools/old_primrec.ML \
haftmann@31723
   208
  Tools/primrec.ML \
haftmann@27368
   209
  Tools/prop_logic.ML \
haftmann@27368
   210
  Tools/refute.ML \
haftmann@27368
   211
  Tools/refute_isar.ML \
haftmann@27368
   212
  Tools/rewrite_hol_proof.ML \
haftmann@27368
   213
  Tools/sat_funcs.ML \
haftmann@27368
   214
  Tools/sat_solver.ML \
haftmann@27368
   215
  Tools/split_rule.ML \
haftmann@31723
   216
  Tools/typedef.ML \
haftmann@27368
   217
  Transitive_Closure.thy \
haftmann@27368
   218
  Typedef.thy \
haftmann@27368
   219
  Wellfounded.thy \
haftmann@27368
   220
  $(SRC)/Provers/Arith/cancel_div_mod.ML \
haftmann@27368
   221
  $(SRC)/Provers/Arith/cancel_sums.ML \
haftmann@27368
   222
  $(SRC)/Provers/Arith/fast_lin_arith.ML \
haftmann@27368
   223
  $(SRC)/Provers/order.ML \
haftmann@27368
   224
  $(SRC)/Provers/trancl.ML \
haftmann@27368
   225
  $(SRC)/Tools/rat.ML
haftmann@28312
   226
haftmann@28312
   227
$(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES)
wenzelm@28500
   228
	@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
haftmann@27368
   229
haftmann@28401
   230
MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
haftmann@35725
   231
  Big_Operators.thy \
haftmann@32657
   232
  Code_Evaluation.thy \
haftmann@31205
   233
  Code_Numeral.thy \
haftmann@33296
   234
  Divides.thy \
bulwahn@34948
   235
  DSequence.thy \
haftmann@27368
   236
  Equiv_Relations.thy \
haftmann@27368
   237
  Groebner_Basis.thy \
haftmann@27368
   238
  Hilbert_Choice.thy \
wenzelm@32733
   239
  Int.thy \
bulwahn@34948
   240
  Lazy_Sequence.thy \
haftmann@27421
   241
  List.thy \
haftmann@27421
   242
  Main.thy \
haftmann@27421
   243
  Map.thy \
haftmann@30925
   244
  Nat_Numeral.thy \
haftmann@33318
   245
  Nat_Transfer.thy \
blanchet@36915
   246
  Nitpick.thy \
haftmann@33356
   247
  Numeral_Simprocs.thy \
haftmann@27421
   248
  Presburger.thy \
bulwahn@33250
   249
  Predicate_Compile.thy \
haftmann@31203
   250
  Quickcheck.thy \
kaliszyk@35222
   251
  Quotient.thy \
haftmann@31203
   252
  Random.thy \
bulwahn@34948
   253
  Random_Sequence.thy \
haftmann@27421
   254
  Recdef.thy \
blanchet@36916
   255
  Refute.thy \
haftmann@36751
   256
  Semiring_Normalization.thy \
haftmann@27421
   257
  SetInterval.thy \
blanchet@35827
   258
  Sledgehammer.thy \
boehmes@36898
   259
  SMT.thy \
haftmann@31048
   260
  String.thy \
haftmann@31203
   261
  Typerep.thy \
haftmann@27421
   262
  $(SRC)/Provers/Arith/assoc_fold.ML \
haftmann@27421
   263
  $(SRC)/Provers/Arith/cancel_numeral_factor.ML \
haftmann@27421
   264
  $(SRC)/Provers/Arith/cancel_numerals.ML \
haftmann@27421
   265
  $(SRC)/Provers/Arith/combine_numerals.ML \
haftmann@27421
   266
  $(SRC)/Provers/Arith/extract_common_term.ML \
haftmann@27421
   267
  $(SRC)/Tools/Metis/metis.ML \
blanchet@38047
   268
  Tools/ATP/async_manager.ML \
blanchet@38047
   269
  Tools/ATP/atp_problem.ML \
blanchet@38047
   270
  Tools/ATP/atp_systems.ML \
haftmann@33318
   271
  Tools/choice_specification.ML \
haftmann@31068
   272
  Tools/int_arith.ML \
haftmann@36753
   273
  Tools/groebner.ML \
haftmann@31055
   274
  Tools/list_code.ML \
haftmann@27421
   275
  Tools/meson.ML \
haftmann@31068
   276
  Tools/nat_numeral_simprocs.ML \
blanchet@36915
   277
  Tools/Nitpick/kodkod.ML \
blanchet@36915
   278
  Tools/Nitpick/kodkod_sat.ML \
blanchet@36915
   279
  Tools/Nitpick/minipick.ML \
blanchet@36915
   280
  Tools/Nitpick/nitpick.ML \
blanchet@36915
   281
  Tools/Nitpick/nitpick_hol.ML \
blanchet@36915
   282
  Tools/Nitpick/nitpick_isar.ML \
blanchet@36915
   283
  Tools/Nitpick/nitpick_kodkod.ML \
blanchet@36915
   284
  Tools/Nitpick/nitpick_model.ML \
blanchet@36915
   285
  Tools/Nitpick/nitpick_mono.ML \
blanchet@36915
   286
  Tools/Nitpick/nitpick_nut.ML \
blanchet@36915
   287
  Tools/Nitpick/nitpick_peephole.ML \
blanchet@36915
   288
  Tools/Nitpick/nitpick_preproc.ML \
blanchet@36915
   289
  Tools/Nitpick/nitpick_rep.ML \
blanchet@36915
   290
  Tools/Nitpick/nitpick_scope.ML \
blanchet@36915
   291
  Tools/Nitpick/nitpick_tests.ML \
blanchet@36915
   292
  Tools/Nitpick/nitpick_util.ML \
haftmann@27421
   293
  Tools/numeral.ML \
haftmann@31068
   294
  Tools/numeral_simprocs.ML \
haftmann@27421
   295
  Tools/numeral_syntax.ML \
bulwahn@33250
   296
  Tools/Predicate_Compile/predicate_compile_aux.ML \
bulwahn@36046
   297
  Tools/Predicate_Compile/predicate_compile_compilations.ML \
bulwahn@33250
   298
  Tools/Predicate_Compile/predicate_compile_core.ML \
bulwahn@33250
   299
  Tools/Predicate_Compile/predicate_compile_data.ML \
bulwahn@33250
   300
  Tools/Predicate_Compile/predicate_compile_fun.ML \
bulwahn@33250
   301
  Tools/Predicate_Compile/predicate_compile.ML \
bulwahn@36032
   302
  Tools/Predicate_Compile/predicate_compile_specialisation.ML \
bulwahn@33250
   303
  Tools/Predicate_Compile/predicate_compile_pred.ML \
haftmann@31260
   304
  Tools/quickcheck_generators.ML \
haftmann@27421
   305
  Tools/Qelim/cooper.ML \
haftmann@36803
   306
  Tools/Qelim/cooper_procedure.ML \
haftmann@27421
   307
  Tools/Qelim/qelim.ML \
kaliszyk@35222
   308
  Tools/Quotient/quotient_def.ML \
kaliszyk@35222
   309
  Tools/Quotient/quotient_info.ML \
kaliszyk@35222
   310
  Tools/Quotient/quotient_tacs.ML \
kaliszyk@35222
   311
  Tools/Quotient/quotient_term.ML \
kaliszyk@35222
   312
  Tools/Quotient/quotient_typ.ML \
haftmann@31723
   313
  Tools/recdef.ML \
haftmann@38394
   314
  Tools/record.ML \
haftmann@36753
   315
  Tools/semiring_normalizer.ML \
blanchet@37574
   316
  Tools/Sledgehammer/clausifier.ML \
blanchet@35865
   317
  Tools/Sledgehammer/meson_tactic.ML \
blanchet@37578
   318
  Tools/Sledgehammer/metis_clauses.ML \
blanchet@35825
   319
  Tools/Sledgehammer/metis_tactics.ML \
blanchet@38021
   320
  Tools/Sledgehammer/sledgehammer.ML \
blanchet@35825
   321
  Tools/Sledgehammer/sledgehammer_fact_filter.ML \
blanchet@38282
   322
  Tools/Sledgehammer/sledgehammer_fact_minimize.ML \
blanchet@35866
   323
  Tools/Sledgehammer/sledgehammer_isar.ML \
blanchet@35825
   324
  Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \
blanchet@38282
   325
  Tools/Sledgehammer/sledgehammer_translate.ML \
blanchet@35967
   326
  Tools/Sledgehammer/sledgehammer_util.ML \
boehmes@36898
   327
  Tools/SMT/cvc3_solver.ML \
boehmes@36898
   328
  Tools/SMT/smtlib_interface.ML \
boehmes@36898
   329
  Tools/SMT/smt_monomorph.ML \
boehmes@36898
   330
  Tools/SMT/smt_normalize.ML \
boehmes@36898
   331
  Tools/SMT/smt_solver.ML \
boehmes@36898
   332
  Tools/SMT/smt_translate.ML \
boehmes@36898
   333
  Tools/SMT/yices_solver.ML \
boehmes@36898
   334
  Tools/SMT/z3_interface.ML \
boehmes@36898
   335
  Tools/SMT/z3_model.ML \
boehmes@36898
   336
  Tools/SMT/z3_proof_literals.ML \
boehmes@36898
   337
  Tools/SMT/z3_proof_parser.ML \
boehmes@36898
   338
  Tools/SMT/z3_proof_reconstruction.ML \
boehmes@36898
   339
  Tools/SMT/z3_proof_tools.ML \
boehmes@36898
   340
  Tools/SMT/z3_solver.ML \
haftmann@31055
   341
  Tools/string_code.ML \
haftmann@27421
   342
  Tools/string_syntax.ML \
haftmann@33318
   343
  Tools/transfer.ML \
haftmann@27421
   344
  Tools/TFL/casesplit.ML \
haftmann@27421
   345
  Tools/TFL/dcterm.ML \
haftmann@27421
   346
  Tools/TFL/post.ML \
haftmann@27421
   347
  Tools/TFL/rules.ML \
haftmann@27421
   348
  Tools/TFL/tfl.ML \
haftmann@27421
   349
  Tools/TFL/thms.ML \
haftmann@27421
   350
  Tools/TFL/thry.ML \
haftmann@27421
   351
  Tools/TFL/usyntax.ML \
wenzelm@28477
   352
  Tools/TFL/utils.ML
haftmann@28401
   353
haftmann@28401
   354
$(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES)
wenzelm@28500
   355
	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
haftmann@28401
   356
haftmann@37292
   357
$(OUT)/HOL-Proofs: main.ML $(MAIN_DEPENDENCIES)
haftmann@37292
   358
	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true -p 2 -q 0 $(OUT)/Pure HOL-Proofs
haftmann@37292
   359
wenzelm@34205
   360
HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \
huffman@30096
   361
  Archimedean_Field.thy \
wenzelm@32733
   362
  Complex.thy \
haftmann@28952
   363
  Complex_Main.thy \
haftmann@28952
   364
  Deriv.thy \
haftmann@28952
   365
  Fact.thy \
haftmann@32479
   366
  GCD.thy \
haftmann@28952
   367
  Lim.thy \
huffman@31352
   368
  Limits.thy \
haftmann@28952
   369
  Ln.thy \
haftmann@28952
   370
  Log.thy \
haftmann@32479
   371
  Lubs.thy \
haftmann@28952
   372
  MacLaurin.thy \
haftmann@28952
   373
  NthRoot.thy \
wenzelm@32733
   374
  Parity.thy \
wenzelm@32733
   375
  RComplete.thy \
haftmann@35372
   376
  Rat.thy \
wenzelm@32733
   377
  Real.thy \
wenzelm@32733
   378
  RealDef.thy \
wenzelm@32733
   379
  RealVector.thy \
haftmann@29197
   380
  SEQ.thy \
haftmann@28952
   381
  Series.thy \
paulson@33269
   382
  SupInf.thy \
haftmann@28952
   383
  Taylor.thy \
haftmann@28952
   384
  Transcendental.thy \
haftmann@28952
   385
  Tools/float_syntax.ML \
boehmes@36899
   386
  Tools/SMT/smt_real.ML
wenzelm@34205
   387
wenzelm@34205
   388
$(OUT)/HOL: ROOT.ML $(HOL_DEPENDENCIES)
wenzelm@34205
   389
	@$(ISABELLE_TOOL) usedir -b -g true $(OUT)/Pure HOL
wenzelm@34205
   390
wenzelm@7535
   391
wenzelm@7535
   392
wenzelm@10255
   393
## HOL-Library
wenzelm@10255
   394
haftmann@37691
   395
HOL-Library: HOL $(OUT)/HOL-Library
wenzelm@10255
   396
wenzelm@38137
   397
$(OUT)/HOL-Library: $(OUT)/HOL Library/ROOT.ML				\
haftmann@37691
   398
  $(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML			\
haftmann@37818
   399
  Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy		\
wenzelm@38137
   400
  Library/AssocList.thy Library/BigO.thy Library/Binomial.thy		\
haftmann@37968
   401
  Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy	\
haftmann@37662
   402
  Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy	\
wenzelm@38137
   403
  Library/Code_Integer.thy Library/Code_Natural.thy			\
bulwahn@38119
   404
  Library/Code_Prolog.thy Tools/Predicate_Compile/code_prolog.ML	\
haftmann@37968
   405
  Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy	\
wenzelm@38137
   406
  Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy	\
haftmann@37968
   407
  Library/Efficient_Nat.thy Library/Enum.thy Library/Eval_Witness.thy	\
haftmann@37968
   408
  Library/Executable_Set.thy Library/Float.thy				\
haftmann@37968
   409
  Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
haftmann@37968
   410
  Library/FrechetDeriv.thy Library/Fset.thy Library/FuncSet.thy		\
haftmann@38622
   411
  Library/Function_Algebras.thy						\
haftmann@37968
   412
  Library/Fundamental_Theorem_Algebra.thy Library/Glbs.thy		\
haftmann@37968
   413
  Library/Indicator_Function.thy Library/Infinite_Set.thy		\
haftmann@37968
   414
  Library/Inner_Product.thy Library/Kleene_Algebra.thy			\
wenzelm@37118
   415
  Library/LaTeXsugar.thy Library/Lattice_Algebras.thy			\
wenzelm@37118
   416
  Library/Lattice_Syntax.thy Library/Library.thy			\
wenzelm@37118
   417
  Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy	\
krauss@37790
   418
  Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy	\
haftmann@37818
   419
  Library/Multiset.thy Library/Nat_Bijection.thy			\
wenzelm@38137
   420
  Library/Nat_Infinity.thy Library/Nested_Environment.thy		\
wenzelm@38137
   421
  Library/Numeral_Type.thy Library/OptionalSugar.thy			\
wenzelm@38137
   422
  Library/Order_Relation.thy Library/Permutation.thy			\
wenzelm@38137
   423
  Library/Permutations.thy Library/Poly_Deriv.thy			\
wenzelm@38137
   424
  Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy	\
wenzelm@38137
   425
  Library/Preorder.thy Library/Product_Vector.thy			\
wenzelm@38137
   426
  Library/Product_ord.thy Library/Product_plus.thy			\
wenzelm@38137
   427
  Library/Quickcheck_Types.thy Library/Quicksort.thy			\
wenzelm@37118
   428
  Library/Quotient_List.thy Library/Quotient_Option.thy			\
wenzelm@37118
   429
  Library/Quotient_Product.thy Library/Quotient_Sum.thy			\
wenzelm@37118
   430
  Library/Quotient_Syntax.thy Library/Quotient_Type.thy			\
wenzelm@37118
   431
  Library/RBT.thy Library/RBT_Impl.thy Library/README.html		\
haftmann@38622
   432
  Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy	\
haftmann@38622
   433
  Library/Reflection.thy Library/SML_Quickcheck.thy 			\
wenzelm@37118
   434
  Library/Sublist_Order.thy Library/Sum_Of_Squares.thy			\
wenzelm@37118
   435
  Library/Sum_Of_Squares/sos_wrapper.ML					\
wenzelm@37118
   436
  Library/Sum_Of_Squares/sum_of_squares.ML				\
wenzelm@37118
   437
  Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy		\
wenzelm@37118
   438
  Library/While_Combinator.thy Library/Zorn.thy				\
haftmann@37818
   439
  $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML	\
krauss@37789
   440
  Library/reflection.ML Library/reify_data.ML				\
haftmann@37691
   441
  Library/document/root.bib Library/document/root.tex
wenzelm@38137
   442
	@cd Library; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL-Library
wenzelm@10255
   443
wenzelm@10255
   444
wenzelm@31795
   445
## HOL-Hahn_Banach
haftmann@27421
   446
wenzelm@31795
   447
HOL-Hahn_Banach: HOL $(LOG)/HOL-Hahn_Banach.gz
haftmann@27421
   448
wenzelm@31795
   449
$(LOG)/HOL-Hahn_Banach.gz: $(OUT)/HOL Hahn_Banach/Bounds.thy		\
wenzelm@31795
   450
  Hahn_Banach/Function_Norm.thy Hahn_Banach/Function_Order.thy		\
wenzelm@31795
   451
  Hahn_Banach/Hahn_Banach.thy Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	\
wenzelm@31795
   452
  Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Hahn_Banach/Linearform.thy	\
wenzelm@31795
   453
  Hahn_Banach/Normed_Space.thy Hahn_Banach/README.html			\
wenzelm@31795
   454
  Hahn_Banach/ROOT.ML Hahn_Banach/Subspace.thy				\
wenzelm@31795
   455
  Hahn_Banach/Vector_Space.thy Hahn_Banach/Zorn_Lemma.thy		\
wenzelm@31795
   456
  Hahn_Banach/document/root.bib Hahn_Banach/document/root.tex
wenzelm@31795
   457
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hahn_Banach
haftmann@27421
   458
haftmann@27421
   459
wenzelm@4518
   460
## HOL-Subst
wenzelm@4518
   461
wenzelm@4518
   462
HOL-Subst: HOL $(LOG)/HOL-Subst.gz
wenzelm@4518
   463
wenzelm@27164
   464
$(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.thy Subst/ROOT.ML		\
wenzelm@27164
   465
  Subst/Subst.thy Subst/UTerm.thy Subst/Unifier.thy Subst/Unify.thy
wenzelm@28500
   466
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Subst
wenzelm@2448
   467
wenzelm@2448
   468
wenzelm@4518
   469
## HOL-Induct
wenzelm@2473
   470
wenzelm@4518
   471
HOL-Induct: HOL $(LOG)/HOL-Induct.gz
paulson@3125
   472
wenzelm@33688
   473
$(LOG)/HOL-Induct.gz: $(OUT)/HOL Induct/Com.thy Induct/Comb.thy		\
wenzelm@33688
   474
  Induct/Ordinals.thy Induct/PropLog.thy Induct/QuoNestedDataType.thy	\
wenzelm@33688
   475
  Induct/QuoDataType.thy Induct/ROOT.ML Induct/Sexp.thy			\
wenzelm@35249
   476
  Induct/Sigma_Algebra.thy Induct/ABexp.thy Induct/SList.thy		\
wenzelm@35249
   477
  Induct/Term.thy Induct/Tree.thy Induct/document/root.tex
wenzelm@28500
   478
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Induct
paulson@3125
   479
paulson@3125
   480
wenzelm@4518
   481
## HOL-IMP
wenzelm@4518
   482
wenzelm@4518
   483
HOL-IMP: HOL $(LOG)/HOL-IMP.gz
wenzelm@2448
   484
wenzelm@27164
   485
$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Compiler0.thy		\
wenzelm@27164
   486
  IMP/Compiler.thy IMP/Denotation.thy IMP/Expr.thy IMP/Hoare.thy	\
wenzelm@27164
   487
  IMP/Natural.thy IMP/Examples.thy IMP/Transition.thy IMP/VC.thy	\
wenzelm@27164
   488
  IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib
wenzelm@28500
   489
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL IMP
wenzelm@2448
   490
wenzelm@2448
   491
oheimb@8179
   492
## HOL-IMPP
oheimb@8179
   493
oheimb@8179
   494
HOL-IMPP: HOL $(LOG)/HOL-IMPP.gz
oheimb@8179
   495
wenzelm@27164
   496
$(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy		\
wenzelm@19803
   497
  IMPP/Natural.thy IMPP/Hoare.thy IMPP/Misc.thy IMPP/EvenOdd.thy
wenzelm@28500
   498
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL IMPP
oheimb@8179
   499
oheimb@8179
   500
haftmann@27421
   501
## HOL-Import
skalberg@14516
   502
wenzelm@19097
   503
IMPORTER_FILES = Import/lazy_seq.ML Import/proof_kernel.ML Import/replay.ML \
wenzelm@20610
   504
  Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \
skalberg@14516
   505
  Import/HOL4Syntax.thy Import/HOL4Compat.thy Import/import_syntax.ML \
haftmann@31723
   506
  Import/hol4rews.ML Import/import.ML Import/ROOT.ML
skalberg@14516
   507
obua@17323
   508
IMPORTER_HOLLIGHT_FILES = Import/proof_kernel.ML Import/replay.ML \
obua@17323
   509
  Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \
obua@17323
   510
  Import/HOL4Syntax.thy Import/HOLLightCompat.thy Import/import_syntax.ML \
haftmann@31771
   511
  Import/hol4rews.ML Import/import.ML Import/ROOT.ML
obua@17323
   512
haftmann@27421
   513
HOL-Import: HOL $(LOG)/HOL-Import.gz
skalberg@14516
   514
haftmann@27421
   515
$(LOG)/HOL-Import.gz: $(OUT)/HOL $(IMPORTER_FILES)
wenzelm@37296
   516
	@$(ISABELLE_TOOL) usedir -p 0 $(OUT)/HOL Import
skalberg@14516
   517
skalberg@14516
   518
haftmann@27421
   519
## HOL-Generate-HOL
skalberg@14516
   520
haftmann@27421
   521
HOL-Generate-HOL: HOL $(LOG)/HOL-Generate-HOL.gz
skalberg@14516
   522
haftmann@27421
   523
$(LOG)/HOL-Generate-HOL.gz: $(OUT)/HOL			\
wenzelm@27164
   524
  $(IMPORTER_FILES) Import/Generate-HOL/GenHOL4Base.thy			\
wenzelm@27164
   525
  Import/Generate-HOL/GenHOL4Prob.thy					\
wenzelm@27164
   526
  Import/Generate-HOL/GenHOL4Real.thy					\
wenzelm@27164
   527
  Import/Generate-HOL/GenHOL4Vec.thy					\
skalberg@14516
   528
  Import/Generate-HOL/GenHOL4Word32.thy Import/Generate-HOL/ROOT.ML
wenzelm@28500
   529
	@cd Import; $(ISABELLE_TOOL) usedir $(OUT)/HOL Generate-HOL
skalberg@14516
   530
wenzelm@17460
   531
haftmann@27421
   532
## HOL-Generate-HOLLight
wenzelm@17460
   533
haftmann@27421
   534
HOL-Generate-HOLLight: HOL $(LOG)/HOL-Generate-HOLLight.gz
obua@17323
   535
haftmann@37742
   536
$(LOG)/HOL-Generate-HOLLight.gz: $(OUT)/HOL				\
wenzelm@27164
   537
  $(IMPORTER_HOLLIGHT_FILES) Import/Generate-HOLLight/GenHOLLight.thy	\
wenzelm@27164
   538
  Import/Generate-HOLLight/ROOT.ML
wenzelm@28500
   539
	@cd Import; $(ISABELLE_TOOL) usedir $(OUT)/HOL Generate-HOLLight
skalberg@14516
   540
wenzelm@17460
   541
skalberg@14516
   542
## HOL-Import-HOL
skalberg@14516
   543
haftmann@27421
   544
HOL4: HOL $(LOG)/HOL4.gz
skalberg@14516
   545
skalberg@14516
   546
HOL_IMPORT_FILES = arithmetic.imp bits.imp boolean_sequence.imp bool.imp \
skalberg@14516
   547
  bword_arith.imp bword_bitop.imp bword_num.imp combin.imp divides.imp \
skalberg@14516
   548
  hrat.imp hreal.imp ind_type.imp lim.imp list.imp marker.imp nets.imp \
skalberg@14516
   549
  numeral.imp num.imp one.imp operator.imp option.imp pair.imp poly.imp \
skalberg@14516
   550
  powser.imp pred_set.imp prime.imp prim_rec.imp prob_algebra.imp \
skalberg@14516
   551
  prob_canon.imp prob_extra.imp prob.imp prob_indep.imp prob_pseudo.imp \
webertj@23194
   552
  prob_uniform.imp realax.imp real.imp relation.imp res_quan.imp \
webertj@23194
   553
  rich_list.imp \
skalberg@14516
   554
  seq.imp state_transformer.imp sum.imp topology.imp transc.imp word32.imp \
skalberg@14516
   555
  word_base.imp word_bitop.imp word_num.imp
skalberg@14516
   556
haftmann@37742
   557
$(LOG)/HOL4.gz: $(OUT)/HOL $(IMPORTER_FILES)				\
wenzelm@27164
   558
  $(HOL_IMPORT_FILES:%=Import/HOL/%) Import/HOL/HOL4Base.thy		\
wenzelm@27164
   559
  Import/HOL/HOL4Prob.thy Import/HOL/HOL4Real.thy			\
wenzelm@27164
   560
  Import/HOL/HOL4Vec.thy Import/HOL/HOL4Word32.thy Import/HOL/HOL4.thy	\
wenzelm@27164
   561
  Import/HOL/ROOT.ML
wenzelm@28500
   562
	@cd Import/HOL; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL4
skalberg@14516
   563
haftmann@27421
   564
HOLLight: HOL $(LOG)/HOLLight.gz
obua@17645
   565
haftmann@37742
   566
$(LOG)/HOLLight.gz: $(OUT)/HOL $(IMPORTER_HOLLIGHT_FILES)		\
wenzelm@27164
   567
  Import/HOLLight/hollight.imp Import/HOLLight/HOLLight.thy		\
obua@17645
   568
  Import/HOLLight/ROOT.ML
wenzelm@28500
   569
	@cd Import/HOLLight; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOLLight
obua@17645
   570
skalberg@14516
   571
haftmann@32479
   572
## HOL-Number_Theory
nipkow@31719
   573
haftmann@32479
   574
HOL-Number_Theory: HOL $(LOG)/HOL-Number_Theory.gz
nipkow@31719
   575
haftmann@32479
   576
$(LOG)/HOL-Number_Theory.gz: $(OUT)/HOL $(ALGEBRA_DEPENDENCIES) \
haftmann@31771
   577
  Library/Multiset.thy \
haftmann@32479
   578
  Number_Theory/Binomial.thy \
haftmann@32479
   579
  Number_Theory/Cong.thy \
haftmann@32479
   580
  Number_Theory/Fib.thy \
haftmann@32479
   581
  Number_Theory/MiscAlgebra.thy \
haftmann@32479
   582
  Number_Theory/Number_Theory.thy \
haftmann@32479
   583
  Number_Theory/Residues.thy \
haftmann@32479
   584
  Number_Theory/UniqueFactorization.thy  \
haftmann@32479
   585
  Number_Theory/ROOT.ML
haftmann@32479
   586
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Number_Theory
nipkow@31719
   587
nipkow@31719
   588
haftmann@32479
   589
## HOL-Old_Number_Theory
paulson@9510
   590
haftmann@32479
   591
HOL-Old_Number_Theory: HOL $(LOG)/HOL-Old_Number_Theory.gz
paulson@9510
   592
haftmann@37021
   593
$(LOG)/HOL-Old_Number_Theory.gz: $(OUT)/HOL Library/Permutation.thy	\
haftmann@37021
   594
  Old_Number_Theory/Primes.thy Old_Number_Theory/Fib.thy		\
haftmann@37021
   595
  Old_Number_Theory/Factorization.thy Old_Number_Theory/BijectionRel.thy\
haftmann@37021
   596
  Old_Number_Theory/Chinese.thy Old_Number_Theory/EulerFermat.thy	\
haftmann@37021
   597
  Old_Number_Theory/IntFact.thy Old_Number_Theory/IntPrimes.thy		\
haftmann@37021
   598
  Old_Number_Theory/WilsonBij.thy Old_Number_Theory/WilsonRuss.thy	\
haftmann@37021
   599
  Old_Number_Theory/Finite2.thy Old_Number_Theory/Int2.thy		\
haftmann@37021
   600
  Old_Number_Theory/EvenOdd.thy Old_Number_Theory/Residues.thy		\
haftmann@37021
   601
  Old_Number_Theory/Euler.thy Old_Number_Theory/Gauss.thy		\
haftmann@32479
   602
  Old_Number_Theory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy	\
haftmann@37021
   603
  Old_Number_Theory/Legacy_GCD.thy Old_Number_Theory/Pocklington.thy	\
haftmann@37021
   604
  Old_Number_Theory/ROOT.ML
haftmann@32479
   605
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Old_Number_Theory
paulson@9510
   606
paulson@9510
   607
wenzelm@4518
   608
## HOL-Hoare
wenzelm@4518
   609
wenzelm@4518
   610
HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz
wenzelm@2448
   611
wenzelm@27164
   612
$(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.thy Hoare/Examples.thy	\
wenzelm@27164
   613
  Hoare/Hoare.thy Hoare/hoare_tac.ML Hoare/Heap.thy			\
haftmann@35319
   614
  Hoare/Hoare_Logic.thy	Hoare/Hoare_Logic_Abort.thy			\
wenzelm@27164
   615
  Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy Hoare/ROOT.ML		\
wenzelm@27164
   616
  Hoare/ExamplesAbort.thy Hoare/HeapSyntaxAbort.thy			\
haftmann@35319
   617
  Hoare/SchorrWaite.thy Hoare/Separation.thy				\
wenzelm@27164
   618
  Hoare/SepLogHeap.thy Hoare/document/root.tex Hoare/document/root.bib
wenzelm@28500
   619
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Hoare
wenzelm@2448
   620
wenzelm@2448
   621
haftmann@32621
   622
## HOL-Hoare_Parallel
prensani@12996
   623
haftmann@32621
   624
HOL-Hoare_Parallel: HOL $(LOG)/HOL-Hoare_Parallel.gz
prensani@12996
   625
haftmann@32621
   626
$(LOG)/HOL-Hoare_Parallel.gz: $(OUT)/HOL Hoare_Parallel/Gar_Coll.thy	\
wenzelm@33439
   627
  Hoare_Parallel/Graph.thy Hoare_Parallel/Hoare_Parallel.thy		\
wenzelm@33439
   628
  Hoare_Parallel/Mul_Gar_Coll.thy Hoare_Parallel/OG_Com.thy		\
wenzelm@33439
   629
  Hoare_Parallel/OG_Examples.thy Hoare_Parallel/OG_Hoare.thy		\
wenzelm@33439
   630
  Hoare_Parallel/OG_Syntax.thy Hoare_Parallel/OG_Tactics.thy		\
wenzelm@33439
   631
  Hoare_Parallel/OG_Tran.thy Hoare_Parallel/Quote_Antiquote.thy		\
wenzelm@33439
   632
  Hoare_Parallel/RG_Com.thy Hoare_Parallel/RG_Examples.thy		\
wenzelm@33439
   633
  Hoare_Parallel/RG_Hoare.thy Hoare_Parallel/RG_Syntax.thy		\
wenzelm@33439
   634
  Hoare_Parallel/RG_Tran.thy Hoare_Parallel/ROOT.ML			\
wenzelm@33439
   635
  Hoare_Parallel/document/root.tex Hoare_Parallel/document/root.bib
haftmann@32621
   636
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hoare_Parallel
prensani@12996
   637
prensani@12996
   638
haftmann@37747
   639
## HOL-Library-Codegenerator_Test
haftmann@37691
   640
haftmann@37747
   641
HOL-Library-Codegenerator_Test: HOL-Library $(LOG)/HOL-Library-Codegenerator_Test.gz
haftmann@37691
   642
haftmann@37747
   643
$(LOG)/HOL-Library-Codegenerator_Test.gz: $(OUT)/HOL-Library		\
haftmann@37742
   644
  Codegenerator_Test/ROOT.ML 						\
haftmann@37742
   645
  Codegenerator_Test/Candidates.thy					\
haftmann@37691
   646
  Codegenerator_Test/Candidates_Pretty.thy				\
haftmann@37691
   647
  Codegenerator_Test/Generate.thy					\
haftmann@37691
   648
  Codegenerator_Test/Generate_Pretty.thy
haftmann@37691
   649
	@$(ISABELLE_TOOL) usedir -d false -g false -i false $(OUT)/HOL-Library Codegenerator_Test
haftmann@37691
   650
haftmann@37691
   651
wenzelm@33027
   652
## HOL-Metis_Examples
paulson@23449
   653
wenzelm@33027
   654
HOL-Metis_Examples: HOL $(LOG)/HOL-Metis_Examples.gz
paulson@23449
   655
haftmann@37742
   656
$(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML		\
haftmann@37742
   657
  Metis_Examples/Abstraction.thy Metis_Examples/BigO.thy		\
haftmann@37742
   658
  Metis_Examples/BT.thy Metis_Examples/Message.thy			\
haftmann@37742
   659
  Metis_Examples/Tarski.thy Metis_Examples/TransClosure.thy		\
wenzelm@33027
   660
  Metis_Examples/set.thy
wenzelm@33027
   661
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples
paulson@23449
   662
paulson@23449
   663
blanchet@33197
   664
## HOL-Nitpick_Examples
blanchet@33197
   665
blanchet@33197
   666
HOL-Nitpick_Examples: HOL $(LOG)/HOL-Nitpick_Examples.gz
blanchet@33197
   667
blanchet@34126
   668
$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \
blanchet@34126
   669
  Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \
blanchet@35076
   670
  Nitpick_Examples/Hotel_Nits.thy Nitpick_Examples/Induct_Nits.thy \
blanchet@35076
   671
  Nitpick_Examples/Integer_Nits.thy Nitpick_Examples/Manual_Nits.thy \
blanchet@35076
   672
  Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy \
blanchet@35076
   673
  Nitpick_Examples/Nitpick_Examples.thy Nitpick_Examples/Pattern_Nits.thy \
blanchet@35076
   674
  Nitpick_Examples/Record_Nits.thy Nitpick_Examples/Refute_Nits.thy \
blanchet@35076
   675
  Nitpick_Examples/Special_Nits.thy Nitpick_Examples/Tests_Nits.thy \
blanchet@35076
   676
  Nitpick_Examples/Typedef_Nits.thy
blanchet@33197
   677
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples
blanchet@33197
   678
blanchet@33197
   679
paulson@7999
   680
## HOL-Algebra
paulson@7999
   681
wenzelm@33439
   682
HOL-Algebra: HOL $(OUT)/HOL-Algebra
paulson@7999
   683
haftmann@31771
   684
ALGEBRA_DEPENDENCIES = $(OUT)/HOL \
haftmann@31771
   685
  Algebra/ROOT.ML \
haftmann@31771
   686
  Library/Binomial.thy \
haftmann@31771
   687
  Library/FuncSet.thy \
haftmann@31771
   688
  Library/Multiset.thy \
haftmann@31771
   689
  Library/Permutation.thy \
haftmann@32479
   690
  Number_Theory/Primes.thy \
haftmann@31771
   691
  Algebra/AbelCoset.thy \
haftmann@31771
   692
  Algebra/Bij.thy \
haftmann@31771
   693
  Algebra/Congruence.thy \
haftmann@31771
   694
  Algebra/Coset.thy \
haftmann@31771
   695
  Algebra/Divisibility.thy \
haftmann@31771
   696
  Algebra/Exponent.thy \
haftmann@31771
   697
  Algebra/FiniteProduct.thy \
haftmann@31771
   698
  Algebra/Group.thy \
haftmann@31771
   699
  Algebra/Ideal.thy \
haftmann@31771
   700
  Algebra/IntRing.thy \
haftmann@31771
   701
  Algebra/Lattice.thy \
haftmann@31771
   702
  Algebra/Module.thy \
haftmann@31771
   703
  Algebra/QuotRing.thy \
haftmann@31771
   704
  Algebra/Ring.thy \
haftmann@31771
   705
  Algebra/RingHom.thy \
haftmann@31771
   706
  Algebra/Sylow.thy \
haftmann@31771
   707
  Algebra/UnivPoly.thy \
haftmann@31771
   708
  Algebra/abstract/Abstract.thy \
haftmann@31771
   709
  Algebra/abstract/Factor.thy \
haftmann@31771
   710
  Algebra/abstract/Field.thy \
haftmann@31771
   711
  Algebra/abstract/Ideal2.thy \
haftmann@31771
   712
  Algebra/abstract/PID.thy \
haftmann@31771
   713
  Algebra/abstract/Ring2.thy \
haftmann@31771
   714
  Algebra/abstract/RingHomo.thy \
haftmann@31771
   715
  Algebra/document/root.tex \
haftmann@31771
   716
  Algebra/document/root.tex \
haftmann@31771
   717
  Algebra/poly/LongDiv.thy \
haftmann@31771
   718
  Algebra/poly/PolyHomo.thy \
haftmann@31771
   719
  Algebra/poly/Polynomial.thy \
haftmann@31771
   720
  Algebra/poly/UnivPoly2.thy \
haftmann@31771
   721
  Algebra/ringsimp.ML
haftmann@31771
   722
wenzelm@33448
   723
$(OUT)/HOL-Algebra: $(ALGEBRA_DEPENDENCIES)
wenzelm@28500
   724
	@cd Algebra; $(ISABELLE_TOOL) usedir -b -g true -V outline=/proof,/ML $(OUT)/HOL HOL-Algebra
paulson@7999
   725
wenzelm@27477
   726
wenzelm@4518
   727
## HOL-Auth
wenzelm@3819
   728
wenzelm@4518
   729
HOL-Auth: HOL $(LOG)/HOL-Auth.gz
wenzelm@3819
   730
nipkow@28098
   731
$(LOG)/HOL-Auth.gz: $(OUT)/HOL 						\
haftmann@37021
   732
  Auth/Auth_Shared.thy Auth/Auth_Public.thy Auth/All_Symmetric.thy	\
haftmann@37021
   733
  Auth/Guard/Auth_Guard_Shared.thy					\
haftmann@37021
   734
  Auth/Guard/Auth_Guard_Public.thy					\
haftmann@32632
   735
  Auth/Smartcard/Auth_Smartcard.thy Auth/All_Symmetric.thy		\
wenzelm@27164
   736
  Auth/CertifiedEmail.thy Auth/Event.thy Auth/Message.thy		\
wenzelm@27164
   737
  Auth/NS_Public.thy Auth/NS_Public_Bad.thy Auth/NS_Shared.thy		\
wenzelm@27164
   738
  Auth/OtwayRees.thy Auth/OtwayReesBella.thy Auth/OtwayRees_AN.thy	\
wenzelm@27164
   739
  Auth/OtwayRees_Bad.thy Auth/Public.thy Auth/ROOT.ML Auth/Recur.thy	\
wenzelm@27164
   740
  Auth/Shared.thy Auth/TLS.thy Auth/WooLam.thy Auth/Kerberos_BAN.thy	\
wenzelm@27164
   741
  Auth/Kerberos_BAN_Gets.thy Auth/KerberosIV.thy			\
wenzelm@27164
   742
  Auth/KerberosIV_Gets.thy Auth/KerberosV.thy Auth/Yahalom.thy		\
wenzelm@27164
   743
  Auth/Yahalom2.thy Auth/Yahalom_Bad.thy Auth/ZhouGollmann.thy		\
wenzelm@27164
   744
  Auth/Guard/Analz.thy Auth/Guard/Extensions.thy Auth/Guard/GuardK.thy	\
wenzelm@27164
   745
  Auth/Guard/Guard_Public.thy Auth/Guard/Guard_Shared.thy		\
wenzelm@27164
   746
  Auth/Guard/Guard.thy Auth/Guard/List_Msg.thy				\
wenzelm@27164
   747
  Auth/Guard/Guard_NS_Public.thy Auth/Guard/Guard_OtwayRees.thy		\
wenzelm@27164
   748
  Auth/Guard/P1.thy Auth/Guard/P2.thy Auth/Guard/Proto.thy		\
wenzelm@27164
   749
  Auth/Guard/Guard_Yahalom.thy Auth/Smartcard/EventSC.thy		\
wenzelm@27164
   750
  Auth/Smartcard/ShoupRubinBella.thy Auth/Smartcard/ShoupRubin.thy	\
wenzelm@27164
   751
  Auth/Smartcard/Smartcard.thy Auth/document/root.tex
wenzelm@28500
   752
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Auth
wenzelm@2448
   753
wenzelm@2448
   754
paulson@4777
   755
## HOL-UNITY
paulson@4777
   756
paulson@4777
   757
HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz
paulson@4777
   758
wenzelm@27164
   759
$(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML	\
wenzelm@33439
   760
  UNITY/UNITY_Main.thy UNITY/UNITY_Examples.thy UNITY/UNITY_tactics.ML	\
wenzelm@33439
   761
  UNITY/Comp.thy UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy	\
wenzelm@27164
   762
  UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy UNITY/Guar.thy	\
wenzelm@27164
   763
  UNITY/Lift_prog.thy UNITY/ListOrder.thy UNITY/ProgressSets.thy	\
wenzelm@27164
   764
  UNITY/PPROD.thy UNITY/Project.thy UNITY/Rename.thy			\
wenzelm@27164
   765
  UNITY/Transformers.thy UNITY/SubstAx.thy UNITY/UNITY.thy		\
wenzelm@27164
   766
  UNITY/Union.thy UNITY/WFair.thy UNITY/Simple/Channel.thy		\
wenzelm@27164
   767
  UNITY/Simple/Common.thy UNITY/Simple/Deadlock.thy			\
wenzelm@27164
   768
  UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy				\
wenzelm@27164
   769
  UNITY/Simple/NSP_Bad.thy UNITY/Simple/Network.thy			\
wenzelm@27164
   770
  UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy			\
wenzelm@27164
   771
  UNITY/Simple/Token.thy UNITY/Comp/Alloc.thy UNITY/Comp/AllocBase.thy	\
wenzelm@27164
   772
  UNITY/Comp/AllocImpl.thy UNITY/Comp/Client.thy			\
wenzelm@27164
   773
  UNITY/Comp/Counter.thy UNITY/Comp/Counterc.thy			\
wenzelm@27164
   774
  UNITY/Comp/Handshake.thy UNITY/Comp/PriorityAux.thy			\
wenzelm@27164
   775
  UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy			\
wenzelm@27164
   776
  UNITY/Comp/TimerArray.thy UNITY/document/root.tex
wenzelm@28500
   777
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL UNITY
paulson@4777
   778
paulson@4777
   779
wenzelm@10966
   780
## HOL-Unix
wenzelm@10966
   781
wenzelm@10966
   782
HOL-Unix: HOL $(LOG)/HOL-Unix.gz
wenzelm@10966
   783
haftmann@37742
   784
$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy		\
haftmann@37742
   785
  Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy			\
wenzelm@10966
   786
  Unix/document/root.bib Unix/document/root.tex
wenzelm@28500
   787
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Unix
wenzelm@10966
   788
wenzelm@27477
   789
obua@19203
   790
## HOL-ZF
obua@19203
   791
obua@19203
   792
HOL-ZF: HOL $(LOG)/HOL-ZF.gz
obua@19203
   793
krauss@35502
   794
$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/LProd.thy	\
wenzelm@27164
   795
  ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex
wenzelm@28500
   796
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF
wenzelm@10966
   797
wenzelm@27477
   798
haftmann@29399
   799
## HOL-Imperative_HOL
haftmann@29399
   800
haftmann@29399
   801
HOL-Imperative_HOL: HOL $(LOG)/HOL-Imperative_HOL.gz
haftmann@29399
   802
haftmann@37772
   803
$(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL Imperative_HOL/Array.thy	\
haftmann@37772
   804
  Imperative_HOL/Heap.thy Imperative_HOL/Heap_Monad.thy			\
haftmann@37772
   805
  Imperative_HOL/Imperative_HOL.thy Imperative_HOL/Imperative_HOL_ex.thy\
haftmann@37776
   806
  Imperative_HOL/Mrec.thy Imperative_HOL/Ref.thy			\
haftmann@37772
   807
  Imperative_HOL/ex/Imperative_Quicksort.thy				\
haftmann@37772
   808
  Imperative_HOL/ex/Imperative_Reverse.thy				\
haftmann@37772
   809
  Imperative_HOL/ex/Linked_Lists.thy					\
haftmann@37772
   810
  Imperative_HOL/ex/SatChecker.thy					\
haftmann@37772
   811
  Imperative_HOL/ex/Sorted_List.thy					\
haftmann@37772
   812
  Imperative_HOL/ex/Subarray.thy					\
haftmann@30689
   813
  Imperative_HOL/ex/Sublist.thy
haftmann@29399
   814
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Imperative_HOL
haftmann@29399
   815
haftmann@29399
   816
haftmann@29823
   817
## HOL-Decision_Procs
haftmann@29823
   818
haftmann@29823
   819
HOL-Decision_Procs: HOL $(LOG)/HOL-Decision_Procs.gz
haftmann@29823
   820
haftmann@29823
   821
$(LOG)/HOL-Decision_Procs.gz: $(OUT)/HOL \
haftmann@29823
   822
  Decision_Procs/Approximation.thy \
haftmann@33356
   823
  Decision_Procs/Commutative_Ring.thy \
haftmann@33356
   824
  Decision_Procs/Commutative_Ring_Complete.thy \
haftmann@29823
   825
  Decision_Procs/Cooper.thy \
wenzelm@35053
   826
  Decision_Procs/Decision_Procs.thy \
haftmann@29823
   827
  Decision_Procs/Dense_Linear_Order.thy \
haftmann@29823
   828
  Decision_Procs/Ferrack.thy \
haftmann@29823
   829
  Decision_Procs/MIR.thy \
wenzelm@35053
   830
  Decision_Procs/Parametric_Ferrante_Rackoff.thy \
wenzelm@35053
   831
  Decision_Procs/Polynomial_List.thy \
wenzelm@37120
   832
  Decision_Procs/ROOT.ML \
wenzelm@35053
   833
  Decision_Procs/Reflected_Multivariate_Polynomial.thy \
wenzelm@35053
   834
  Decision_Procs/commutative_ring_tac.ML \
wenzelm@35053
   835
  Decision_Procs/cooper_tac.ML \
haftmann@30429
   836
  Decision_Procs/ex/Approximation_Ex.thy \
haftmann@33356
   837
  Decision_Procs/ex/Commutative_Ring_Ex.thy \
wenzelm@35053
   838
  Decision_Procs/ex/Dense_Linear_Order_Ex.thy \
wenzelm@35053
   839
  Decision_Procs/ferrack_tac.ML \
wenzelm@37120
   840
  Decision_Procs/ferrante_rackoff.ML \
wenzelm@37120
   841
  Decision_Procs/ferrante_rackoff_data.ML \
wenzelm@37120
   842
  Decision_Procs/langford.ML \
wenzelm@37120
   843
  Decision_Procs/langford_data.ML \
wenzelm@37120
   844
  Decision_Procs/mir_tac.ML
haftmann@29823
   845
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Decision_Procs
haftmann@29823
   846
haftmann@29823
   847
wenzelm@30400
   848
## HOL-Docs
wenzelm@30400
   849
wenzelm@30400
   850
HOL-Docs: HOL $(LOG)/HOL-Docs.gz
wenzelm@30400
   851
haftmann@37742
   852
$(LOG)/HOL-Docs.gz: $(OUT)/HOL Docs/Main_Doc.thy Docs/ROOT.ML		\
wenzelm@30400
   853
  Docs/document/root.tex
nipkow@30440
   854
	@$(ISABELLE_TOOL) usedir -D generated $(OUT)/HOL Docs
wenzelm@30400
   855
wenzelm@30400
   856
wenzelm@34205
   857
## HOL-Proofs-Lambda
wenzelm@2448
   858
wenzelm@34205
   859
HOL-Proofs-Lambda: HOL-Proofs $(LOG)/HOL-Proofs-Lambda.gz
wenzelm@2448
   860
wenzelm@34205
   861
$(LOG)/HOL-Proofs-Lambda.gz: $(OUT)/HOL-Proofs Lambda/Commutation.thy	\
wenzelm@34205
   862
  Lambda/Eta.thy Lambda/InductTermi.thy Lambda/Lambda.thy		\
wenzelm@34205
   863
  Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy	\
wenzelm@34205
   864
  Lambda/NormalForm.thy Lambda/ParRed.thy Lambda/Standardization.thy	\
wenzelm@34205
   865
  Lambda/StrongNorm.thy Lambda/Type.thy Lambda/WeakNorm.thy		\
wenzelm@34205
   866
  Lambda/ROOT.ML Lambda/document/root.bib Lambda/document/root.tex
wenzelm@37296
   867
	@$(ISABELLE_TOOL) usedir -g true -m no_brackets -p 2 -q 0 $(OUT)/HOL-Proofs Lambda
wenzelm@2448
   868
wenzelm@2448
   869
oheimb@9015
   870
## HOL-Prolog
oheimb@9015
   871
oheimb@9015
   872
HOL-Prolog: HOL $(LOG)/HOL-Prolog.gz
oheimb@9015
   873
wenzelm@27164
   874
$(LOG)/HOL-Prolog.gz: $(OUT)/HOL Prolog/ROOT.ML Prolog/prolog.ML	\
wenzelm@27164
   875
  Prolog/HOHH.thy Prolog/Test.thy Prolog/Func.thy Prolog/Type.thy
wenzelm@28500
   876
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Prolog
oheimb@9015
   877
oheimb@9015
   878
nipkow@8012
   879
## HOL-MicroJava
nipkow@8012
   880
nipkow@8012
   881
HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
nipkow@8012
   882
wenzelm@27164
   883
$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL Library/Executable_Set.thy		\
wenzelm@27164
   884
  MicroJava/ROOT.ML MicroJava/Comp/AuxLemmas.thy			\
wenzelm@27164
   885
  MicroJava/Comp/CorrComp.thy MicroJava/Comp/CorrCompTp.thy		\
wenzelm@27164
   886
  MicroJava/Comp/DefsComp.thy MicroJava/Comp/Index.thy			\
wenzelm@27164
   887
  MicroJava/Comp/LemmasComp.thy MicroJava/Comp/NatCanonify.thy		\
wenzelm@27164
   888
  MicroJava/Comp/TranslComp.thy MicroJava/Comp/TranslCompTp.thy		\
wenzelm@27164
   889
  MicroJava/Comp/TypeInf.thy MicroJava/J/Conform.thy			\
wenzelm@27164
   890
  MicroJava/J/Eval.thy MicroJava/J/JBasis.thy				\
wenzelm@27164
   891
  MicroJava/J/JTypeSafe.thy MicroJava/J/Decl.thy MicroJava/J/State.thy	\
wenzelm@27164
   892
  MicroJava/J/Term.thy MicroJava/J/Type.thy MicroJava/J/TypeRel.thy	\
wenzelm@27164
   893
  MicroJava/J/WellForm.thy MicroJava/J/Value.thy			\
wenzelm@27164
   894
  MicroJava/J/WellType.thy MicroJava/J/Example.thy			\
wenzelm@27164
   895
  MicroJava/J/JListExample.thy MicroJava/JVM/JVMExec.thy		\
wenzelm@27164
   896
  MicroJava/JVM/JVMInstructions.thy MicroJava/JVM/JVMState.thy		\
wenzelm@27164
   897
  MicroJava/JVM/JVMExecInstr.thy MicroJava/JVM/JVMListExample.thy	\
haftmann@33954
   898
  MicroJava/JVM/JVMExceptions.thy MicroJava/DFA/Abstract_BV.thy		\
haftmann@33954
   899
  MicroJava/DFA/Err.thy MicroJava/DFA/Kildall.thy			\
haftmann@33954
   900
  MicroJava/DFA/LBVComplete.thy MicroJava/DFA/LBVCorrect.thy		\
haftmann@33954
   901
  MicroJava/DFA/LBVSpec.thy MicroJava/DFA/Listn.thy			\
haftmann@33954
   902
  MicroJava/DFA/Opt.thy MicroJava/DFA/Product.thy			\
haftmann@33954
   903
  MicroJava/DFA/SemilatAlg.thy MicroJava/DFA/Semilat.thy		\
haftmann@33954
   904
  MicroJava/DFA/Semilattices.thy MicroJava/DFA/Typing_Framework_err.thy	\
haftmann@33954
   905
  MicroJava/DFA/Typing_Framework.thy MicroJava/BV/BVSpec.thy		\
wenzelm@27164
   906
  MicroJava/BV/BVSpecTypeSafe.thy MicroJava/BV/Correct.thy		\
haftmann@33954
   907
  MicroJava/BV/JType.thy MicroJava/BV/JVM.thy MicroJava/BV/JVMType.thy	\
wenzelm@27164
   908
  MicroJava/BV/Effect.thy MicroJava/BV/EffectMono.thy			\
wenzelm@27164
   909
  MicroJava/BV/Typing_Framework_JVM.thy MicroJava/BV/BVExample.thy	\
haftmann@33954
   910
  MicroJava/BV/LBVJVM.thy MicroJava/document/root.bib			\
haftmann@33954
   911
  MicroJava/document/root.tex MicroJava/document/introduction.tex
wenzelm@28500
   912
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL MicroJava
wenzelm@11850
   913
nipkow@8012
   914
oheimb@11376
   915
## HOL-NanoJava
oheimb@11376
   916
oheimb@11376
   917
HOL-NanoJava: HOL $(LOG)/HOL-NanoJava.gz
oheimb@11376
   918
wenzelm@27164
   919
$(LOG)/HOL-NanoJava.gz: $(OUT)/HOL NanoJava/ROOT.ML NanoJava/Term.thy	\
wenzelm@27164
   920
  NanoJava/Decl.thy NanoJava/TypeRel.thy NanoJava/State.thy		\
wenzelm@27164
   921
  NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy		\
oheimb@11376
   922
  NanoJava/document/root.bib NanoJava/document/root.tex
wenzelm@28500
   923
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NanoJava
wenzelm@11850
   924
wenzelm@8193
   925
schirmer@12855
   926
## HOL-Bali
schirmer@12855
   927
schirmer@12855
   928
HOL-Bali: HOL $(LOG)/HOL-Bali.gz
schirmer@12855
   929
wenzelm@33024
   930
$(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/Bali.thy Bali/AxCompl.thy		\
wenzelm@33024
   931
  Bali/AxExample.thy Bali/AxSem.thy Bali/AxSound.thy Bali/Basis.thy	\
wenzelm@33024
   932
  Bali/Conform.thy Bali/Decl.thy Bali/DeclConcepts.thy Bali/Eval.thy	\
wenzelm@33024
   933
  Bali/Evaln.thy Bali/Example.thy Bali/Name.thy Bali/ROOT.ML		\
wenzelm@33024
   934
  Bali/State.thy Bali/Table.thy Bali/Term.thy Bali/Trans.thy		\
wenzelm@33024
   935
  Bali/Type.thy Bali/TypeRel.thy Bali/TypeSafe.thy Bali/Value.thy	\
wenzelm@33024
   936
  Bali/WellForm.thy Bali/DefiniteAssignment.thy				\
wenzelm@33024
   937
  Bali/DefiniteAssignmentCorrect.thy Bali/WellType.thy			\
wenzelm@33024
   938
  Bali/document/root.tex
wenzelm@28500
   939
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Bali
schirmer@12855
   940
schirmer@12855
   941
wenzelm@34205
   942
## HOL-Proofs-Extraction
berghofe@13403
   943
wenzelm@34205
   944
HOL-Proofs-Extraction: HOL-Proofs $(LOG)/HOL-Proofs-Extraction.gz
berghofe@13403
   945
wenzelm@34205
   946
$(LOG)/HOL-Proofs-Extraction.gz: $(OUT)/HOL-Proofs			\
wenzelm@34205
   947
  Library/Efficient_Nat.thy Extraction/Euclid.thy			\
wenzelm@34205
   948
  Extraction/Greatest_Common_Divisor.thy Extraction/Higman.thy		\
wenzelm@34205
   949
  Extraction/Pigeonhole.thy Extraction/QuotRem.thy Extraction/ROOT.ML	\
wenzelm@34205
   950
  Extraction/Util.thy Extraction/Warshall.thy				\
wenzelm@34205
   951
  Extraction/document/root.tex Extraction/document/root.bib
wenzelm@37296
   952
	@$(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs Extraction
berghofe@13403
   953
berghofe@13403
   954
wenzelm@4518
   955
## HOL-IOA
wenzelm@4518
   956
wenzelm@4518
   957
HOL-IOA: HOL $(LOG)/HOL-IOA.gz
wenzelm@2448
   958
wenzelm@27164
   959
$(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.thy IOA/IOA.thy IOA/ROOT.ML	\
wenzelm@27164
   960
  IOA/Solve.thy
wenzelm@28500
   961
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL IOA
wenzelm@4518
   962
wenzelm@4518
   963
wenzelm@10157
   964
## HOL-Lattice
wenzelm@10157
   965
wenzelm@10157
   966
HOL-Lattice: HOL $(LOG)/HOL-Lattice.gz
wenzelm@10157
   967
wenzelm@27164
   968
$(LOG)/HOL-Lattice.gz: $(OUT)/HOL Lattice/Bounds.thy			\
wenzelm@27164
   969
  Lattice/CompleteLattice.thy Lattice/Lattice.thy Lattice/Orders.thy	\
wenzelm@10157
   970
  Lattice/ROOT.ML Lattice/document/root.tex
wenzelm@28500
   971
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Lattice
wenzelm@10157
   972
wenzelm@10157
   973
wenzelm@4518
   974
## HOL-ex
wenzelm@2448
   975
wenzelm@4518
   976
HOL-ex: HOL $(LOG)/HOL-ex.gz
wenzelm@2448
   977
wenzelm@33439
   978
$(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy	\
wenzelm@33024
   979
  Number_Theory/Primes.thy						\
wenzelm@33024
   980
  ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy		\
wenzelm@30179
   981
  ex/Arithmetic_Series_Complex.thy ex/BT.thy ex/BinEx.thy		\
wenzelm@30179
   982
  ex/Binary.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy		\
haftmann@37691
   983
  ex/CodegenSML_Test.thy ex/Coherent.thy ex/Dedekind_Real.thy		\
wenzelm@33439
   984
  ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy	\
hoelzl@35329
   985
  ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy	\
hoelzl@35329
   986
  ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy		\
hoelzl@35329
   987
  ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy			\
hoelzl@35329
   988
  ex/Induction_Schema.thy ex/InductiveInvariant.thy			\
hoelzl@35329
   989
  ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy		\
hoelzl@35329
   990
  ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy				\
wenzelm@33024
   991
  ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy			\
wenzelm@33024
   992
  ex/Multiquote.thy ex/NatSum.thy ex/Numeral.thy ex/PER.thy		\
bulwahn@37917
   993
  ex/PresburgerEx.thy ex/Primrec.thy 					\
bulwahn@37917
   994
  ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy 	\
wenzelm@33024
   995
  ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy		\
wenzelm@27164
   996
  ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
wenzelm@33024
   997
  ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy		\
wenzelm@33439
   998
  ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy	\
krauss@37760
   999
  ex/Unification.thy ex/While_Combinator_Example.thy ex/document/root.bib \
krauss@37760
  1000
	ex/document/root.tex		\
wenzelm@33024
  1001
  ex/set.thy ex/svc_funcs.ML ex/svc_test.thy
wenzelm@28500
  1002
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
wenzelm@2448
  1003
wenzelm@2448
  1004
wenzelm@33026
  1005
## HOL-Isar_Examples
wenzelm@6445
  1006
wenzelm@33026
  1007
HOL-Isar_Examples: HOL $(LOG)/HOL-Isar_Examples.gz
wenzelm@6445
  1008
wenzelm@33026
  1009
$(LOG)/HOL-Isar_Examples.gz: $(OUT)/HOL Isar_Examples/Basic_Logic.thy	\
wenzelm@33026
  1010
  Isar_Examples/Cantor.thy Isar_Examples/Drinker.thy			\
wenzelm@33026
  1011
  Isar_Examples/Expr_Compiler.thy Isar_Examples/Fibonacci.thy		\
wenzelm@33026
  1012
  Isar_Examples/Group.thy Isar_Examples/Hoare.thy			\
wenzelm@33026
  1013
  Isar_Examples/Hoare_Ex.thy Isar_Examples/Knaster_Tarski.thy		\
wenzelm@33026
  1014
  Isar_Examples/Mutilated_Checkerboard.thy				\
wenzelm@33026
  1015
  Isar_Examples/Nested_Datatype.thy Isar_Examples/Peirce.thy		\
wenzelm@33026
  1016
  Isar_Examples/Puzzle.thy Isar_Examples/Summation.thy			\
wenzelm@33026
  1017
  Isar_Examples/ROOT.ML Isar_Examples/document/proof.sty		\
wenzelm@33026
  1018
  Isar_Examples/document/root.bib Isar_Examples/document/root.tex	\
wenzelm@37672
  1019
  Isar_Examples/document/style.tex Hoare/hoare_tac.ML			\
wenzelm@37672
  1020
  Number_Theory/Primes.thy
wenzelm@33026
  1021
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Isar_Examples
wenzelm@6445
  1022
wenzelm@6445
  1023
wenzelm@33028
  1024
## HOL-SET_Protocol
paulson@14199
  1025
wenzelm@33028
  1026
HOL-SET_Protocol: HOL $(LOG)/HOL-SET_Protocol.gz
paulson@14199
  1027
wenzelm@33028
  1028
$(LOG)/HOL-SET_Protocol.gz: $(OUT)/HOL SET_Protocol/ROOT.ML		\
wenzelm@33028
  1029
  SET_Protocol/Message_SET.thy SET_Protocol/Event_SET.thy		\
wenzelm@33028
  1030
  SET_Protocol/Public_SET.thy SET_Protocol/Cardholder_Registration.thy	\
wenzelm@33028
  1031
  SET_Protocol/Merchant_Registration.thy SET_Protocol/Purchase.thy	\
wenzelm@33028
  1032
  SET_Protocol/document/root.tex
wenzelm@33028
  1033
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL SET_Protocol
paulson@14199
  1034
paulson@14199
  1035
haftmann@27421
  1036
## HOL-Matrix
kleing@14610
  1037
wenzelm@28637
  1038
HOL-Matrix: HOL $(LOG)/HOL-Matrix.gz
obua@17323
  1039
wenzelm@37872
  1040
$(LOG)/HOL-Matrix.gz: $(OUT)/HOL Matrix/ComputeFloat.thy		\
wenzelm@37872
  1041
  Matrix/ComputeHOL.thy Matrix/ComputeNumeral.thy			\
wenzelm@37872
  1042
  Matrix/Compute_Oracle/Compute_Oracle.thy Matrix/Compute_Oracle/am.ML	\
wenzelm@37872
  1043
  Matrix/Compute_Oracle/am_compiler.ML Matrix/Compute_Oracle/am_ghc.ML	\
wenzelm@37872
  1044
  Matrix/Compute_Oracle/am_interpreter.ML				\
wenzelm@37872
  1045
  Matrix/Compute_Oracle/am_sml.ML Matrix/Compute_Oracle/compute.ML	\
wenzelm@37872
  1046
  Matrix/Compute_Oracle/linker.ML Matrix/Cplex.thy			\
haftmann@37764
  1047
  Matrix/CplexMatrixConverter.ML Matrix/Cplex_tools.ML			\
wenzelm@37872
  1048
  Matrix/FloatSparseMatrixBuilder.ML Matrix/LP.thy Matrix/Matrix.thy	\
wenzelm@37872
  1049
  Matrix/ROOT.ML Matrix/SparseMatrix.thy Matrix/document/root.tex	\
wenzelm@37872
  1050
  Matrix/fspmlp.ML Matrix/matrixlp.ML Tools/float_arith.ML
wenzelm@28500
  1051
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Matrix
obua@16873
  1052
paulson@14199
  1053
wenzelm@4518
  1054
## TLA
wenzelm@4518
  1055
wenzelm@4518
  1056
TLA: HOL $(OUT)/TLA
wenzelm@4518
  1057
wenzelm@27164
  1058
$(OUT)/TLA: $(OUT)/HOL TLA/Action.thy TLA/Init.thy TLA/Intensional.thy	\
wenzelm@21624
  1059
  TLA/ROOT.ML TLA/Stfun.thy TLA/TLA.thy
wenzelm@28500
  1060
	@cd TLA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL TLA
wenzelm@4518
  1061
wenzelm@4518
  1062
wenzelm@4518
  1063
## TLA-Inc
wenzelm@4518
  1064
wenzelm@4518
  1065
TLA-Inc: TLA $(LOG)/TLA-Inc.gz
wenzelm@4518
  1066
wenzelm@21624
  1067
$(LOG)/TLA-Inc.gz: $(OUT)/TLA TLA/Inc/Inc.thy
wenzelm@28500
  1068
	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Inc
wenzelm@4518
  1069
wenzelm@4518
  1070
wenzelm@4518
  1071
## TLA-Buffer
wenzelm@4518
  1072
wenzelm@4518
  1073
TLA-Buffer: TLA $(LOG)/TLA-Buffer.gz
wenzelm@2448
  1074
wenzelm@33024
  1075
$(LOG)/TLA-Buffer.gz: $(OUT)/TLA TLA/Buffer/Buffer.thy	\
wenzelm@33024
  1076
  TLA/Buffer/DBuffer.thy
wenzelm@28500
  1077
	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Buffer
wenzelm@4518
  1078
wenzelm@4518
  1079
wenzelm@4518
  1080
## TLA-Memory
wenzelm@4518
  1081
wenzelm@4518
  1082
TLA-Memory: TLA $(LOG)/TLA-Memory.gz
wenzelm@4447
  1083
wenzelm@27164
  1084
$(LOG)/TLA-Memory.gz: $(OUT)/TLA TLA/Memory/MemClerk.thy		\
wenzelm@27164
  1085
  TLA/Memory/MemClerkParameters.thy TLA/Memory/Memory.thy		\
wenzelm@27164
  1086
  TLA/Memory/MemoryImplementation.thy TLA/Memory/MemoryParameters.thy	\
wenzelm@27164
  1087
  TLA/Memory/ProcedureInterface.thy TLA/Memory/RPC.thy			\
wenzelm@21624
  1088
  TLA/Memory/RPCMemoryParams.thy TLA/Memory/RPCParameters.thy
wenzelm@28500
  1089
	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Memory
wenzelm@4518
  1090
wenzelm@4518
  1091
himmelma@33175
  1092
## HOL-Multivariate_Analysis
himmelma@33175
  1093
boehmes@36898
  1094
HOL-Multivariate_Analysis: HOL $(OUT)/HOL-Multivariate_Analysis
himmelma@33175
  1095
wenzelm@36937
  1096
$(OUT)/HOL-Multivariate_Analysis: $(OUT)/HOL				\
wenzelm@36937
  1097
  Multivariate_Analysis/Brouwer_Fixpoint.thy				\
wenzelm@37522
  1098
  Multivariate_Analysis/Cartesian_Euclidean_Space.thy                   \
wenzelm@36937
  1099
  Multivariate_Analysis/Convex_Euclidean_Space.thy			\
wenzelm@36937
  1100
  Multivariate_Analysis/Derivative.thy					\
wenzelm@36937
  1101
  Multivariate_Analysis/Determinants.thy				\
wenzelm@36937
  1102
  Multivariate_Analysis/Euclidean_Space.thy				\
wenzelm@36937
  1103
  Multivariate_Analysis/Fashoda.thy					\
wenzelm@36937
  1104
  Multivariate_Analysis/Finite_Cartesian_Product.thy			\
wenzelm@36937
  1105
  Multivariate_Analysis/Integration.certs				\
wenzelm@36937
  1106
  Multivariate_Analysis/Integration.thy					\
hoelzl@38656
  1107
  Multivariate_Analysis/Gauge_Measure.thy					\
wenzelm@36937
  1108
  Multivariate_Analysis/L2_Norm.thy					\
wenzelm@36937
  1109
  Multivariate_Analysis/Multivariate_Analysis.thy			\
wenzelm@36937
  1110
  Multivariate_Analysis/Operator_Norm.thy				\
wenzelm@36937
  1111
  Multivariate_Analysis/Path_Connected.thy				\
wenzelm@36937
  1112
  Multivariate_Analysis/ROOT.ML						\
wenzelm@36937
  1113
  Multivariate_Analysis/Real_Integration.thy				\
wenzelm@36937
  1114
  Multivariate_Analysis/Topology_Euclidean_Space.thy			\
wenzelm@36937
  1115
  Multivariate_Analysis/document/root.tex				\
haftmann@37742
  1116
  Multivariate_Analysis/normarith.ML Library/Glbs.thy			\
haftmann@37742
  1117
  Library/Inner_Product.thy Library/Numeral_Type.thy			\
wenzelm@36937
  1118
  Library/Convex.thy Library/FrechetDeriv.thy				\
hoelzl@36649
  1119
  Library/Product_Vector.thy Library/Product_plus.thy
boehmes@36898
  1120
	@cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Multivariate_Analysis
himmelma@33175
  1121
wenzelm@33285
  1122
paulson@33271
  1123
## HOL-Probability
paulson@33271
  1124
hoelzl@38656
  1125
HOL-Probability: HOL-Multivariate_Analysis $(OUT)/HOL-Probability
paulson@33271
  1126
hoelzl@38656
  1127
$(OUT)/HOL-Probability: $(OUT)/HOL-Multivariate_Analysis Probability/ROOT.ML	\
haftmann@37742
  1128
  Probability/Probability.thy Probability/Sigma_Algebra.thy		\
hoelzl@38656
  1129
  Probability/Caratheodory.thy		\
haftmann@37742
  1130
  Probability/Borel.thy Probability/Measure.thy				\
hoelzl@38656
  1131
  Probability/Lebesgue_Integration.thy Probability/Lebesgue_Measure.thy		\
hoelzl@38656
  1132
  Probability/Positive_Infinite_Real.thy Probability/Product_Measure.thy	\
haftmann@37742
  1133
  Probability/Probability_Space.thy Probability/Information.thy		\
haftmann@37742
  1134
  Probability/ex/Dining_Cryptographers.thy Library/FuncSet.thy		\
hoelzl@38656
  1135
  Probability/Lebesgue_Measure.thy \
hoelzl@38656
  1136
  Library/Nat_Bijection.thy Library/Countable.thy
hoelzl@38656
  1137
	@cd Probability; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Multivariate_Analysis HOL-Probability
paulson@33271
  1138
berghofe@19497
  1139
## HOL-Nominal
berghofe@19497
  1140
berghofe@19497
  1141
HOL-Nominal: HOL $(OUT)/HOL-Nominal
berghofe@19497
  1142
urbanc@22245
  1143
$(OUT)/HOL-Nominal: $(OUT)/HOL Nominal/ROOT.ML \
urbanc@22245
  1144
  Nominal/Nominal.thy \
urbanc@22245
  1145
  Nominal/nominal_atoms.ML \
haftmann@31936
  1146
  Nominal/nominal_datatype.ML \
berghofe@22784
  1147
  Nominal/nominal_fresh_fun.ML \
urbanc@22247
  1148
  Nominal/nominal_induct.ML \
berghofe@22314
  1149
  Nominal/nominal_inductive.ML \
berghofe@28652
  1150
  Nominal/nominal_inductive2.ML \
urbanc@22245
  1151
  Nominal/nominal_permeq.ML \
urbanc@22245
  1152
  Nominal/nominal_primrec.ML \
urbanc@22245
  1153
  Nominal/nominal_thmdecls.ML \
berghofe@21542
  1154
  Library/Infinite_Set.thy
wenzelm@28500
  1155
	@cd Nominal; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Nominal
berghofe@19497
  1156
berghofe@19497
  1157
berghofe@19497
  1158
## HOL-Nominal-Examples
berghofe@19497
  1159
berghofe@19497
  1160
HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz
berghofe@19497
  1161
krauss@19564
  1162
$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal 	\
haftmann@32636
  1163
  Nominal/Examples/Nominal_Examples.thy \
urbanc@27163
  1164
  Nominal/Examples/CK_Machine.thy \
urbanc@22073
  1165
  Nominal/Examples/CR.thy \
urbanc@22821
  1166
  Nominal/Examples/CR_Takahashi.thy \
wenzelm@36277
  1167
  Nominal/Examples/Class1.thy \
wenzelm@36277
  1168
  Nominal/Examples/Class2.thy \
wenzelm@36277
  1169
  Nominal/Examples/Class3.thy \
urbanc@22073
  1170
  Nominal/Examples/Compile.thy \
wenzelm@25725
  1171
  Nominal/Examples/Contexts.thy \
wenzelm@25725
  1172
  Nominal/Examples/Crary.thy \
urbanc@22073
  1173
  Nominal/Examples/Fsub.thy \
wenzelm@25725
  1174
  Nominal/Examples/Height.thy \
wenzelm@25725
  1175
  Nominal/Examples/Lam_Funs.thy \
urbanc@22073
  1176
  Nominal/Examples/Lambda_mu.thy \
wenzelm@25725
  1177
  Nominal/Examples/LocalWeakening.thy \
berghofe@33189
  1178
  Nominal/Examples/Pattern.thy \
wenzelm@25725
  1179
  Nominal/Examples/ROOT.ML \
urbanc@22073
  1180
  Nominal/Examples/SN.thy \
urbanc@23144
  1181
  Nominal/Examples/SOS.thy \
berghofe@27624
  1182
  Nominal/Examples/Standardization.thy \
urbanc@24896
  1183
  Nominal/Examples/Support.thy \
urbanc@27032
  1184
  Nominal/Examples/Type_Preservation.thy \
wenzelm@25725
  1185
  Nominal/Examples/VC_Condition.thy \
urbanc@26195
  1186
  Nominal/Examples/W.thy \
wenzelm@25725
  1187
  Nominal/Examples/Weakening.thy
wenzelm@28500
  1188
	@cd Nominal; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Nominal Examples
berghofe@19497
  1189
berghofe@19497
  1190
kleing@24333
  1191
## HOL-Word
kleing@24333
  1192
kleing@24333
  1193
HOL-Word: HOL $(OUT)/HOL-Word
kleing@24333
  1194
wenzelm@33024
  1195
$(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML Library/Boolean_Algebra.thy	\
haftmann@37655
  1196
  Library/Numeral_Type.thy Word/Misc_Numeric.thy Word/Misc_Typedef.thy	\
haftmann@37659
  1197
  Word/Type_Length.thy Word/Bit_Representation.thy Word/Bit_Int.thy	\
haftmann@37659
  1198
  Word/Bool_List_Representation.thy Word/Bit_Operations.thy		\
haftmann@37660
  1199
  Word/Word.thy Word/document/root.tex					\
boehmes@36899
  1200
  Word/document/root.bib Tools/SMT/smt_word.ML
wenzelm@28500
  1201
	@cd Word; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Word
kleing@24333
  1202
kleing@24333
  1203
huffman@24442
  1204
## HOL-Word-Examples
huffman@24442
  1205
huffman@24442
  1206
HOL-Word-Examples: HOL-Word $(LOG)/HOL-Word-Examples.gz
huffman@24442
  1207
wenzelm@27164
  1208
$(LOG)/HOL-Word-Examples.gz: $(OUT)/HOL-Word Word/Examples/ROOT.ML	\
huffman@24442
  1209
  Word/Examples/WordExamples.thy
wenzelm@28500
  1210
	@cd Word; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Word Examples
huffman@24442
  1211
wenzelm@27477
  1212
schirmer@25171
  1213
## HOL-Statespace
schirmer@25171
  1214
schirmer@25171
  1215
HOL-Statespace: HOL $(LOG)/HOL-Statespace.gz
schirmer@25171
  1216
wenzelm@27164
  1217
$(LOG)/HOL-Statespace.gz: $(OUT)/HOL Statespace/DistinctTreeProver.thy	\
wenzelm@27164
  1218
  Statespace/StateFun.thy Statespace/StateSpaceLocale.thy		\
wenzelm@27164
  1219
  Statespace/StateSpaceSyntax.thy Statespace/StateSpaceEx.thy		\
wenzelm@27164
  1220
  Statespace/distinct_tree_prover.ML Statespace/state_space.ML		\
wenzelm@27164
  1221
  Statespace/state_fun.ML Statespace/document/root.tex
wenzelm@28500
  1222
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Statespace
huffman@24442
  1223
wenzelm@27477
  1224
huffman@27470
  1225
## HOL-NSA
huffman@27470
  1226
wenzelm@27477
  1227
HOL-NSA: HOL $(OUT)/HOL-NSA
huffman@27470
  1228
wenzelm@33024
  1229
$(OUT)/HOL-NSA: $(OUT)/HOL NSA/CLim.thy NSA/CStar.thy NSA/NSCA.thy	\
wenzelm@33024
  1230
  NSA/NSComplex.thy NSA/HDeriv.thy NSA/HLim.thy NSA/HLog.thy		\
wenzelm@33024
  1231
  NSA/HSEQ.thy NSA/HSeries.thy NSA/HTranscendental.thy			\
wenzelm@33024
  1232
  NSA/Hypercomplex.thy NSA/HyperDef.thy NSA/HyperNat.thy		\
wenzelm@33024
  1233
  NSA/Hyperreal.thy NSA/Filter.thy NSA/NatStar.thy NSA/NSA.thy		\
wenzelm@33024
  1234
  NSA/StarDef.thy NSA/Star.thy NSA/transfer.ML				\
wenzelm@33024
  1235
  Library/Infinite_Set.thy Library/Zorn.thy NSA/ROOT.ML
wenzelm@28500
  1236
	@cd NSA; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-NSA
huffman@27470
  1237
wenzelm@27477
  1238
huffman@27470
  1239
## HOL-NSA-Examples
huffman@27470
  1240
huffman@27470
  1241
HOL-NSA-Examples: HOL-NSA $(LOG)/HOL-NSA-Examples.gz
huffman@27470
  1242
haftmann@37742
  1243
$(LOG)/HOL-NSA-Examples.gz: $(OUT)/HOL-NSA NSA/Examples/ROOT.ML		\
huffman@27470
  1244
  NSA/Examples/NSPrimes.thy
wenzelm@28500
  1245
	@cd NSA; $(ISABELLE_TOOL) usedir $(OUT)/HOL-NSA Examples
huffman@27470
  1246
wenzelm@27477
  1247
boehmes@32496
  1248
## HOL-Mirabelle
boehmes@32496
  1249
boehmes@32496
  1250
HOL-Mirabelle: HOL $(LOG)/HOL-Mirabelle.gz
boehmes@32496
  1251
wenzelm@33024
  1252
$(LOG)/HOL-Mirabelle.gz: $(OUT)/HOL Mirabelle/Mirabelle_Test.thy	\
wenzelm@33024
  1253
  Mirabelle/Mirabelle.thy Mirabelle/Tools/mirabelle.ML			\
wenzelm@33024
  1254
  Mirabelle/ROOT.ML Mirabelle/Tools/mirabelle_arith.ML			\
wenzelm@33024
  1255
  Mirabelle/Tools/mirabelle_metis.ML					\
wenzelm@33024
  1256
  Mirabelle/Tools/mirabelle_quickcheck.ML				\
wenzelm@33024
  1257
  Mirabelle/Tools/mirabelle_refute.ML					\
boehmes@32496
  1258
  Mirabelle/Tools/mirabelle_sledgehammer.ML
boehmes@32496
  1259
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
boehmes@32496
  1260
boehmes@32496
  1261
wenzelm@36933
  1262
## HOL-Word-SMT_Examples
boehmes@32618
  1263
wenzelm@36933
  1264
HOL-Word-SMT_Examples: HOL-Word $(LOG)/HOL-Word-SMT_Examples.gz
boehmes@32618
  1265
wenzelm@36933
  1266
$(LOG)/HOL-Word-SMT_Examples.gz: $(OUT)/HOL-Word SMT_Examples/ROOT.ML	\
boehmes@36899
  1267
  SMT_Examples/SMT_Examples.thy SMT_Examples/SMT_Examples.certs		\
boehmes@36899
  1268
  SMT_Examples/SMT_Word_Examples.thy SMT_Examples/SMT_Tests.thy		\
boehmes@36899
  1269
  SMT_Examples/SMT_Word_Examples.certs SMT_Examples/SMT_Tests.certs
boehmes@36899
  1270
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL-Word SMT_Examples
boehmes@33010
  1271
boehmes@33010
  1272
boehmes@33419
  1273
## HOL-Boogie
boehmes@33419
  1274
boehmes@36899
  1275
HOL-Boogie: HOL-Word $(OUT)/HOL-Boogie
boehmes@33419
  1276
boehmes@36901
  1277
$(OUT)/HOL-Boogie: $(OUT)/HOL-Word Boogie/ROOT.ML Boogie/Boogie.thy	\
wenzelm@33439
  1278
  Boogie/Tools/boogie_vcs.ML Boogie/Tools/boogie_loader.ML		\
boehmes@34069
  1279
  Boogie/Tools/boogie_commands.ML Boogie/Tools/boogie_tactics.ML
boehmes@36899
  1280
	@cd Boogie; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-Boogie
boehmes@33419
  1281
boehmes@33419
  1282
boehmes@33419
  1283
## HOL-Boogie_Examples
boehmes@33419
  1284
wenzelm@33439
  1285
HOL-Boogie-Examples: HOL-Boogie $(LOG)/HOL-Boogie-Examples.gz
boehmes@33419
  1286
wenzelm@33439
  1287
$(LOG)/HOL-Boogie-Examples.gz: $(OUT)/HOL-Boogie			\
wenzelm@33439
  1288
  Boogie/Examples/ROOT.ML Boogie/Examples/Boogie_Max.thy		\
wenzelm@33439
  1289
  Boogie/Examples/Boogie_Max.b2i Boogie/Examples/Boogie_Dijkstra.thy	\
wenzelm@33439
  1290
  Boogie/Examples/VCC_Max.thy Boogie/Examples/Boogie_Dijkstra.b2i	\
boehmes@34996
  1291
  Boogie/Examples/VCC_Max.b2i Boogie/Examples/Boogie_Max.certs		\
boehmes@34996
  1292
  Boogie/Examples/Boogie_Dijkstra.certs Boogie/Examples/VCC_Max.certs
boehmes@33419
  1293
	@cd Boogie; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Boogie Examples
boehmes@33419
  1294
boehmes@33419
  1295
bulwahn@34965
  1296
## HOL-Mutabelle
bulwahn@34965
  1297
bulwahn@34965
  1298
HOL-Mutabelle: HOL $(LOG)/HOL-Mutabelle.gz
bulwahn@34965
  1299
bulwahn@34965
  1300
$(LOG)/HOL-Mutabelle.gz: $(OUT)/HOL Mutabelle/MutabelleExtra.thy	\
wenzelm@35959
  1301
  Mutabelle/ROOT.ML Mutabelle/mutabelle.ML				\
bulwahn@34965
  1302
  Mutabelle/mutabelle_extra.ML
bulwahn@34965
  1303
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mutabelle
bulwahn@34965
  1304
bulwahn@34965
  1305
kaliszyk@35222
  1306
## HOL-Quotient_Examples
kaliszyk@35222
  1307
kaliszyk@35222
  1308
HOL-Quotient_Examples: HOL $(LOG)/HOL-Quotient_Examples.gz
kaliszyk@35222
  1309
wenzelm@35959
  1310
$(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL				\
haftmann@37742
  1311
  Quotient_Examples/FSet.thy Quotient_Examples/Quotient_Int.thy		\
kaliszyk@36524
  1312
  Quotient_Examples/Quotient_Message.thy
kaliszyk@35222
  1313
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
kaliszyk@35222
  1314
kaliszyk@35222
  1315
bulwahn@35950
  1316
## HOL-Predicate_Compile_Examples
bulwahn@35950
  1317
bulwahn@35950
  1318
HOL-Predicate_Compile_Examples: HOL $(LOG)/HOL-Predicate_Compile_Examples.gz
bulwahn@35950
  1319
wenzelm@35959
  1320
$(LOG)/HOL-Predicate_Compile_Examples.gz: $(OUT)/HOL			\
bulwahn@35955
  1321
  Predicate_Compile_Examples/ROOT.ML					\
bulwahn@35955
  1322
  Predicate_Compile_Examples/Predicate_Compile_Examples.thy		\
bulwahn@38074
  1323
  Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy  \
bulwahn@38074
  1324
  Predicate_Compile_Examples/Code_Prolog_Examples.thy
bulwahn@35950
  1325
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Predicate_Compile_Examples
kaliszyk@35222
  1326
wenzelm@35959
  1327
wenzelm@4518
  1328
## clean
wenzelm@4447
  1329
wenzelm@4447
  1330
clean:
wenzelm@33450
  1331
	@rm -f $(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz			\
wenzelm@33450
  1332
		$(LOG)/HOL-Bali.gz $(LOG)/HOL-Base.gz			\
wenzelm@33450
  1333
		$(LOG)/HOL-Boogie-Examples.gz $(LOG)/HOL-Boogie.gz	\
wenzelm@34205
  1334
		$(LOG)/HOL-Decision_Procs.gz $(LOG)/HOL-Hahn_Banach.gz	\
wenzelm@34205
  1335
		$(LOG)/HOL-Hoare.gz $(LOG)/HOL-Hoare_Parallel.gz	\
wenzelm@34205
  1336
		$(LOG)/HOL-IMP.gz $(LOG)/HOL-IMPP.gz $(LOG)/HOL-IOA.gz	\
wenzelm@33450
  1337
		$(LOG)/HOL-Imperative_HOL.gz $(LOG)/HOL-Import.gz	\
wenzelm@33450
  1338
		$(LOG)/HOL-Induct.gz $(LOG)/HOL-Isar_Examples.gz	\
wenzelm@34205
  1339
		$(LOG)/HOL-Lattice $(LOG)/HOL-Lattice.gz		\
wenzelm@34205
  1340
		$(LOG)/HOL-Lex.gz $(LOG)/HOL-Library.gz			\
wenzelm@34205
  1341
		$(LOG)/HOL-Main.gz $(LOG)/HOL-Matrix			\
wenzelm@34205
  1342
		$(LOG)/HOL-Matrix.gz $(LOG)/HOL-Metis_Examples.gz	\
wenzelm@34205
  1343
		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-Mirabelle.gz		\
wenzelm@33450
  1344
		$(LOG)/HOL-Multivariate_Analysis.gz			\
wenzelm@33450
  1345
		$(LOG)/HOL-NSA-Examples.gz $(LOG)/HOL-NSA.gz		\
wenzelm@33450
  1346
		$(LOG)/HOL-NanoJava.gz $(LOG)/HOL-Nitpick_Examples.gz	\
wenzelm@33450
  1347
		$(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-Nominal.gz	\
wenzelm@33450
  1348
		$(LOG)/HOL-Number_Theory.gz				\
wenzelm@33450
  1349
		$(LOG)/HOL-Old_Number_Theory.gz $(LOG)/HOL-Plain.gz	\
wenzelm@35959
  1350
		$(LOG)/HOL-Predicate_Compile_Examples.gz		\
wenzelm@33450
  1351
		$(LOG)/HOL-Probability.gz $(LOG)/HOL-Prolog.gz		\
wenzelm@34205
  1352
		$(LOG)/HOL-Proofs.gz $(LOG)/HOL-Proofs-Extraction.gz	\
wenzelm@34205
  1353
		$(LOG)/HOL-Proofs-Lambda.gz $(LOG)/HOL-SET_Protocol.gz	\
wenzelm@36933
  1354
		$(LOG)/HOL-Word-SMT_Examples.gz				\
wenzelm@36933
  1355
		$(LOG)/HOL-Statespace.gz $(LOG)/HOL-Subst.gz		\
wenzelm@36933
  1356
		$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz			\
wenzelm@36933
  1357
		$(LOG)/HOL-Word-Examples.gz $(LOG)/HOL-Word.gz		\
wenzelm@36933
  1358
		$(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz $(LOG)/HOL.gz		\
wenzelm@36933
  1359
		$(LOG)/HOL4.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Inc.gz	\
wenzelm@36933
  1360
		$(LOG)/TLA-Memory.gz $(LOG)/TLA.gz $(OUT)/HOL		\
wenzelm@36933
  1361
		$(OUT)/HOL-Algebra $(OUT)/HOL-Base $(OUT)/HOL-Boogie	\
wenzelm@36933
  1362
		$(OUT)/HOL-Main $(OUT)/HOL-Multivariate_Analysis	\
wenzelm@36933
  1363
		$(OUT)/HOL-NSA $(OUT)/HOL-Nominal $(OUT)/HOL-Plain	\
wenzelm@35931
  1364
		$(OUT)/HOL-Probability $(OUT)/HOL-Proofs		\
boehmes@36898
  1365
		$(OUT)/HOL-Word $(OUT)/HOL4 $(OUT)/TLA