src/HOL/IsaMakefile
author kleing
Mon, 20 Aug 2007 04:34:31 +0200
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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
     1
#
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
     2
# IsaMakefile for HOL
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
     3
#
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
     4
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
     5
## targets
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
     6
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
     7
default: HOL
17460
7780d953598c generate: added HOL-Complex-Generate-HOLLight;
wenzelm
parents: 17430
diff changeset
     8
generate: HOL-Complex-Generate-HOL HOL-Complex-Generate-HOLLight
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
     9
images: HOL HOL-Algebra HOL-Complex HOL-Complex-Matrix HOL-Nominal \
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
    10
        HOL-Word TLA HOL4
10135
c2a4dccf6e67 reorganized AxClasses;
wenzelm
parents: 10094
diff changeset
    11
10255
bb66874b4750 added HOL/Library, rearranged several files;
wenzelm
parents: 10214
diff changeset
    12
#Note: keep targets sorted (except for HOL-Library)
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    13
test: \
24325
5c29e8822f50 make HOL-ex earlier;
wenzelm
parents: 24288
diff changeset
    14
  HOL-ex \
10255
bb66874b4750 added HOL/Library, rearranged several files;
wenzelm
parents: 10214
diff changeset
    15
  HOL-Library \
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    16
  HOL-Auth \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    17
  HOL-AxClasses \
14031
3240066af013 Added Bali to test
schirmer
parents: 14029
diff changeset
    18
  HOL-Bali \
17610
58778df33e2f tuned order of targets;
wenzelm
parents: 17546
diff changeset
    19
  HOL-Complex-HahnBanach \
15771
08cc20626a0f restored the target HOL-Complex-Import
paulson
parents: 15731
diff changeset
    20
  HOL-Complex-Import \
17610
58778df33e2f tuned order of targets;
wenzelm
parents: 17546
diff changeset
    21
  HOL-Complex-ex \
13403
bc2b32ee62fd Added theory for setting up program extraction.
berghofe
parents: 13224
diff changeset
    22
  HOL-Extraction \
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    23
  HOL-Hoare \
13019
98f0a09a33c3 Target HoareParallel in IsaMakefile
prensani
parents: 13004
diff changeset
    24
  HOL-HoareParallel \
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    25
  HOL-IMP \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    26
  HOL-IMPP \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    27
  HOL-IOA \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    28
  HOL-Induct \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    29
  HOL-Isar_examples \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    30
  HOL-Lambda \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    31
  HOL-Lattice \
23449
dd874e6a3282 integration of Metis prover
paulson
parents: 23445
diff changeset
    32
  HOL-MetisExamples \
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    33
  HOL-MicroJava \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    34
  HOL-Modelcheck \
11376
bf98ad1c22c6 added NanoJava
oheimb
parents: 11370
diff changeset
    35
  HOL-NanoJava \
19497
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
    36
  HOL-Nominal-Examples \
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    37
  HOL-NumberTheory \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    38
  HOL-Prolog \
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
    39
  HOL-SET-Protocol \
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    40
  HOL-Subst \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    41
      TLA-Buffer \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    42
      TLA-Inc \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    43
      TLA-Memory \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    44
  HOL-UNITY \
10966
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
    45
  HOL-Unix \
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    46
  HOL-W0 \
24325
5c29e8822f50 make HOL-ex earlier;
wenzelm
parents: 24288
diff changeset
    47
  HOL-ZF
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    48
    # ^ this is the sort position
10614
d5c14e205c24 added Library/Rational_Numbers.thy;
wenzelm
parents: 10574
diff changeset
    49
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    50
all: test images
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
    51
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
    52
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
    53
## global settings
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
    54
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
    55
SRC = $(ISABELLE_HOME)/src
3118
24dae6222579 fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?);
wenzelm
parents: 3079
diff changeset
    56
OUT = $(ISABELLE_OUTPUT)
4447
b7ee449eb345 log files;
wenzelm
parents: 4289
diff changeset
    57
LOG = $(OUT)/log
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    58
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
    59
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
    60
## HOL
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    61
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
    62
HOL: Pure $(OUT)/HOL
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
    63
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
    64
Pure:
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
    65
	@cd $(SRC)/Pure; $(ISATOOL) make Pure
3232
19a2b853ba7b Removal of ex/LexProd; TFL files; new treatment of Prover files
paulson
parents: 3222
diff changeset
    66
23194
webertj
parents: 23193
diff changeset
    67
$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML		\
webertj
parents: 23193
diff changeset
    68
  $(SRC)/Provers/Arith/assoc_fold.ML					\
webertj
parents: 23193
diff changeset
    69
  $(SRC)/Provers/Arith/cancel_div_mod.ML				\
webertj
parents: 23193
diff changeset
    70
  $(SRC)/Provers/Arith/cancel_numeral_factor.ML				\
webertj
parents: 23193
diff changeset
    71
  $(SRC)/Provers/Arith/cancel_numerals.ML				\
webertj
parents: 23193
diff changeset
    72
  $(SRC)/Provers/Arith/cancel_sums.ML					\
webertj
parents: 23193
diff changeset
    73
  $(SRC)/Provers/Arith/combine_numerals.ML				\
webertj
parents: 23193
diff changeset
    74
  $(SRC)/Provers/Arith/extract_common_term.ML				\
webertj
parents: 23193
diff changeset
    75
  $(SRC)/Provers/Arith/fast_lin_arith.ML				\
webertj
parents: 23193
diff changeset
    76
  $(SRC)/Tools/IsaPlanner/isand.ML					\
webertj
parents: 23193
diff changeset
    77
  $(SRC)/Tools/IsaPlanner/rw_inst.ML					\
webertj
parents: 23193
diff changeset
    78
  $(SRC)/Tools/IsaPlanner/rw_tools.ML					\
webertj
parents: 23193
diff changeset
    79
  $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Provers/blast.ML		\
webertj
parents: 23193
diff changeset
    80
  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML			\
webertj
parents: 23193
diff changeset
    81
  $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML			\
webertj
parents: 23193
diff changeset
    82
  $(SRC)/Provers/induct_method.ML $(SRC)/Provers/order.ML		\
webertj
parents: 23193
diff changeset
    83
  $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML		\
webertj
parents: 23193
diff changeset
    84
  $(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML			\
24139
eac44d0fe228 added dependency on Tools/Metis/metis.ML;
wenzelm
parents: 24127
diff changeset
    85
  $(SRC)/Provers/trancl.ML $(SRC)/Tools/integer.ML $(SRC)/Tools/Metis/metis.ML\
24280
c9867bdf2424 updated code generator setup
haftmann
parents: 24194
diff changeset
    86
  $(SRC)/Pure/codegen.ML			\
c9867bdf2424 updated code generator setup
haftmann
parents: 24194
diff changeset
    87
  $(SRC)/Tools/code/code_funcgr.ML			\
c9867bdf2424 updated code generator setup
haftmann
parents: 24194
diff changeset
    88
  $(SRC)/Tools/code/code_name.ML $(SRC)/Tools/code/code_package.ML		\
c9867bdf2424 updated code generator setup
haftmann
parents: 24194
diff changeset
    89
  $(SRC)/Tools/code/code_target.ML $(SRC)/Tools/code/code_thingol.ML	\
24162
8dfd5dd65d82 split off theory Option for benefit of code generator
haftmann
parents: 24152
diff changeset
    90
  $(SRC)/Tools/nbe.ML $(SRC)/Tools/rat.ML Tools/TFL/casesplit.ML ATP_Linkup.thy	\
24280
c9867bdf2424 updated code generator setup
haftmann
parents: 24194
diff changeset
    91
  Accessible_Part.thy Arith_Tools.thy Code_Setup.thy Datatype.thy 			\
23462
11728d83794c renamed NatSimprocs.thy to Arith_Tools.thy;
wenzelm
parents: 23454
diff changeset
    92
  Dense_Linear_Order.thy Divides.thy Equiv_Relations.thy Extraction.thy	\
11728d83794c renamed NatSimprocs.thy to Arith_Tools.thy;
wenzelm
parents: 23454
diff changeset
    93
  Finite_Set.thy FixedPoint.thy Fun.thy FunDef.thy HOL.thy		\
11728d83794c renamed NatSimprocs.thy to Arith_Tools.thy;
wenzelm
parents: 23454
diff changeset
    94
  Hilbert_Choice.thy Inductive.thy IntArith.thy IntDef.thy IntDiv.thy	\
23882
83b0f2518380 dropped Nat.ML legacy bindings
haftmann
parents: 23854
diff changeset
    95
  Lattices.thy List.thy Main.thy Map.thy Nat.thy NatBin.thy	\
24194
96013f81faef re-eliminated Option.thy
haftmann
parents: 24162
diff changeset
    96
  Numeral.thy OrderedGroup.thy Orderings.thy Power.thy PreList.thy	\
23462
11728d83794c renamed NatSimprocs.thy to Arith_Tools.thy;
wenzelm
parents: 23454
diff changeset
    97
  Predicate.thy Product_Type.thy ROOT.ML Recdef.thy			\
23252
67268bb40b21 Semiring normalization and Groebner Bases.
wenzelm
parents: 23247
diff changeset
    98
  Record.thy Refute.thy Relation.thy Relation_Power.thy			\
67268bb40b21 Semiring normalization and Groebner Bases.
wenzelm
parents: 23247
diff changeset
    99
  Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy Sum_Type.thy	\
24288
4016baca4973 combining the relevance filter with res_atp
paulson
parents: 24280
diff changeset
   100
  Groebner_Basis.thy Tools/watcher.ML	\
23252
67268bb40b21 Semiring normalization and Groebner Bases.
wenzelm
parents: 23247
diff changeset
   101
  Tools/Groebner_Basis/groebner.ML Tools/Groebner_Basis/misc.ML		\
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents: 23462
diff changeset
   102
  Tools/Groebner_Basis/normalizer.ML					\
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents: 23462
diff changeset
   103
  Tools/Groebner_Basis/normalizer_data.ML Tools/Qelim/cooper.ML		\
24082
2811a7c0f3b1 Added dependency on langford files in Tools/Qelim
chaieb
parents: 24036
diff changeset
   104
  Tools/Qelim/langford_data.ML Tools/Qelim/langford.ML		\
23466
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents: 23462
diff changeset
   105
  Tools/Qelim/cooper_data.ML Tools/Qelim/ferrante_rackoff.ML		\
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents: 23462
diff changeset
   106
  Tools/Qelim/ferrante_rackoff_data.ML Tools/Qelim/generated_cooper.ML	\
886655a150f6 moved quantifier elimination tools to Tools/Qelim/;
wenzelm
parents: 23462
diff changeset
   107
  Tools/Qelim/presburger.ML Tools/Qelim/qelim.ML			\
23454
c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
wenzelm
parents: 23449
diff changeset
   108
  Tools/TFL/dcterm.ML Tools/TFL/post.ML Tools/TFL/rules.ML		\
c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
wenzelm
parents: 23449
diff changeset
   109
  Tools/TFL/tfl.ML Tools/TFL/thms.ML Tools/TFL/thry.ML			\
c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
wenzelm
parents: 23449
diff changeset
   110
  Tools/TFL/usyntax.ML Tools/TFL/utils.ML Tools/cnf_funcs.ML		\
c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
wenzelm
parents: 23449
diff changeset
   111
  Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML			\
c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
wenzelm
parents: 23449
diff changeset
   112
  Tools/datatype_case.ML Tools/datatype_codegen.ML			\
c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
wenzelm
parents: 23449
diff changeset
   113
  Tools/datatype_hooks.ML Tools/datatype_package.ML			\
c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
wenzelm
parents: 23449
diff changeset
   114
  Tools/datatype_prop.ML Tools/datatype_realizer.ML			\
c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
wenzelm
parents: 23449
diff changeset
   115
  Tools/datatype_rep_proofs.ML Tools/function_package/auto_term.ML	\
23194
webertj
parents: 23193
diff changeset
   116
  Tools/function_package/context_tree.ML				\
webertj
parents: 23193
diff changeset
   117
  Tools/function_package/fundef_common.ML				\
webertj
parents: 23193
diff changeset
   118
  Tools/function_package/fundef_core.ML					\
webertj
parents: 23193
diff changeset
   119
  Tools/function_package/fundef_datatype.ML				\
webertj
parents: 23193
diff changeset
   120
  Tools/function_package/fundef_lib.ML					\
webertj
parents: 23193
diff changeset
   121
  Tools/function_package/fundef_package.ML				\
webertj
parents: 23193
diff changeset
   122
  Tools/function_package/inductive_wrap.ML				\
webertj
parents: 23193
diff changeset
   123
  Tools/function_package/lexicographic_order.ML				\
webertj
parents: 23193
diff changeset
   124
  Tools/function_package/mutual.ML					\
23574
42765aff66d6 added Tools/numeral.ML;
wenzelm
parents: 23549
diff changeset
   125
  Tools/function_package/pattern_split.ML Tools/inductive_codegen.ML	\
23734
0e11b904b3a3 Added new package for inductive sets.
berghofe
parents: 23666
diff changeset
   126
  Tools/inductive_package.ML Tools/inductive_realizer.ML		\
24091
109f19a13872 added Tools/lin_arith.ML;
wenzelm
parents: 24082
diff changeset
   127
  Tools/inductive_set_package.ML Tools/lin_arith.ML Tools/meson.ML	\
23574
42765aff66d6 added Tools/numeral.ML;
wenzelm
parents: 23549
diff changeset
   128
  Tools/metis_tools.ML Tools/numeral.ML Tools/numeral_syntax.ML		\
23734
0e11b904b3a3 Added new package for inductive sets.
berghofe
parents: 23666
diff changeset
   129
  Tools/polyhash.ML Tools/primrec_package.ML Tools/prop_logic.ML 	\
23454
c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
wenzelm
parents: 23449
diff changeset
   130
  Tools/recdef_package.ML Tools/recfun_codegen.ML			\
c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
wenzelm
parents: 23449
diff changeset
   131
  Tools/record_package.ML Tools/refute.ML Tools/refute_isar.ML		\
c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
wenzelm
parents: 23449
diff changeset
   132
  Tools/res_atp.ML Tools/res_atp_methods.ML Tools/res_atp_provers.ML	\
24036
936cc23a3472 removed obsolete Tools/res_atpset.ML;
wenzelm
parents: 23882
diff changeset
   133
  Tools/res_axioms.ML Tools/res_clause.ML Tools/res_hol_clause.ML	\
936cc23a3472 removed obsolete Tools/res_atpset.ML;
wenzelm
parents: 23882
diff changeset
   134
  Tools/res_reconstruct.ML Tools/rewrite_hol_proof.ML 			\
936cc23a3472 removed obsolete Tools/res_atpset.ML;
wenzelm
parents: 23882
diff changeset
   135
  Tools/sat_funcs.ML Tools/sat_solver.ML Tools/specification_package.ML	\
936cc23a3472 removed obsolete Tools/res_atpset.ML;
wenzelm
parents: 23882
diff changeset
   136
  Tools/split_rule.ML Tools/string_syntax.ML Tools/typecopy_package.ML	\
23194
webertj
parents: 23193
diff changeset
   137
  Tools/typedef_codegen.ML Tools/typedef_package.ML			\
webertj
parents: 23193
diff changeset
   138
  Transitive_Closure.thy Typedef.thy Wellfounded_Recursion.thy		\
webertj
parents: 23193
diff changeset
   139
  Wellfounded_Relations.thy arith_data.ML document/root.tex hologic.ML	\
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents: 23150
diff changeset
   140
  int_arith1.ML int_factor_simprocs.ML nat_simprocs.ML simpdata.ML
16187
6ec757011ad6 renamed HOL_PROOF_OBJECTS to HOL_USEDIR_OPTIONS;
wenzelm
parents: 16090
diff changeset
   141
	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   142
13029
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents: 13019
diff changeset
   143
13967
9cdab3186c0b fixed HOL-Real-HahnBanach (-> HOL-Complex-HahnBanach)
kleing
parents: 13966
diff changeset
   144
## HOL-Complex-HahnBanach
13029
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents: 13019
diff changeset
   145
13967
9cdab3186c0b fixed HOL-Real-HahnBanach (-> HOL-Complex-HahnBanach)
kleing
parents: 13966
diff changeset
   146
HOL-Complex-HahnBanach: HOL-Complex $(LOG)/HOL-Complex-HahnBanach.gz
13029
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents: 13019
diff changeset
   147
16019
0e1405402d53 Simplifier already setup in Pure;
wenzelm
parents: 15871
diff changeset
   148
$(LOG)/HOL-Complex-HahnBanach.gz: $(OUT)/HOL-Complex			\
0e1405402d53 Simplifier already setup in Pure;
wenzelm
parents: 15871
diff changeset
   149
  Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy		\
0e1405402d53 Simplifier already setup in Pure;
wenzelm
parents: 15871
diff changeset
   150
  Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy	\
0e1405402d53 Simplifier already setup in Pure;
wenzelm
parents: 15871
diff changeset
   151
  Real/HahnBanach/HahnBanachExtLemmas.thy				\
0e1405402d53 Simplifier already setup in Pure;
wenzelm
parents: 15871
diff changeset
   152
  Real/HahnBanach/HahnBanachSupLemmas.thy				\
0e1405402d53 Simplifier already setup in Pure;
wenzelm
parents: 15871
diff changeset
   153
  Real/HahnBanach/Linearform.thy Real/HahnBanach/NormedSpace.thy	\
0e1405402d53 Simplifier already setup in Pure;
wenzelm
parents: 15871
diff changeset
   154
  Real/HahnBanach/README.html Real/HahnBanach/ROOT.ML			\
0e1405402d53 Simplifier already setup in Pure;
wenzelm
parents: 15871
diff changeset
   155
  Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy		\
0e1405402d53 Simplifier already setup in Pure;
wenzelm
parents: 15871
diff changeset
   156
  Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/root.bib	\
13029
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents: 13019
diff changeset
   157
  Real/HahnBanach/document/root.tex
13966
2160abf7cfe7 removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents: 13964
diff changeset
   158
	@cd Real; $(ISATOOL) usedir -g true $(OUT)/HOL-Complex HahnBanach
13029
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents: 13019
diff changeset
   159
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents: 13019
diff changeset
   160
13961
233dd3bb2390 new directory Complex
paulson
parents: 13949
diff changeset
   161
## HOL-Complex
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents: 10732
diff changeset
   162
13966
2160abf7cfe7 removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex
paulson
parents: 13964
diff changeset
   163
HOL-Complex: HOL $(OUT)/HOL-Complex
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents: 10732
diff changeset
   164
23247
b99dce43d252 merged Code_Generator.thy into HOL.thy
haftmann
parents: 23243
diff changeset
   165
$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML $(SRC)/Tools/float.ML \
23194
webertj
parents: 23193
diff changeset
   166
  Library/Zorn.thy							\
23454
c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
wenzelm
parents: 23449
diff changeset
   167
  Real/ContNotDenum.thy Real/float_arith.ML Real/Float.thy		\
24103
c13243a11e37 removed obsolete HOL/Real/ROOT.ML;
wenzelm
parents: 24091
diff changeset
   168
  Real/Lubs.thy Real/PReal.thy Real/RComplete.thy 			\
23454
c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
wenzelm
parents: 23449
diff changeset
   169
  Real/Rational.thy Real/Real.thy Real/RealDef.thy Real/RealPow.thy	\
c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
wenzelm
parents: 23449
diff changeset
   170
  Real/RealVector.thy Real/rat_arith.ML Real/real_arith.ML		\
23194
webertj
parents: 23193
diff changeset
   171
  Hyperreal/StarDef.thy Hyperreal/StarClasses.thy			\
webertj
parents: 23193
diff changeset
   172
  Hyperreal/EvenOdd.thy Hyperreal/Fact.thy Hyperreal/HLog.thy		\
webertj
parents: 23193
diff changeset
   173
  Hyperreal/Filter.thy Hyperreal/HSeries.thy Hyperreal/transfer.ML	\
webertj
parents: 23193
diff changeset
   174
  Hyperreal/HLim.thy Hyperreal/HSEQ.thy Hyperreal/HTranscendental.thy	\
webertj
parents: 23193
diff changeset
   175
  Hyperreal/HDeriv.thy Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy	\
webertj
parents: 23193
diff changeset
   176
  Hyperreal/Hyperreal.thy						\
webertj
parents: 23193
diff changeset
   177
  Hyperreal/Integration.thy Hyperreal/Lim.thy Hyperreal/Log.thy		\
webertj
parents: 23193
diff changeset
   178
  Hyperreal/Ln.thy Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy	\
webertj
parents: 23193
diff changeset
   179
  Hyperreal/NSA.thy Hyperreal/NthRoot.thy Hyperreal/Poly.thy		\
webertj
parents: 23193
diff changeset
   180
  Hyperreal/SEQ.thy Hyperreal/Series.thy Hyperreal/Star.thy		\
webertj
parents: 23193
diff changeset
   181
  Hyperreal/Taylor.thy Hyperreal/FrechetDeriv.thy Hyperreal/Deriv.thy	\
webertj
parents: 23193
diff changeset
   182
  Hyperreal/Transcendental.thy Hyperreal/hypreal_arith.ML		\
webertj
parents: 23193
diff changeset
   183
  Complex/Complex_Main.thy Complex/CLim.thy				\
webertj
parents: 23193
diff changeset
   184
  Complex/CStar.thy Complex/Complex.thy Complex/NSCA.thy		\
webertj
parents: 23193
diff changeset
   185
  Complex/NSComplex.thy							\
22897
c714f6d0a8d7 removed Complex/ComplexBin.thy;
wenzelm
parents: 22839
diff changeset
   186
  Complex/document/root.tex Library/Infinite_Set.thy Library/Parity.thy
15057
b1a368d93c50 added Complex/root
nipkow
parents: 15037
diff changeset
   187
	@cd Complex; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Complex
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents: 10732
diff changeset
   188
7395
66a3d3bb28e4 clean: include HOL-Real-ex;
wenzelm
parents: 7393
diff changeset
   189
13961
233dd3bb2390 new directory Complex
paulson
parents: 13949
diff changeset
   190
## HOL-Complex-ex
7392
4137c951b36b new directory HOL/Real/ex of real examples
paulson
parents: 7383
diff changeset
   191
13961
233dd3bb2390 new directory Complex
paulson
parents: 13949
diff changeset
   192
HOL-Complex-ex: HOL-Complex $(LOG)/HOL-Complex-ex.gz
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents: 7513
diff changeset
   193
13961
233dd3bb2390 new directory Complex
paulson
parents: 13949
diff changeset
   194
$(LOG)/HOL-Complex-ex.gz: $(OUT)/HOL-Complex Library/Primes.thy \
233dd3bb2390 new directory Complex
paulson
parents: 13949
diff changeset
   195
  Complex/ex/ROOT.ML Complex/ex/document/root.tex \
23194
webertj
parents: 23193
diff changeset
   196
  Complex/ex/BigO_Complex.thy Complex/ex/BinEx.thy \
23265
a6992b91fdde Added two examples in Complex/ex :Reflected QE for linear real arith and QE for mixed integer real linear arithmetic
chaieb
parents: 23252
diff changeset
   197
  Complex/ex/NSPrimes.thy Complex/ex/Sqrt.thy Complex/ex/Sqrt_Script.thy \
a6992b91fdde Added two examples in Complex/ex :Reflected QE for linear real arith and QE for mixed integer real linear arithmetic
chaieb
parents: 23252
diff changeset
   198
  Complex/ex/MIR.thy Complex/ex/mirtac.ML Complex/ex/mireif.ML \
a6992b91fdde Added two examples in Complex/ex :Reflected QE for linear real arith and QE for mixed integer real linear arithmetic
chaieb
parents: 23252
diff changeset
   199
  Complex/ex/ReflectedFerrack.thy Complex/ex/linreif.ML Complex/ex/linrtac.ML
13961
233dd3bb2390 new directory Complex
paulson
parents: 13949
diff changeset
   200
	@cd Complex; $(ISATOOL) usedir $(OUT)/HOL-Complex ex
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents: 7513
diff changeset
   201
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents: 7513
diff changeset
   202
10255
bb66874b4750 added HOL/Library, rearranged several files;
wenzelm
parents: 10214
diff changeset
   203
## HOL-Library
bb66874b4750 added HOL/Library, rearranged several files;
wenzelm
parents: 10214
diff changeset
   204
bb66874b4750 added HOL/Library, rearranged several files;
wenzelm
parents: 10214
diff changeset
   205
HOL-Library: HOL $(LOG)/HOL-Library.gz
bb66874b4750 added HOL/Library, rearranged several files;
wenzelm
parents: 10214
diff changeset
   206
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents: 19499
diff changeset
   207
$(LOG)/HOL-Library.gz: $(OUT)/HOL \
19944
60e0cbeae3d8 Introduction of Ramsey's theorem
paulson
parents: 19839
diff changeset
   208
  Library/SetsAndFunctions.thy Library/BigO.thy Library/Ramsey.thy \
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents: 23772
diff changeset
   209
  Library/Efficient_Nat.thy Library/Executable_Set.thy \
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents: 23772
diff changeset
   210
  Library/Executable_Rat.thy Library/Executable_Real.thy \
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents: 23772
diff changeset
   211
  Library/ML_Int.thy Library/ML_String.thy Library/Infinite_Set.thy \
23192
ec73b9707d48 Moved list comprehension into List
nipkow
parents: 23172
diff changeset
   212
  Library/FuncSet.thy Library/Library.thy \
23194
webertj
parents: 23193
diff changeset
   213
  Library/List_Prefix.thy Library/State_Monad.thy Library/Multiset.thy \
webertj
parents: 23193
diff changeset
   214
  Library/NatPair.thy \
14265
95b42e69436c HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents: 14264
diff changeset
   215
  Library/Permutation.thy Library/Primes.thy Library/Quotient.thy \
23005
914a1de067b6 dropped word_setup.ML
haftmann
parents: 23003
diff changeset
   216
  Library/Nat_Infinity.thy Library/Word.thy \
11349
fcb507c945c3 added Library/Nat_Infinity.thy and Library/Continuity.thy
oheimb
parents: 11287
diff changeset
   217
  Library/README.html Library/Continuity.thy \
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14355
diff changeset
   218
  Library/Nested_Environment.thy Library/Zorn.thy\
12816
668073849ca9 fixed document setup of HOL-Library;
wenzelm
parents: 12793
diff changeset
   219
  Library/Library/ROOT.ML Library/Library/document/root.tex \
15731
29ae73d8a84e Removed dir Orderings in Library
nipkow
parents: 15697
diff changeset
   220
  Library/Library/document/root.bib Library/While_Combinator.thy \
22799
ed7d53db2170 moved code generation pretty integers and characters to separate theories
haftmann
parents: 22784
diff changeset
   221
  Library/Product_ord.thy Library/Char_nat.thy Library/Char_ord.thy \
18397
2d94eb7ff17f added HOL/Library/Coinductive_List.thy;
wenzelm
parents: 18005
diff changeset
   222
  Library/List_lexord.thy Library/Commutative_Ring.thy Library/comm_ring.ML \
21256
47195501ecf7 moved theories Parity, GCD, Binomial to Library;
wenzelm
parents: 21254
diff changeset
   223
  Library/Coinductive_List.thy Library/AssocList.thy \
22359
94a794672c8b Added formalization of size-change principle (experimental).
krauss
parents: 22327
diff changeset
   224
  Library/Parity.thy Library/GCD.thy Library/Binomial.thy \
94a794672c8b Added formalization of size-change principle (experimental).
krauss
parents: 22327
diff changeset
   225
  Library/Graphs.thy Library/Kleene_Algebras.thy Library/SCT_Misc.thy \
23194
webertj
parents: 23193
diff changeset
   226
  Library/SCT_Definition.thy Library/SCT_Theorem.thy \
webertj
parents: 23193
diff changeset
   227
  Library/SCT_Interpretation.thy \
22359
94a794672c8b Added formalization of size-change principle (experimental).
krauss
parents: 22327
diff changeset
   228
  Library/SCT_Implementation.thy Library/Size_Change_Termination.thy \
22517
2f4c97414746 cleaned up Library( and ex/
haftmann
parents: 22505
diff changeset
   229
  Library/SCT_Examples.thy Library/sct.ML \
24332
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents: 24326
diff changeset
   230
  Library/Pure_term.thy Library/Eval.thy Library/Eval_Witness.thy \
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents: 24326
diff changeset
   231
  Library/Pretty_Int.thy \
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents: 24326
diff changeset
   232
  Library/Pretty_Char.thy Library/Pretty_Char_chr.thy Library/Abstract_Rat.thy\
e3a2b75b1cf9 boolean algebras as locales and numbers as types by Brian Huffman
kleing
parents: 24326
diff changeset
   233
  Library/Numeral_Type.thy Library/Boolean_Algebra.thy
11398
d7711be8c3a9 Library/ROOT.ML moved to Library/Library/ROOT.ML to avoid accidential
wenzelm
parents: 11394
diff changeset
   234
	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
10255
bb66874b4750 added HOL/Library, rearranged several files;
wenzelm
parents: 10214
diff changeset
   235
bb66874b4750 added HOL/Library, rearranged several files;
wenzelm
parents: 10214
diff changeset
   236
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   237
## HOL-Subst
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   238
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   239
HOL-Subst: HOL $(LOG)/HOL-Subst.gz
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   240
15635
8408a06590a6 converted HOL-Subst to tactic scripts
paulson
parents: 15622
diff changeset
   241
$(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.thy \
8408a06590a6 converted HOL-Subst to tactic scripts
paulson
parents: 15622
diff changeset
   242
  Subst/ROOT.ML Subst/Subst.thy Subst/UTerm.thy Subst/Unifier.thy \
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   243
  Subst/Unify.thy
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   244
	@$(ISATOOL) usedir $(OUT)/HOL Subst
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   245
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   246
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   247
## HOL-Induct
2473
3eb12c85846c minor tuning;
wenzelm
parents: 2448
diff changeset
   248
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   249
HOL-Induct: HOL $(LOG)/HOL-Induct.gz
3125
3f0ab2c306f7 Moved induction examples to directory Induct
paulson
parents: 3118
diff changeset
   250
10255
bb66874b4750 added HOL/Library, rearranged several files;
wenzelm
parents: 10214
diff changeset
   251
$(LOG)/HOL-Induct.gz: $(OUT)/HOL \
13075
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 13059
diff changeset
   252
  Induct/Com.thy Induct/Comb.thy Induct/LFilter.thy \
d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar
paulson
parents: 13059
diff changeset
   253
  Induct/LList.thy Induct/Mutil.thy Induct/Ordinals.thy \
15172
73069e033a0b new example of a quotiented nested data type
paulson
parents: 15150
diff changeset
   254
  Induct/PropLog.thy Induct/QuoNestedDataType.thy Induct/QuoDataType.thy\
73069e033a0b new example of a quotiented nested data type
paulson
parents: 15150
diff changeset
   255
  Induct/ROOT.ML \
13079
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 13075
diff changeset
   256
  Induct/Sexp.thy Induct/Sigma_Algebra.thy \
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts
paulson
parents: 13075
diff changeset
   257
  Induct/SList.thy Induct/ABexp.thy Induct/Term.thy \
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 11026
diff changeset
   258
  Induct/Tree.thy Induct/document/root.tex
3125
3f0ab2c306f7 Moved induction examples to directory Induct
paulson
parents: 3118
diff changeset
   259
	@$(ISATOOL) usedir $(OUT)/HOL Induct
3f0ab2c306f7 Moved induction examples to directory Induct
paulson
parents: 3118
diff changeset
   260
3f0ab2c306f7 Moved induction examples to directory Induct
paulson
parents: 3118
diff changeset
   261
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   262
## HOL-IMP
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   263
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   264
HOL-IMP: HOL $(LOG)/HOL-IMP.gz
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   265
13129
bb448fb75191 added dep on IMP/Compiler0
nipkow
parents: 13117
diff changeset
   266
$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Compiler0.thy IMP/Compiler.thy \
12432
90b0fc84f8d9 HOL/IMP converted to Isar
kleing
parents: 12410
diff changeset
   267
  IMP/Denotation.thy IMP/Expr.thy IMP/Hoare.thy \
90b0fc84f8d9 HOL/IMP converted to Isar
kleing
parents: 12410
diff changeset
   268
  IMP/Natural.thy IMP/Examples.thy \
90b0fc84f8d9 HOL/IMP converted to Isar
kleing
parents: 12410
diff changeset
   269
  IMP/Transition.thy IMP/VC.thy IMP/ROOT.ML IMP/document/root.tex \
90b0fc84f8d9 HOL/IMP converted to Isar
kleing
parents: 12410
diff changeset
   270
  IMP/document/root.bib
12548
9d247ad51c81 HOL/IMP: include session graph;
wenzelm
parents: 12521
diff changeset
   271
	@$(ISATOOL) usedir -g true $(OUT)/HOL IMP
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   272
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   273
8179
6a0b1037bab3 added forgotten rules to make IMPP
oheimb
parents: 8177
diff changeset
   274
## HOL-IMPP
6a0b1037bab3 added forgotten rules to make IMPP
oheimb
parents: 8177
diff changeset
   275
6a0b1037bab3 added forgotten rules to make IMPP
oheimb
parents: 8177
diff changeset
   276
HOL-IMPP: HOL $(LOG)/HOL-IMPP.gz
6a0b1037bab3 added forgotten rules to make IMPP
oheimb
parents: 8177
diff changeset
   277
19803
aa2581752afb removed obsolete ML files;
wenzelm
parents: 19802
diff changeset
   278
$(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy \
aa2581752afb removed obsolete ML files;
wenzelm
parents: 19802
diff changeset
   279
  IMPP/Natural.thy IMPP/Hoare.thy IMPP/Misc.thy IMPP/EvenOdd.thy
8179
6a0b1037bab3 added forgotten rules to make IMPP
oheimb
parents: 8177
diff changeset
   280
	@$(ISATOOL) usedir $(OUT)/HOL IMPP
6a0b1037bab3 added forgotten rules to make IMPP
oheimb
parents: 8177
diff changeset
   281
6a0b1037bab3 added forgotten rules to make IMPP
oheimb
parents: 8177
diff changeset
   282
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   283
## HOL-Complex-Import
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   284
19097
2fc1a6da9366 removed Import/lazy_scan.ML;
wenzelm
parents: 19085
diff changeset
   285
IMPORTER_FILES = Import/lazy_seq.ML Import/proof_kernel.ML Import/replay.ML \
20610
09ef37366a31 moved Import/susp.ML to Pure/General;
wenzelm
parents: 20598
diff changeset
   286
  Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   287
  Import/HOL4Syntax.thy Import/HOL4Compat.thy Import/import_syntax.ML \
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   288
  Import/hol4rews.ML Import/import_package.ML Import/ROOT.ML
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   289
17323
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight
obua
parents: 17308
diff changeset
   290
IMPORTER_HOLLIGHT_FILES = Import/proof_kernel.ML Import/replay.ML \
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight
obua
parents: 17308
diff changeset
   291
  Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight
obua
parents: 17308
diff changeset
   292
  Import/HOL4Syntax.thy Import/HOLLightCompat.thy Import/import_syntax.ML \
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight
obua
parents: 17308
diff changeset
   293
  Import/hol4rews.ML Import/import_package.ML Import/ROOT.ML
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight
obua
parents: 17308
diff changeset
   294
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   295
HOL-Complex-Import: HOL-Complex $(LOG)/HOL-Complex-Import.gz
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   296
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   297
$(LOG)/HOL-Complex-Import.gz: $(OUT)/HOL-Complex $(IMPORTER_FILES)
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   298
	@$(ISATOOL) usedir $(OUT)/HOL-Complex Import
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   299
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   300
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   301
## HOL-Complex-Generate-HOL
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   302
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   303
HOL-Complex-Generate-HOL: HOL-Complex $(LOG)/HOL-Complex-Generate-HOL.gz
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   304
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   305
$(LOG)/HOL-Complex-Generate-HOL.gz: $(OUT)/HOL-Complex $(IMPORTER_FILES)  \
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   306
  Import/Generate-HOL/GenHOL4Base.thy Import/Generate-HOL/GenHOL4Prob.thy \
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   307
  Import/Generate-HOL/GenHOL4Real.thy Import/Generate-HOL/GenHOL4Vec.thy  \
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   308
  Import/Generate-HOL/GenHOL4Word32.thy Import/Generate-HOL/ROOT.ML
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   309
	@cd Import; $(ISATOOL) usedir $(OUT)/HOL-Complex Generate-HOL
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   310
17460
7780d953598c generate: added HOL-Complex-Generate-HOLLight;
wenzelm
parents: 17430
diff changeset
   311
7780d953598c generate: added HOL-Complex-Generate-HOLLight;
wenzelm
parents: 17430
diff changeset
   312
## HOL-Complex-Generate-HOLLight
7780d953598c generate: added HOL-Complex-Generate-HOLLight;
wenzelm
parents: 17430
diff changeset
   313
17323
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight
obua
parents: 17308
diff changeset
   314
HOL-Complex-Generate-HOLLight: HOL-Complex $(LOG)/HOL-Complex-Generate-HOLLight.gz
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight
obua
parents: 17308
diff changeset
   315
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight
obua
parents: 17308
diff changeset
   316
$(LOG)/HOL-Complex-Generate-HOLLight.gz: $(OUT)/HOL-Complex $(IMPORTER_HOLLIGHT_FILES)  \
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight
obua
parents: 17308
diff changeset
   317
  Import/Generate-HOLLight/GenHOLLight.thy Import/Generate-HOLLight/ROOT.ML
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight
obua
parents: 17308
diff changeset
   318
	@cd Import; $(ISATOOL) usedir $(OUT)/HOL-Complex Generate-HOLLight
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   319
17460
7780d953598c generate: added HOL-Complex-Generate-HOLLight;
wenzelm
parents: 17430
diff changeset
   320
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   321
## HOL-Import-HOL
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   322
14626
dfb8d2977263 renamed HOL-Import-HOL to HOL4, added to images target
kleing
parents: 14610
diff changeset
   323
HOL4: HOL-Complex $(LOG)/HOL4.gz
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   324
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   325
HOL_IMPORT_FILES = arithmetic.imp bits.imp boolean_sequence.imp bool.imp \
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   326
  bword_arith.imp bword_bitop.imp bword_num.imp combin.imp divides.imp \
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   327
  hrat.imp hreal.imp ind_type.imp lim.imp list.imp marker.imp nets.imp \
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   328
  numeral.imp num.imp one.imp operator.imp option.imp pair.imp poly.imp \
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   329
  powser.imp pred_set.imp prime.imp prim_rec.imp prob_algebra.imp \
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   330
  prob_canon.imp prob_extra.imp prob.imp prob_indep.imp prob_pseudo.imp \
23194
webertj
parents: 23193
diff changeset
   331
  prob_uniform.imp realax.imp real.imp relation.imp res_quan.imp \
webertj
parents: 23193
diff changeset
   332
  rich_list.imp \
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   333
  seq.imp state_transformer.imp sum.imp topology.imp transc.imp word32.imp \
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   334
  word_base.imp word_bitop.imp word_num.imp
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   335
14626
dfb8d2977263 renamed HOL-Import-HOL to HOL4, added to images target
kleing
parents: 14610
diff changeset
   336
$(LOG)/HOL4.gz: $(OUT)/HOL-Complex $(IMPORTER_FILES) \
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   337
  $(HOL_IMPORT_FILES:%=Import/HOL/%) Import/HOL/HOL4Base.thy \
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   338
  Import/HOL/HOL4Prob.thy Import/HOL/HOL4Real.thy Import/HOL/HOL4Vec.thy \
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   339
  Import/HOL/HOL4Word32.thy Import/HOL/HOL4.thy Import/HOL/ROOT.ML
14626
dfb8d2977263 renamed HOL-Import-HOL to HOL4, added to images target
kleing
parents: 14610
diff changeset
   340
	@cd Import/HOL; $(ISATOOL) usedir -b $(OUT)/HOL-Complex HOL4
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   341
17645
940371ea0ff3 added entry for running HOLLight
obua
parents: 17637
diff changeset
   342
HOLLight: HOL-Complex $(LOG)/HOLLight.gz
940371ea0ff3 added entry for running HOLLight
obua
parents: 17637
diff changeset
   343
940371ea0ff3 added entry for running HOLLight
obua
parents: 17637
diff changeset
   344
$(LOG)/HOLLight.gz: $(OUT)/HOL-Complex $(IMPORTER_HOLLIGHT_FILES) \
940371ea0ff3 added entry for running HOLLight
obua
parents: 17637
diff changeset
   345
  Import/HOLLight/hollight.imp Import/HOLLight/HOLLight.thy \
940371ea0ff3 added entry for running HOLLight
obua
parents: 17637
diff changeset
   346
  Import/HOLLight/ROOT.ML
940371ea0ff3 added entry for running HOLLight
obua
parents: 17637
diff changeset
   347
	@cd Import/HOLLight; $(ISATOOL) usedir -b $(OUT)/HOL-Complex HOLLight
940371ea0ff3 added entry for running HOLLight
obua
parents: 17637
diff changeset
   348
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   349
9510
dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied
paulson
parents: 9481
diff changeset
   350
## HOL-NumberTheory
dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied
paulson
parents: 9481
diff changeset
   351
dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied
paulson
parents: 9481
diff changeset
   352
HOL-NumberTheory: HOL $(LOG)/HOL-NumberTheory.gz
dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied
paulson
parents: 9481
diff changeset
   353
dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied
paulson
parents: 9481
diff changeset
   354
$(LOG)/HOL-NumberTheory.gz: $(OUT)/HOL \
11363
a548865b1b6a moved Primes.thy from NumberTheory to Library
paulson
parents: 11362
diff changeset
   355
  Library/Permutation.thy Library/Primes.thy NumberTheory/Fib.thy \
11049
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 11046
diff changeset
   356
  NumberTheory/Factorization.thy NumberTheory/BijectionRel.thy \
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 11046
diff changeset
   357
  NumberTheory/Chinese.thy NumberTheory/EulerFermat.thy \
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 11046
diff changeset
   358
  NumberTheory/IntFact.thy NumberTheory/IntPrimes.thy \
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup;
wenzelm
parents: 11046
diff changeset
   359
  NumberTheory/WilsonBij.thy NumberTheory/WilsonRuss.thy \
13873
f9f49a1ec0f2 quadratic reciprocity files
paulson
parents: 13870
diff changeset
   360
  NumberTheory/Finite2.thy NumberTheory/Int2.thy NumberTheory/EvenOdd.thy\
f9f49a1ec0f2 quadratic reciprocity files
paulson
parents: 13870
diff changeset
   361
  NumberTheory/Residues.thy NumberTheory/Euler.thy NumberTheory/Gauss.thy\
20808
96d413f78870 moved Infinite_Set.thy to Library;
wenzelm
parents: 20787
diff changeset
   362
  NumberTheory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy\
9510
dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied
paulson
parents: 9481
diff changeset
   363
  NumberTheory/ROOT.ML
11850
cdfc3fce577e document graphs for several sessions;
wenzelm
parents: 11837
diff changeset
   364
	@$(ISATOOL) usedir -g true $(OUT)/HOL NumberTheory
9510
dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied
paulson
parents: 9481
diff changeset
   365
dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied
paulson
parents: 9481
diff changeset
   366
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   367
## HOL-Hoare
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   368
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   369
HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   370
19802
c2860c37e574 removed obsolete ML files;
wenzelm
parents: 19801
diff changeset
   371
$(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.thy \
13697
e4db4f06cec1 Hoare.ML -> hoare.ML
nipkow
parents: 13695
diff changeset
   372
  Hoare/Examples.thy Hoare/hoare.ML Hoare/Hoare.thy \
13875
12997e3ddd8d *** empty log message ***
nipkow
parents: 13873
diff changeset
   373
  Hoare/Heap.thy Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy \
12997e3ddd8d *** empty log message ***
nipkow
parents: 13873
diff changeset
   374
  Hoare/ROOT.ML Hoare/ExamplesAbort.thy  Hoare/HeapSyntaxAbort.thy \
14075
ab2e26ae90e3 *** empty log message ***
nipkow
parents: 14070
diff changeset
   375
  Hoare/hoareAbort.ML Hoare/HoareAbort.thy Hoare/SchorrWaite.thy \
19402
742b7934ccfc Hoare(Parallel) dependencies on document/*
nipkow
parents: 19234
diff changeset
   376
  Hoare/Separation.thy Hoare/SepLogHeap.thy \
742b7934ccfc Hoare(Parallel) dependencies on document/*
nipkow
parents: 19234
diff changeset
   377
  Hoare/document/root.tex Hoare/document/root.bib
2826
0b0d9e3bc661 isatool usedir;
wenzelm
parents: 2635
diff changeset
   378
	@$(ISATOOL) usedir $(OUT)/HOL Hoare
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   379
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   380
12996
7ac0a7e306db Completed annonce of HoareParallel
prensani
parents: 12951
diff changeset
   381
## HOL-HoareParallel
7ac0a7e306db Completed annonce of HoareParallel
prensani
parents: 12951
diff changeset
   382
7ac0a7e306db Completed annonce of HoareParallel
prensani
parents: 12951
diff changeset
   383
HOL-HoareParallel: HOL $(LOG)/HOL-HoareParallel.gz
7ac0a7e306db Completed annonce of HoareParallel
prensani
parents: 12951
diff changeset
   384
7ac0a7e306db Completed annonce of HoareParallel
prensani
parents: 12951
diff changeset
   385
$(LOG)/HOL-HoareParallel.gz: $(OUT)/HOL HoareParallel/Gar_Coll.thy \
7ac0a7e306db Completed annonce of HoareParallel
prensani
parents: 12951
diff changeset
   386
  HoareParallel/Graph.thy HoareParallel/Mul_Gar_Coll.thy	   \
7ac0a7e306db Completed annonce of HoareParallel
prensani
parents: 12951
diff changeset
   387
  HoareParallel/OG_Com.thy HoareParallel/OG_Examples.thy	   \
7ac0a7e306db Completed annonce of HoareParallel
prensani
parents: 12951
diff changeset
   388
  HoareParallel/OG_Hoare.thy HoareParallel/OG_Syntax.thy	   \
7ac0a7e306db Completed annonce of HoareParallel
prensani
parents: 12951
diff changeset
   389
  HoareParallel/OG_Tactics.thy HoareParallel/OG_Tran.thy	   \
13019
98f0a09a33c3 Target HoareParallel in IsaMakefile
prensani
parents: 13004
diff changeset
   390
  HoareParallel/Quote_Antiquote.thy                                \
12996
7ac0a7e306db Completed annonce of HoareParallel
prensani
parents: 12951
diff changeset
   391
  HoareParallel/RG_Com.thy HoareParallel/RG_Examples.thy	   \
7ac0a7e306db Completed annonce of HoareParallel
prensani
parents: 12951
diff changeset
   392
  HoareParallel/RG_Hoare.thy HoareParallel/RG_Syntax.thy	   \
7ac0a7e306db Completed annonce of HoareParallel
prensani
parents: 12951
diff changeset
   393
  HoareParallel/RG_Tran.thy HoareParallel/ROOT.ML		   \
19402
742b7934ccfc Hoare(Parallel) dependencies on document/*
nipkow
parents: 19234
diff changeset
   394
  HoareParallel/document/root.tex HoareParallel/document/root.bib
13029
84e4ba7fb033 added HOL-Hyperreal-ex;
wenzelm
parents: 13019
diff changeset
   395
	@$(ISATOOL) usedir -g true $(OUT)/HOL HoareParallel
12996
7ac0a7e306db Completed annonce of HoareParallel
prensani
parents: 12951
diff changeset
   396
7ac0a7e306db Completed annonce of HoareParallel
prensani
parents: 12951
diff changeset
   397
23449
dd874e6a3282 integration of Metis prover
paulson
parents: 23445
diff changeset
   398
## HOL-MetisExamples
dd874e6a3282 integration of Metis prover
paulson
parents: 23445
diff changeset
   399
dd874e6a3282 integration of Metis prover
paulson
parents: 23445
diff changeset
   400
HOL-MetisExamples: HOL $(LOG)/HOL-MetisExamples.gz
dd874e6a3282 integration of Metis prover
paulson
parents: 23445
diff changeset
   401
dd874e6a3282 integration of Metis prover
paulson
parents: 23445
diff changeset
   402
$(LOG)/HOL-MetisExamples.gz: $(OUT)/HOL \
dd874e6a3282 integration of Metis prover
paulson
parents: 23445
diff changeset
   403
  MetisExamples/ROOT.ML \
dd874e6a3282 integration of Metis prover
paulson
parents: 23445
diff changeset
   404
  MetisExamples/Abstraction.thy MetisExamples/BigO.thy MetisExamples/BT.thy \
dd874e6a3282 integration of Metis prover
paulson
parents: 23445
diff changeset
   405
  MetisExamples/Message.thy MetisExamples/Tarski.thy MetisExamples/TransClosure.thy \
dd874e6a3282 integration of Metis prover
paulson
parents: 23445
diff changeset
   406
  MetisExamples/set.thy
23454
c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
wenzelm
parents: 23449
diff changeset
   407
	@$(ISATOOL) usedir $(OUT)/HOL MetisExamples
23449
dd874e6a3282 integration of Metis prover
paulson
parents: 23445
diff changeset
   408
dd874e6a3282 integration of Metis prover
paulson
parents: 23445
diff changeset
   409
7999
7acf6eb8eec1 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents: 7985
diff changeset
   410
## HOL-Algebra
7acf6eb8eec1 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents: 7985
diff changeset
   411
7acf6eb8eec1 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents: 7985
diff changeset
   412
HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz
7acf6eb8eec1 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents: 7985
diff changeset
   413
21423
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21317
diff changeset
   414
$(LOG)/HOL-Algebra.gz: $(OUT)/HOL Algebra/ROOT.ML Library/Primes.thy	\
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21317
diff changeset
   415
  Library/FuncSet.thy Algebra/AbelCoset.thy Algebra/Bij.thy		\
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21317
diff changeset
   416
  Algebra/Coset.thy Algebra/Exponent.thy Algebra/FiniteProduct.thy	\
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21317
diff changeset
   417
  Algebra/Group.thy Algebra/Ideal.thy Algebra/IntRing.thy		\
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21317
diff changeset
   418
  Algebra/Lattice.thy Algebra/Module.thy Algebra/QuotRing.thy		\
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21317
diff changeset
   419
  Algebra/Ring.thy Algebra/RingHom.thy Algebra/Sylow.thy		\
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21317
diff changeset
   420
  Algebra/UnivPoly.thy Algebra/abstract/Abstract.thy			\
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21317
diff changeset
   421
  Algebra/abstract/Factor.thy Algebra/abstract/Field.thy		\
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21317
diff changeset
   422
  Algebra/abstract/Ideal2.thy Algebra/abstract/PID.thy			\
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21317
diff changeset
   423
  Algebra/abstract/Ring2.thy Algebra/abstract/RingHomo.thy		\
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21317
diff changeset
   424
  Algebra/document/root.tex Algebra/poly/LongDiv.thy			\
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21317
diff changeset
   425
  Algebra/poly/PolyHomo.thy Algebra/poly/Polynomial.thy			\
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts;
wenzelm
parents: 21317
diff changeset
   426
  Algebra/poly/UnivPoly2.thy Algebra/ringsimp.ML
14578
1f3f7e58b195 session graph;
wenzelm
parents: 14569
diff changeset
   427
	@cd Algebra; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Algebra
7999
7acf6eb8eec1 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents: 7985
diff changeset
   428
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   429
## HOL-Auth
3819
5a6a6f18b109 added TLA stuff;
wenzelm
parents: 3616
diff changeset
   430
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   431
HOL-Auth: HOL $(LOG)/HOL-Auth.gz
3819
5a6a6f18b109 added TLA stuff;
wenzelm
parents: 3616
diff changeset
   432
14132
4d682b249437 new theory Library/NatPair
paulson
parents: 14115
diff changeset
   433
$(LOG)/HOL-Auth.gz: $(OUT)/HOL Library/NatPair.thy \
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13923
diff changeset
   434
  Auth/CertifiedEmail.thy Auth/Event.thy \
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13923
diff changeset
   435
  Auth/Message.thy Auth/NS_Public.thy Auth/NS_Public_Bad.thy \
23194
webertj
parents: 23193
diff changeset
   436
  Auth/NS_Shared.thy Auth/OtwayRees.thy Auth/OtwayReesBella.thy \
webertj
parents: 23193
diff changeset
   437
  Auth/OtwayRees_AN.thy \
13923
019342d03d81 Auth: certified email protocol
paulson
parents: 13908
diff changeset
   438
  Auth/OtwayRees_Bad.thy Auth/Public.thy Auth/ROOT.ML \
13926
6e62e5357a10 converting more HOL-Auth to new-style theories
paulson
parents: 13923
diff changeset
   439
  Auth/Recur.thy Auth/Shared.thy \
23194
webertj
parents: 23193
diff changeset
   440
  Auth/TLS.thy Auth/WooLam.thy Auth/Kerberos_BAN.thy \
webertj
parents: 23193
diff changeset
   441
  Auth/Kerberos_BAN_Gets.thy \
18886
9f27383426db new and updated protocol proofs by Giamp Bella
paulson
parents: 18793
diff changeset
   442
  Auth/KerberosIV.thy Auth/KerberosIV_Gets.thy Auth/KerberosV.thy \
13508
890d736b93a5 Frederic Blanqui's new "guard" examples
paulson
parents: 13481
diff changeset
   443
  Auth/Yahalom.thy Auth/Yahalom2.thy Auth/Yahalom_Bad.thy \
14145
2e31b8cc8788 ZhouGollmann: new example (fair non-repudiation protocol)
paulson
parents: 14132
diff changeset
   444
  Auth/ZhouGollmann.thy \
13508
890d736b93a5 Frederic Blanqui's new "guard" examples
paulson
parents: 13481
diff changeset
   445
  Auth/Guard/Analz.thy Auth/Guard/Extensions.thy Auth/Guard/GuardK.thy \
890d736b93a5 Frederic Blanqui's new "guard" examples
paulson
parents: 13481
diff changeset
   446
  Auth/Guard/Guard_Public.thy Auth/Guard/Guard_Shared.thy \
890d736b93a5 Frederic Blanqui's new "guard" examples
paulson
parents: 13481
diff changeset
   447
  Auth/Guard/Guard.thy Auth/Guard/List_Msg.thy \
17394
a8c9ed3f9818 renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents: 17384
diff changeset
   448
  Auth/Guard/Guard_NS_Public.thy Auth/Guard/Guard_OtwayRees.thy \
13508
890d736b93a5 Frederic Blanqui's new "guard" examples
paulson
parents: 13481
diff changeset
   449
  Auth/Guard/P1.thy Auth/Guard/P2.thy \
23194
webertj
parents: 23193
diff changeset
   450
  Auth/Guard/Proto.thy Auth/Guard/Guard_Yahalom.thy \
webertj
parents: 23193
diff changeset
   451
  Auth/Smartcard/EventSC.thy Auth/Smartcard/ShoupRubinBella.thy \
webertj
parents: 23193
diff changeset
   452
  Auth/Smartcard/ShoupRubin.thy Auth/Smartcard/Smartcard.thy \
23164
69e55066dbca moved Integ files to canonical place;
wenzelm
parents: 23150
diff changeset
   453
  Auth/document/root.tex
13964
bfca18e9ab72 fixed missing -g true for HOL-Auth
kleing
parents: 13961
diff changeset
   454
	@$(ISATOOL) usedir -g true $(OUT)/HOL Auth
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   455
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   456
4777
379f32b0ae40 New target HOL-UNITY
paulson
parents: 4729
diff changeset
   457
## HOL-UNITY
379f32b0ae40 New target HOL-UNITY
paulson
parents: 4729
diff changeset
   458
379f32b0ae40 New target HOL-UNITY
paulson
parents: 4729
diff changeset
   459
HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz
379f32b0ae40 New target HOL-UNITY
paulson
parents: 4729
diff changeset
   460
10787
f42353afd6d3 new UNITY examples by Sidi Ehmety
paulson
parents: 10772
diff changeset
   461
$(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 13787
diff changeset
   462
  UNITY/UNITY_Main.thy UNITY/UNITY_tactics.ML \
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 13796
diff changeset
   463
  UNITY/Comp.thy UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy \
13853
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents: 13851
diff changeset
   464
  UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy UNITY/Guar.thy\
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents: 13851
diff changeset
   465
  UNITY/Lift_prog.thy UNITY/ListOrder.thy UNITY/ProgressSets.thy\
89131afa9f01 New theory ProgressSets. Definition of closure sets
paulson
parents: 13851
diff changeset
   466
  UNITY/PPROD.thy  UNITY/Project.thy UNITY/Rename.thy UNITY/Transformers.thy\
13797
baefae13ad37 conversion of UNITY theories to new-style
paulson
parents: 13796
diff changeset
   467
  UNITY/SubstAx.thy UNITY/UNITY.thy UNITY/Union.thy UNITY/WFair.thy \
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 13787
diff changeset
   468
  UNITY/Simple/Channel.thy UNITY/Simple/Common.thy  \
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 13787
diff changeset
   469
  UNITY/Simple/Deadlock.thy UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy  \
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
   470
  UNITY/Simple/NSP_Bad.thy UNITY/Simple/Network.thy\
13790
8d7e9fce8c50 converting UNITY to new-style theories
paulson
parents: 13787
diff changeset
   471
  UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy UNITY/Simple/Token.thy\
21632
e7c1f1a77d18 converted legacy ML script;
wenzelm
parents: 21624
diff changeset
   472
  UNITY/Comp/Alloc.thy UNITY/Comp/AllocBase.thy UNITY/Comp/AllocImpl.thy \
e7c1f1a77d18 converted legacy ML script;
wenzelm
parents: 21624
diff changeset
   473
  UNITY/Comp/Client.thy UNITY/Comp/Counter.thy UNITY/Comp/Counterc.thy \
e7c1f1a77d18 converted legacy ML script;
wenzelm
parents: 21624
diff changeset
   474
  UNITY/Comp/Handshake.thy UNITY/Comp/PriorityAux.thy \
14087
cb07c3948668 Conversion of UNITY/Comp/Priority.thy to a linear Isar script
paulson
parents: 14075
diff changeset
   475
  UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \
14150
9a23e4eb5eb3 A document for UNITY
paulson
parents: 14145
diff changeset
   476
  UNITY/Comp/TimerArray.thy\
9a23e4eb5eb3 A document for UNITY
paulson
parents: 14145
diff changeset
   477
  UNITY/document/root.tex 
9a23e4eb5eb3 A document for UNITY
paulson
parents: 14145
diff changeset
   478
	@$(ISATOOL) usedir -g true $(OUT)/HOL UNITY
4777
379f32b0ae40 New target HOL-UNITY
paulson
parents: 4729
diff changeset
   479
379f32b0ae40 New target HOL-UNITY
paulson
parents: 4729
diff changeset
   480
10966
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
   481
## HOL-Unix
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
   482
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
   483
HOL-Unix: HOL $(LOG)/HOL-Unix.gz
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
   484
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
   485
$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy \
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
   486
  Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy \
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
   487
  Unix/document/root.bib Unix/document/root.tex
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
   488
	@$(ISATOOL) usedir $(OUT)/HOL Unix
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
   489
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents: 19192
diff changeset
   490
## HOL-ZF
778507520684 Added HOL-ZF to Isabelle.
obua
parents: 19192
diff changeset
   491
778507520684 Added HOL-ZF to Isabelle.
obua
parents: 19192
diff changeset
   492
HOL-ZF: HOL $(LOG)/HOL-ZF.gz
778507520684 Added HOL-ZF to Isabelle.
obua
parents: 19192
diff changeset
   493
778507520684 Added HOL-ZF to Isabelle.
obua
parents: 19192
diff changeset
   494
$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML  \
778507520684 Added HOL-ZF to Isabelle.
obua
parents: 19192
diff changeset
   495
  ZF/Helper.thy ZF/LProd.thy ZF/HOLZF.thy \
778507520684 Added HOL-ZF to Isabelle.
obua
parents: 19192
diff changeset
   496
  ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex
778507520684 Added HOL-ZF to Isabelle.
obua
parents: 19192
diff changeset
   497
	@$(ISATOOL) usedir $(OUT)/HOL ZF
10966
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
   498
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   499
## HOL-Modelcheck
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   500
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   501
HOL-Modelcheck: HOL $(LOG)/HOL-Modelcheck.gz
3218
44f01b718eab added Modelcheck example;
mueller
parents: 3195
diff changeset
   502
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   503
$(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL Modelcheck/CTL.thy \
22819
a7b425bb668c removed legacy ML files;
wenzelm
parents: 22799
diff changeset
   504
  Modelcheck/EindhovenExample.thy Modelcheck/EindhovenSyn.thy \
a7b425bb668c removed legacy ML files;
wenzelm
parents: 22799
diff changeset
   505
  Modelcheck/MuCalculus.thy Modelcheck/MuckeExample1.thy \
a7b425bb668c removed legacy ML files;
wenzelm
parents: 22799
diff changeset
   506
  Modelcheck/MuckeExample2.thy Modelcheck/MuckeSyn.thy \
a7b425bb668c removed legacy ML files;
wenzelm
parents: 22799
diff changeset
   507
  Modelcheck/ROOT.ML Modelcheck/mucke_oracle.ML
3218
44f01b718eab added Modelcheck example;
mueller
parents: 3195
diff changeset
   508
	@$(ISATOOL) usedir $(OUT)/HOL Modelcheck
44f01b718eab added Modelcheck example;
mueller
parents: 3195
diff changeset
   509
44f01b718eab added Modelcheck example;
mueller
parents: 3195
diff changeset
   510
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   511
## HOL-Lambda
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   512
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   513
HOL-Lambda: HOL $(LOG)/HOL-Lambda.gz
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   514
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents: 19499
diff changeset
   515
$(LOG)/HOL-Lambda.gz: $(OUT)/HOL \
23194
webertj
parents: 23193
diff changeset
   516
  Lambda/Commutation.thy Lambda/Eta.thy Lambda/InductTermi.thy \
webertj
parents: 23193
diff changeset
   517
  Lambda/Lambda.thy \
9771
54c6a2c6e569 converted Lambda scripts;
wenzelm
parents: 9762
diff changeset
   518
  Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy \
14070
86c56794b641 Added new theories StrongNorm and WeakNorm to Lambda example.
berghofe
parents: 14044
diff changeset
   519
  Lambda/ParRed.thy Lambda/StrongNorm.thy Lambda/Type.thy \
86c56794b641 Added new theories StrongNorm and WeakNorm to Lambda example.
berghofe
parents: 14044
diff changeset
   520
  Lambda/WeakNorm.thy Lambda/ROOT.ML \
86c56794b641 Added new theories StrongNorm and WeakNorm to Lambda example.
berghofe
parents: 14044
diff changeset
   521
  Lambda/document/root.bib Lambda/document/root.tex
22100
33d7468302bb HOL-Lambda: usedir -m no_brackets;
wenzelm
parents: 22077
diff changeset
   522
	@$(ISATOOL) usedir -g true -m no_brackets $(OUT)/HOL Lambda
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   523
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   524
9015
8006e9009621 added HOL/Prolog
oheimb
parents: 8958
diff changeset
   525
## HOL-Prolog
8006e9009621 added HOL/Prolog
oheimb
parents: 8958
diff changeset
   526
8006e9009621 added HOL/Prolog
oheimb
parents: 8958
diff changeset
   527
HOL-Prolog: HOL $(LOG)/HOL-Prolog.gz
8006e9009621 added HOL/Prolog
oheimb
parents: 8958
diff changeset
   528
23194
webertj
parents: 23193
diff changeset
   529
$(LOG)/HOL-Prolog.gz: $(OUT)/HOL Prolog/ROOT.ML Prolog/prolog.ML \
webertj
parents: 23193
diff changeset
   530
  Prolog/HOHH.thy \
21425
c11ab38b78a7 HOL-Prolog: converted legacy ML scripts;
wenzelm
parents: 21423
diff changeset
   531
  Prolog/Test.thy Prolog/Func.thy Prolog/Type.thy
9015
8006e9009621 added HOL/Prolog
oheimb
parents: 8958
diff changeset
   532
	@$(ISATOOL) usedir $(OUT)/HOL Prolog
8006e9009621 added HOL/Prolog
oheimb
parents: 8958
diff changeset
   533
8006e9009621 added HOL/Prolog
oheimb
parents: 8958
diff changeset
   534
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   535
## HOL-W0
2527
0ba3755ce398 Added W0 and modified MiniML.
nipkow
parents: 2473
diff changeset
   536
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   537
HOL-W0: HOL $(LOG)/HOL-W0.gz
2527
0ba3755ce398 Added W0 and modified MiniML.
nipkow
parents: 2473
diff changeset
   538
12946
75447c743810 Isar_examples/W_correct moved to W0;
wenzelm
parents: 12918
diff changeset
   539
$(LOG)/HOL-W0.gz: $(OUT)/HOL W0/ROOT.ML W0/W0.thy W0/document/root.tex
2826
0b0d9e3bc661 isatool usedir;
wenzelm
parents: 2635
diff changeset
   540
	@$(ISATOOL) usedir $(OUT)/HOL W0
2527
0ba3755ce398 Added W0 and modified MiniML.
nipkow
parents: 2473
diff changeset
   541
0ba3755ce398 Added W0 and modified MiniML.
nipkow
parents: 2473
diff changeset
   542
8012
bbdf3c51c3b8 Added MicroJava
nipkow
parents: 8008
diff changeset
   543
## HOL-MicroJava
bbdf3c51c3b8 Added MicroJava
nipkow
parents: 8008
diff changeset
   544
bbdf3c51c3b8 Added MicroJava
nipkow
parents: 8008
diff changeset
   545
HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
bbdf3c51c3b8 Added MicroJava
nipkow
parents: 8008
diff changeset
   546
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents: 23772
diff changeset
   547
$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL Library/Executable_Set.thy \
17637
409983bbaf00 Added ExecutableSet and Taylor.
berghofe
parents: 17618
diff changeset
   548
  MicroJava/ROOT.ML \
13672
b95d12325b51 Added compiler
streckem
parents: 13589
diff changeset
   549
  MicroJava/Comp/AuxLemmas.thy \
b95d12325b51 Added compiler
streckem
parents: 13589
diff changeset
   550
  MicroJava/Comp/CorrComp.thy \
b95d12325b51 Added compiler
streckem
parents: 13589
diff changeset
   551
  MicroJava/Comp/CorrCompTp.thy \
b95d12325b51 Added compiler
streckem
parents: 13589
diff changeset
   552
  MicroJava/Comp/DefsComp.thy \
b95d12325b51 Added compiler
streckem
parents: 13589
diff changeset
   553
  MicroJava/Comp/Index.thy \
b95d12325b51 Added compiler
streckem
parents: 13589
diff changeset
   554
  MicroJava/Comp/LemmasComp.thy \
b95d12325b51 Added compiler
streckem
parents: 13589
diff changeset
   555
  MicroJava/Comp/NatCanonify.thy \
b95d12325b51 Added compiler
streckem
parents: 13589
diff changeset
   556
  MicroJava/Comp/TranslComp.thy \
b95d12325b51 Added compiler
streckem
parents: 13589
diff changeset
   557
  MicroJava/Comp/TranslCompTp.thy \
b95d12325b51 Added compiler
streckem
parents: 13589
diff changeset
   558
  MicroJava/Comp/TypeInf.thy \
11026
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 11024
diff changeset
   559
  MicroJava/J/Conform.thy MicroJava/J/Eval.thy MicroJava/J/JBasis.thy \
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 11024
diff changeset
   560
  MicroJava/J/JTypeSafe.thy MicroJava/J/Decl.thy MicroJava/J/State.thy \
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 11024
diff changeset
   561
  MicroJava/J/Term.thy MicroJava/J/Type.thy MicroJava/J/TypeRel.thy \
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 11024
diff changeset
   562
  MicroJava/J/WellForm.thy MicroJava/J/Value.thy \
a50365d21144 converted to Isar, simplifying recursion on class hierarchy
oheimb
parents: 11024
diff changeset
   563
  MicroJava/J/WellType.thy MicroJava/J/Example.thy \
12438
afd41635dcf9 Added new files (code generator and examples).
berghofe
parents: 12432
diff changeset
   564
  MicroJava/J/JListExample.thy \
9381
a0491eed2270 MicroJava structure changed
kleing
parents: 9353
diff changeset
   565
  MicroJava/JVM/JVMExec.thy MicroJava/JVM/JVMInstructions.thy\
a0491eed2270 MicroJava structure changed
kleing
parents: 9353
diff changeset
   566
  MicroJava/JVM/JVMState.thy MicroJava/JVM/JVMExecInstr.thy\
12521
b1ebe0320d79 MicroJava exception merge
kleing
parents: 12438
diff changeset
   567
  MicroJava/JVM/JVMListExample.thy MicroJava/JVM/JVMExceptions.thy \
11228
5516e806dc09 MicroJava/BV dependencies incomplete
nipkow
parents: 11220
diff changeset
   568
  MicroJava/BV/BVSpec.thy MicroJava/BV/BVSpecTypeSafe.thy \
5516e806dc09 MicroJava/BV dependencies incomplete
nipkow
parents: 11220
diff changeset
   569
  MicroJava/BV/Correct.thy MicroJava/BV/Err.thy MicroJava/BV/JType.thy \
5516e806dc09 MicroJava/BV dependencies incomplete
nipkow
parents: 11220
diff changeset
   570
  MicroJava/BV/JVM.thy MicroJava/BV/JVMType.thy MicroJava/BV/Kildall.thy \
5516e806dc09 MicroJava/BV dependencies incomplete
nipkow
parents: 11220
diff changeset
   571
  MicroJava/BV/LBVSpec.thy MicroJava/BV/Listn.thy MicroJava/BV/Opt.thy \
5516e806dc09 MicroJava/BV dependencies incomplete
nipkow
parents: 11220
diff changeset
   572
  MicroJava/BV/Product.thy MicroJava/BV/Semilat.thy \
12521
b1ebe0320d79 MicroJava exception merge
kleing
parents: 12438
diff changeset
   573
  MicroJava/BV/Effect.thy MicroJava/BV/EffectMono.thy \
11228
5516e806dc09 MicroJava/BV dependencies incomplete
nipkow
parents: 11220
diff changeset
   574
  MicroJava/BV/Typing_Framework.thy MicroJava/BV/Typing_Framework_err.thy \
13224
6f0928a942d1 LBV instantiantion refactored, streamlined
kleing
parents: 13200
diff changeset
   575
  MicroJava/BV/Typing_Framework_JVM.thy MicroJava/BV/BVExample.thy \
6f0928a942d1 LBV instantiantion refactored, streamlined
kleing
parents: 13200
diff changeset
   576
  MicroJava/BV/LBVSpec.thy MicroJava/BV/LBVCorrect.thy \
6f0928a942d1 LBV instantiantion refactored, streamlined
kleing
parents: 13200
diff changeset
   577
  MicroJava/BV/LBVComplete.thy MicroJava/BV/LBVJVM.thy \
12915
2832fba717ec new MicroJava document
kleing
parents: 12897
diff changeset
   578
  MicroJava/document/root.bib MicroJava/document/root.tex \
2832fba717ec new MicroJava document
kleing
parents: 12897
diff changeset
   579
  MicroJava/document/introduction.tex
11850
cdfc3fce577e document graphs for several sessions;
wenzelm
parents: 11837
diff changeset
   580
	@$(ISATOOL) usedir -g true $(OUT)/HOL MicroJava
cdfc3fce577e document graphs for several sessions;
wenzelm
parents: 11837
diff changeset
   581
8012
bbdf3c51c3b8 Added MicroJava
nipkow
parents: 8008
diff changeset
   582
11376
bf98ad1c22c6 added NanoJava
oheimb
parents: 11370
diff changeset
   583
## HOL-NanoJava
bf98ad1c22c6 added NanoJava
oheimb
parents: 11370
diff changeset
   584
bf98ad1c22c6 added NanoJava
oheimb
parents: 11370
diff changeset
   585
HOL-NanoJava: HOL $(LOG)/HOL-NanoJava.gz
bf98ad1c22c6 added NanoJava
oheimb
parents: 11370
diff changeset
   586
bf98ad1c22c6 added NanoJava
oheimb
parents: 11370
diff changeset
   587
$(LOG)/HOL-NanoJava.gz: $(OUT)/HOL NanoJava/ROOT.ML \
bf98ad1c22c6 added NanoJava
oheimb
parents: 11370
diff changeset
   588
  NanoJava/Term.thy NanoJava/Decl.thy NanoJava/TypeRel.thy NanoJava/State.thy \
bf98ad1c22c6 added NanoJava
oheimb
parents: 11370
diff changeset
   589
  NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy \
bf98ad1c22c6 added NanoJava
oheimb
parents: 11370
diff changeset
   590
  NanoJava/document/root.bib NanoJava/document/root.tex
11850
cdfc3fce577e document graphs for several sessions;
wenzelm
parents: 11837
diff changeset
   591
	@$(ISATOOL) usedir -g true $(OUT)/HOL NanoJava
cdfc3fce577e document graphs for several sessions;
wenzelm
parents: 11837
diff changeset
   592
8193
33e4ec7a2daa added MicroJava/document;
wenzelm
parents: 8179
diff changeset
   593
12855
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
   594
## HOL-Bali
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
   595
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
   596
HOL-Bali: HOL $(LOG)/HOL-Bali.gz
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
   597
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
   598
$(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/AxCompl.thy Bali/AxExample.thy	\
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
   599
  Bali/AxSem.thy Bali/AxSound.thy Bali/Basis.thy Bali/Conform.thy	\
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
   600
  Bali/Decl.thy Bali/DeclConcepts.thy Bali/Eval.thy Bali/Evaln.thy	\
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
   601
  Bali/Example.thy Bali/Name.thy Bali/ROOT.ML Bali/State.thy		\
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
   602
  Bali/Table.thy Bali/Term.thy Bali/Trans.thy Bali/Type.thy		\
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
   603
  Bali/TypeRel.thy Bali/TypeSafe.thy Bali/Value.thy Bali/WellForm.thy	\
13695
3e48dcd25746 two new Bali files
kleing
parents: 13682
diff changeset
   604
  Bali/DefiniteAssignment.thy Bali/DefiniteAssignmentCorrect.thy \
12855
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
   605
  Bali/WellType.thy Bali/document/root.tex
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
   606
	@$(ISATOOL) usedir -g true $(OUT)/HOL Bali
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
   607
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
   608
13403
bc2b32ee62fd Added theory for setting up program extraction.
berghofe
parents: 13224
diff changeset
   609
## HOL-Extraction
bc2b32ee62fd Added theory for setting up program extraction.
berghofe
parents: 13224
diff changeset
   610
bc2b32ee62fd Added theory for setting up program extraction.
berghofe
parents: 13224
diff changeset
   611
HOL-Extraction: HOL $(LOG)/HOL-Extraction.gz
bc2b32ee62fd Added theory for setting up program extraction.
berghofe
parents: 13224
diff changeset
   612
23854
688a8a7bcd4e uniform naming conventions for CG theories
haftmann
parents: 23772
diff changeset
   613
$(LOG)/HOL-Extraction.gz: $(OUT)/HOL Library/Efficient_Nat.thy \
17023
7425bf9f0f4b Added Extraction/Pigeonhole.
berghofe
parents: 17011
diff changeset
   614
  Extraction/Higman.thy Extraction/ROOT.ML Extraction/Pigeonhole.thy \
7425bf9f0f4b Added Extraction/Pigeonhole.
berghofe
parents: 17011
diff changeset
   615
  Extraction/QuotRem.thy \
13403
bc2b32ee62fd Added theory for setting up program extraction.
berghofe
parents: 13224
diff changeset
   616
  Extraction/Warshall.thy Extraction/document/root.tex \
bc2b32ee62fd Added theory for setting up program extraction.
berghofe
parents: 13224
diff changeset
   617
  Extraction/document/root.bib
bc2b32ee62fd Added theory for setting up program extraction.
berghofe
parents: 13224
diff changeset
   618
	@$(ISATOOL) usedir $(OUT)/HOL Extraction
bc2b32ee62fd Added theory for setting up program extraction.
berghofe
parents: 13224
diff changeset
   619
bc2b32ee62fd Added theory for setting up program extraction.
berghofe
parents: 13224
diff changeset
   620
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   621
## HOL-IOA
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   622
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   623
HOL-IOA: HOL $(LOG)/HOL-IOA.gz
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   624
19801
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 19767
diff changeset
   625
$(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.thy IOA/IOA.thy \
b2af2549efd1 removed obsolete ML files;
wenzelm
parents: 19767
diff changeset
   626
  IOA/ROOT.ML IOA/Solve.thy
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   627
	@$(ISATOOL) usedir $(OUT)/HOL IOA
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   628
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   629
10135
c2a4dccf6e67 reorganized AxClasses;
wenzelm
parents: 10094
diff changeset
   630
## HOL-AxClasses
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   631
10135
c2a4dccf6e67 reorganized AxClasses;
wenzelm
parents: 10094
diff changeset
   632
HOL-AxClasses: HOL $(LOG)/HOL-AxClasses.gz
2545
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   633
10135
c2a4dccf6e67 reorganized AxClasses;
wenzelm
parents: 10094
diff changeset
   634
$(LOG)/HOL-AxClasses.gz: $(OUT)/HOL AxClasses/Group.thy \
c2a4dccf6e67 reorganized AxClasses;
wenzelm
parents: 10094
diff changeset
   635
  AxClasses/Product.thy AxClasses/ROOT.ML AxClasses/Semigroups.thy
c2a4dccf6e67 reorganized AxClasses;
wenzelm
parents: 10094
diff changeset
   636
	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
2545
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   637
d10abc8c11fb added AxClasses test;
wenzelm
parents: 2527
diff changeset
   638
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
   639
## HOL-Lattice
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
   640
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
   641
HOL-Lattice: HOL $(LOG)/HOL-Lattice.gz
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
   642
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
   643
$(LOG)/HOL-Lattice.gz: $(OUT)/HOL Lattice/Bounds.thy \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
   644
  Lattice/CompleteLattice.thy Lattice/Lattice.thy Lattice/Orders.thy \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
   645
  Lattice/ROOT.ML Lattice/document/root.tex
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
   646
	@$(ISATOOL) usedir $(OUT)/HOL Lattice
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
   647
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
   648
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   649
## HOL-ex
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   650
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   651
HOL-ex: HOL $(LOG)/HOL-ex.gz
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   652
23194
webertj
parents: 23193
diff changeset
   653
$(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy \
webertj
parents: 23193
diff changeset
   654
  ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy \
23213
43553703267c HOL-ex: tuned deps;
wenzelm
parents: 23194
diff changeset
   655
  ex/BT.thy ex/BinEx.thy ex/CTL.thy \
23454
c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL;
wenzelm
parents: 23449
diff changeset
   656
  ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy ex/Dense_Linear_Order_Ex.thy \
23267
51c605f34c7f added ex/Groebner_Examples.thy;
wenzelm
parents: 23265
diff changeset
   657
  ex/Eval_Examples.thy ex/Groebner_Examples.thy ex/Random.thy \
24194
96013f81faef re-eliminated Option.thy
haftmann
parents: 24162
diff changeset
   658
  ex/Codegenerator.thy ex/Codegenerator_Pretty.thy \
23194
webertj
parents: 23193
diff changeset
   659
  ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy \
webertj
parents: 23193
diff changeset
   660
  ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy \
webertj
parents: 23193
diff changeset
   661
  ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy ex/Binary.thy \
webertj
parents: 23193
diff changeset
   662
  ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy ex/InSort.thy \
webertj
parents: 23193
diff changeset
   663
  ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \
24326
3e9d3ba894b8 converted ex/MT.ML;
wenzelm
parents: 24325
diff changeset
   664
  ex/Intuitionistic.thy ex/Lagrange.thy ex/Locales.thy ex/LocaleTest2.thy \
23194
webertj
parents: 23193
diff changeset
   665
  ex/MT.thy ex/MergeSort.thy ex/MonoidGroup.thy ex/Multiquote.thy \
23502
cc726aa7d66a added NBE
nipkow
parents: 23494
diff changeset
   666
  ex/NatSum.thy ex/NBE.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
23194
webertj
parents: 23193
diff changeset
   667
  ex/Puzzle.thy ex/Qsort.thy ex/Quickcheck_Examples.thy \
23549
88190085bb82 Dependency on reflection_data.ML to build HOL-ex
chaieb
parents: 23519
diff changeset
   668
  ex/Reflection.thy ex/reflection_data.ML ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy \
23274
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 23267
diff changeset
   669
  ex/Records.thy ex/Reflected_Presburger.thy ex/coopertac.ML ex/coopereif.ML \
f997514ad8f4 New Reflected Presburger added to HOL/ex
chaieb
parents: 23267
diff changeset
   670
  ex/Refute_Examples.thy ex/SAT_Examples.thy ex/svc_oracle.ML ex/SVC_Oracle.thy \
23194
webertj
parents: 23193
diff changeset
   671
  ex/Sudoku.thy ex/Tarski.thy ex/Unification.thy ex/document/root.bib \
24127
a56b6ed2e49c converted Meson tests to proper theory;
wenzelm
parents: 24103
diff changeset
   672
  ex/document/root.tex ex/Meson_Test.thy ex/reflection.ML \
23003
4b0bf04a4d68 updated
krauss
parents: 22981
diff changeset
   673
  ex/set.thy ex/svc_funcs.ML ex/svc_test.thy Library/Parity.thy Library/GCD.thy
2826
0b0d9e3bc661 isatool usedir;
wenzelm
parents: 2635
diff changeset
   674
	@$(ISATOOL) usedir $(OUT)/HOL ex
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   675
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   676
6445
931fc1daa8b1 added Isar_examples;
wenzelm
parents: 6440
diff changeset
   677
## HOL-Isar_examples
931fc1daa8b1 added Isar_examples;
wenzelm
parents: 6440
diff changeset
   678
931fc1daa8b1 added Isar_examples;
wenzelm
parents: 6440
diff changeset
   679
HOL-Isar_examples: HOL $(LOG)/HOL-Isar_examples.gz
931fc1daa8b1 added Isar_examples;
wenzelm
parents: 6440
diff changeset
   680
931fc1daa8b1 added Isar_examples;
wenzelm
parents: 6440
diff changeset
   681
$(LOG)/HOL-Isar_examples.gz: $(OUT)/HOL Isar_examples/BasicLogic.thy \
20767
9bc632ae588f removed obsolete Real/document/root.tex;
wenzelm
parents: 20762
diff changeset
   682
  Isar_examples/Cantor.thy Isar_examples/Drinker.thy \
8050
ad6440cd84be added Isar_examples/Fibonacci.thy;
wenzelm
parents: 8040
diff changeset
   683
  Isar_examples/ExprCompiler.thy Isar_examples/Fibonacci.thy \
10143
86c39bba873f added Isar_examples/Hoare.thy Isar_examples/HoareEx.thy;
wenzelm
parents: 10135
diff changeset
   684
  Isar_examples/Group.thy Isar_examples/Hoare.thy Isar_examples/HoareEx.thy \
10255
bb66874b4750 added HOL/Library, rearranged several files;
wenzelm
parents: 10214
diff changeset
   685
  Isar_examples/KnasterTarski.thy Isar_examples/MutilatedCheckerboard.thy \
8677
de62440762b8 added Isar_examples/NestedDatatype.thy;
wenzelm
parents: 8569
diff changeset
   686
  Isar_examples/NestedDatatype.thy Isar_examples/Peirce.thy \
8050
ad6440cd84be added Isar_examples/Fibonacci.thy;
wenzelm
parents: 8040
diff changeset
   687
  Isar_examples/Puzzle.thy Isar_examples/Summation.thy \
12946
75447c743810 Isar_examples/W_correct moved to W0;
wenzelm
parents: 12918
diff changeset
   688
  Isar_examples/ROOT.ML Isar_examples/document/proof.sty \
75447c743810 Isar_examples/W_correct moved to W0;
wenzelm
parents: 12918
diff changeset
   689
  Isar_examples/document/root.bib Isar_examples/document/root.tex \
13703
a36a0d417133 Hoare.ML -> hoare.ML
kleing
parents: 13697
diff changeset
   690
  Isar_examples/document/style.tex Hoare/hoare.ML
6445
931fc1daa8b1 added Isar_examples;
wenzelm
parents: 6440
diff changeset
   691
	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
931fc1daa8b1 added Isar_examples;
wenzelm
parents: 6440
diff changeset
   692
931fc1daa8b1 added Isar_examples;
wenzelm
parents: 6440
diff changeset
   693
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
   694
## HOL-SET-Protocol
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
   695
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
   696
HOL-SET-Protocol: HOL $(LOG)/HOL-SET-Protocol.gz
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
   697
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
   698
$(LOG)/HOL-SET-Protocol.gz: $(OUT)/HOL SET-Protocol/ROOT.ML \
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
   699
  SET-Protocol/MessageSET.thy\
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
   700
  SET-Protocol/EventSET.thy\
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
   701
  SET-Protocol/PublicSET.thy\
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
   702
  SET-Protocol/Cardholder_Registration.thy\
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
   703
  SET-Protocol/Merchant_Registration.thy\
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
   704
  SET-Protocol/Purchase.thy\
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
   705
  SET-Protocol/document/root.tex 
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
   706
	@$(ISATOOL) usedir -g true $(OUT)/HOL SET-Protocol
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
   707
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
   708
16509
20f4c6a950f7 fixed HOL-Complex-Matrix target;
wenzelm
parents: 16484
diff changeset
   709
## HOL-Complex-Matrix
14610
9c2e31e483b2 added HOL-Matrix, added HOL/Matrix/ROOT.ML
kleing
parents: 14603
diff changeset
   710
17546
07371b92d382 HOL-Complex-Matrix: fixed deps;
wenzelm
parents: 17518
diff changeset
   711
HOL-Complex-Matrix: HOL-Complex $(OUT)/HOL-Complex-Matrix
17323
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight
obua
parents: 17308
diff changeset
   712
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight
obua
parents: 17308
diff changeset
   713
$(OUT)/HOL-Complex-Matrix: $(OUT)/HOL-Complex \
23172
f1ae6a8648ef moved IsaPlanner from Provers to Tools;
wenzelm
parents: 23164
diff changeset
   714
  $(SRC)/Tools/Compute_Oracle/Compute_Oracle.thy \
f1ae6a8648ef moved IsaPlanner from Provers to Tools;
wenzelm
parents: 23164
diff changeset
   715
  $(SRC)/Tools/Compute_Oracle/am_compiler.ML \
f1ae6a8648ef moved IsaPlanner from Provers to Tools;
wenzelm
parents: 23164
diff changeset
   716
  $(SRC)/Tools/Compute_Oracle/am_interpreter.ML \
23772
b96db2903a9a changed sources for HOL-Complex-Matrix
obua
parents: 23734
diff changeset
   717
  $(SRC)/Tools/Compute_Oracle/am.ML \
b96db2903a9a changed sources for HOL-Complex-Matrix
obua
parents: 23734
diff changeset
   718
  $(SRC)/Tools/Compute_Oracle/linker.ML \
b96db2903a9a changed sources for HOL-Complex-Matrix
obua
parents: 23734
diff changeset
   719
  $(SRC)/Tools/Compute_Oracle/am_ghc.ML \
b96db2903a9a changed sources for HOL-Complex-Matrix
obua
parents: 23734
diff changeset
   720
  $(SRC)/Tools/Compute_Oracle/am_sml.ML \
23194
webertj
parents: 23193
diff changeset
   721
  $(SRC)/Tools/Compute_Oracle/compute.ML \
23172
f1ae6a8648ef moved IsaPlanner from Provers to Tools;
wenzelm
parents: 23164
diff changeset
   722
  Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
f1ae6a8648ef moved IsaPlanner from Provers to Tools;
wenzelm
parents: 23164
diff changeset
   723
  Matrix/LP.thy Matrix/document/root.tex Matrix/ROOT.ML \
17489
f70d62d5f9c8 Removed superfluous HOL/Matrix/cplex/ROOT.ML.
obua
parents: 17488
diff changeset
   724
  Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents: 16782
diff changeset
   725
  Matrix/cplex/Cplex_tools.ML Matrix/cplex/FloatSparseMatrix.thy \
16873
9ed940a1bebb proving bounds for real linear programs
obua
parents: 16784
diff changeset
   726
  Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \
20787
406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents: 20767
diff changeset
   727
  Matrix/cplex/MatrixLP.thy Matrix/cplex/matrixlp.ML
17323
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight
obua
parents: 17308
diff changeset
   728
	@cd Matrix; $(ISATOOL) usedir -b -g true $(OUT)/HOL-Complex HOL-Complex-Matrix
16873
9ed940a1bebb proving bounds for real linear programs
obua
parents: 16784
diff changeset
   729
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
   730
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   731
## TLA
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   732
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   733
TLA: HOL $(OUT)/TLA
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   734
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 21542
diff changeset
   735
$(OUT)/TLA: $(OUT)/HOL TLA/Action.thy TLA/Init.thy TLA/Intensional.thy \
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 21542
diff changeset
   736
  TLA/ROOT.ML TLA/Stfun.thy TLA/TLA.thy
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   737
	@cd TLA; $(ISATOOL) usedir -b $(OUT)/HOL TLA
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   738
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   739
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   740
## TLA-Inc
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   741
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   742
TLA-Inc: TLA $(LOG)/TLA-Inc.gz
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   743
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 21542
diff changeset
   744
$(LOG)/TLA-Inc.gz: $(OUT)/TLA TLA/Inc/Inc.thy
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   745
	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Inc
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   746
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   747
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   748
## TLA-Buffer
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   749
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   750
TLA-Buffer: TLA $(LOG)/TLA-Buffer.gz
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   751
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 21542
diff changeset
   752
$(LOG)/TLA-Buffer.gz: $(OUT)/TLA TLA/Buffer/Buffer.thy TLA/Buffer/DBuffer.thy
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   753
	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Buffer
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   754
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   755
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   756
## TLA-Memory
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   757
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   758
TLA-Memory: TLA $(LOG)/TLA-Memory.gz
4447
b7ee449eb345 log files;
wenzelm
parents: 4289
diff changeset
   759
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   760
$(LOG)/TLA-Memory.gz: $(OUT)/TLA TLA/Memory/MIParameters.thy \
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 21542
diff changeset
   761
  TLA/Memory/MemClerk.thy TLA/Memory/MemClerkParameters.thy \
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 21542
diff changeset
   762
  TLA/Memory/Memory.thy TLA/Memory/MemoryImplementation.thy \
23194
webertj
parents: 23193
diff changeset
   763
  TLA/Memory/MemoryParameters.thy TLA/Memory/ProcedureInterface.thy \
webertj
parents: 23193
diff changeset
   764
  TLA/Memory/RPC.thy \
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 21542
diff changeset
   765
  TLA/Memory/RPCMemoryParams.thy TLA/Memory/RPCParameters.thy
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   766
	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Memory
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   767
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   768
19497
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
   769
## HOL-Nominal
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
   770
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
   771
HOL-Nominal: HOL $(OUT)/HOL-Nominal
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
   772
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents: 22167
diff changeset
   773
$(OUT)/HOL-Nominal: $(OUT)/HOL Nominal/ROOT.ML \
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents: 22167
diff changeset
   774
  Nominal/Nominal.thy \
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents: 22167
diff changeset
   775
  Nominal/nominal_atoms.ML \
22784
4637b69de71b Added datatype_case.ML and nominal_fresh_fun.ML.
berghofe
parents: 22657
diff changeset
   776
  Nominal/nominal_fresh_fun.ML \
22247
5bad0d429694 corrected typo introduced by me
urbanc
parents: 22245
diff changeset
   777
  Nominal/nominal_induct.ML \
22314
d541f13756a2 Added new file Nominal/nominal_inductive.ML
berghofe
parents: 22260
diff changeset
   778
  Nominal/nominal_inductive.ML \
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents: 22167
diff changeset
   779
  Nominal/nominal_package.ML \
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents: 22167
diff changeset
   780
  Nominal/nominal_permeq.ML \
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents: 22167
diff changeset
   781
  Nominal/nominal_primrec.ML \
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents: 22167
diff changeset
   782
  Nominal/nominal_thmdecls.ML \
21542
4462ee172ef0 Added nominal_primrec.ML
berghofe
parents: 21425
diff changeset
   783
  Library/Infinite_Set.thy
19497
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
   784
	@cd Nominal; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Nominal
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
   785
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
   786
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
   787
## HOL-Nominal-Examples
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
   788
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
   789
HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
   790
19564
d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents: 19499
diff changeset
   791
$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal 	\
22077
2882d9cc5e75 fixed typo introduced by me
urbanc
parents: 22073
diff changeset
   792
  Nominal/Examples/ROOT.ML \
22073
c170dcbe6c9d formalisation of Crary's chapter on logical relations
urbanc
parents: 22067
diff changeset
   793
  Nominal/Examples/CR.thy \
22821
15b2e7ec1f3b alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents: 22819
diff changeset
   794
  Nominal/Examples/CR_Takahashi.thy \
24152
63cc746667a0 reactivated Nominal/Examples/Class.thy;
wenzelm
parents: 24139
diff changeset
   795
  Nominal/Examples/Class.thy \
22073
c170dcbe6c9d formalisation of Crary's chapter on logical relations
urbanc
parents: 22067
diff changeset
   796
  Nominal/Examples/Compile.thy \
c170dcbe6c9d formalisation of Crary's chapter on logical relations
urbanc
parents: 22067
diff changeset
   797
  Nominal/Examples/Fsub.thy \
c170dcbe6c9d formalisation of Crary's chapter on logical relations
urbanc
parents: 22067
diff changeset
   798
  Nominal/Examples/Lambda_mu.thy \
c170dcbe6c9d formalisation of Crary's chapter on logical relations
urbanc
parents: 22067
diff changeset
   799
  Nominal/Examples/Lam_Funs.thy	\
c170dcbe6c9d formalisation of Crary's chapter on logical relations
urbanc
parents: 22067
diff changeset
   800
  Nominal/Examples/SN.thy \
c170dcbe6c9d formalisation of Crary's chapter on logical relations
urbanc
parents: 22067
diff changeset
   801
  Nominal/Examples/Weakening.thy \
22448
f982e73e36de adjusted for the example file SOS.thy
urbanc
parents: 22375
diff changeset
   802
  Nominal/Examples/Crary.thy \
23144
4a9c9e260abf included new example in the compiling process
urbanc
parents: 23100
diff changeset
   803
  Nominal/Examples/SOS.thy \
4a9c9e260abf included new example in the compiling process
urbanc
parents: 23100
diff changeset
   804
  Nominal/Examples/LocalWeakening.thy
19497
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
   805
	@cd Nominal; $(ISATOOL) usedir $(OUT)/HOL-Nominal Examples
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
   806
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
   807
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
   808
## HOL-Word
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
   809
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
   810
HOL-Word: HOL $(OUT)/HOL-Word
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
   811
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
   812
$(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML \
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
   813
  Library/Infinite_Set.thy Library/Parity.thy \
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
   814
  Library/Boolean_Algebra.thy Library/Numeral_Type.thy \
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
   815
  Word/Num_Lemmas.thy \
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
   816
  Word/TdThs.thy \
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
   817
  Word/Size.thy \
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
   818
  Word/BinGeneral.thy \
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
   819
  Word/BinOperations.thy \
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
   820
  Word/BinBoolList.thy \
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
   821
  Word/BitSyntax.thy \
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
   822
  Word/WordDefinition.thy \
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
   823
  Word/WordArith.thy \
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
   824
  Word/WordBitwise.thy \
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
   825
  Word/WordShift.thy \
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
   826
  Word/WordGenLib.thy \
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
   827
  Word/WordMain.thy \
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
   828
  Word/WordExamples.thy
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
   829
	@cd Word; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Word
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
   830
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
   831
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   832
## clean
4447
b7ee449eb345 log files;
wenzelm
parents: 4289
diff changeset
   833
b7ee449eb345 log files;
wenzelm
parents: 4289
diff changeset
   834
clean:
19497
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
   835
	@rm -f  $(OUT)/HOL $(OUT)/HOL-Complex $(OUT)/HOL-Nominal $(OUT)/TLA \
13980
f254d1c92a6a removed obsolete references to HOL-Real
paulson
parents: 13967
diff changeset
   836
		$(LOG)/HOL.gz $(LOG)/TLA.gz \
9481
wenzelm
parents: 9479
diff changeset
   837
		$(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \
wenzelm
parents: 9479
diff changeset
   838
		$(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \
wenzelm
parents: 9479
diff changeset
   839
		$(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \
12996
7ac0a7e306db Completed annonce of HoareParallel
prensani
parents: 12951
diff changeset
   840
		$(LOG)/HOL-HoareParallel.gz \
9481
wenzelm
parents: 9479
diff changeset
   841
		$(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
wenzelm
parents: 9479
diff changeset
   842
		$(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
wenzelm
parents: 9479
diff changeset
   843
		$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
15871
e524119dbf19 *** empty log message ***
bauerg
parents: 15858
diff changeset
   844
                $(LOG)/HOL-Bali.gz \
11376
bf98ad1c22c6 added NanoJava
oheimb
parents: 11370
diff changeset
   845
		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
19497
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
   846
                $(LOG)/HOL-Nominal-Examples.gz \
10135
c2a4dccf6e67 reorganized AxClasses;
wenzelm
parents: 10094
diff changeset
   847
		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
16509
20f4c6a950f7 fixed HOL-Complex-Matrix target;
wenzelm
parents: 16484
diff changeset
   848
		$(LOG)/HOL-Lattice $(LOG)/HOL-Complex-Matrix \
13980
f254d1c92a6a removed obsolete references to HOL-Real
paulson
parents: 13967
diff changeset
   849
		$(LOG)/HOL-Complex.gz \
13961
233dd3bb2390 new directory Complex
paulson
parents: 13949
diff changeset
   850
		$(LOG)/HOL-Complex-ex.gz \
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
   851
		$(LOG)/HOL-Complex-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz \
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
   852
                $(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz \
10981
wenzelm
parents: 10980
diff changeset
   853
		$(LOG)/HOL-Library.gz $(LOG)/HOL-Unix.gz