src/HOL/IsaMakefile
author bulwahn
Fri, 11 Mar 2011 10:37:36 +0100
changeset 41906 e163d435ccf7
parent 41892 2386fb64feaf
child 41911 c6e66b32ce16
permissions -rw-r--r--
adding Lazysmallcheck prototype to HOL-Library
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
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
     8
generate: HOL-Generate-HOL HOL-Generate-HOLLight
33210
94ae82a4452f recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents: 33204
diff changeset
     9
94ae82a4452f recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents: 33204
diff changeset
    10
images: \
94ae82a4452f recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents: 33204
diff changeset
    11
  HOL \
37691
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
    12
  HOL-Library \
33210
94ae82a4452f recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents: 33204
diff changeset
    13
  HOL-Algebra \
33419
8ae45e87b992 added HOL-Boogie
boehmes
parents: 33356
diff changeset
    14
  HOL-Boogie \
33210
94ae82a4452f recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents: 33204
diff changeset
    15
  HOL-Multivariate_Analysis \
94ae82a4452f recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents: 33204
diff changeset
    16
  HOL-NSA \
94ae82a4452f recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents: 33204
diff changeset
    17
  HOL-Nominal \
35931
6c9f7dc1ad07 more accurate dependencies;
wenzelm
parents: 35928
diff changeset
    18
  HOL-Probability \
34205
f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents: 34126
diff changeset
    19
  HOL-Proofs \
41566
676b32bea254 Added HOL-SPARK and removed old_primrec.ML
berghofe
parents: 41505
diff changeset
    20
  HOL-SPARK \
33210
94ae82a4452f recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents: 33204
diff changeset
    21
  HOL-Word \
94ae82a4452f recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents: 33204
diff changeset
    22
  HOL4 \
40774
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF;
huffman
parents: 40676
diff changeset
    23
  HOLCF \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF;
huffman
parents: 40676
diff changeset
    24
  IOA \
37691
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
    25
  TLA \
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
    26
  HOL-Base \
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
    27
  HOL-Main \
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
    28
  HOL-Plain
10135
c2a4dccf6e67 reorganized AxClasses;
wenzelm
parents: 10094
diff changeset
    29
37691
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
    30
#Note: keep targets sorted (except for HOL-ex)
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    31
test: \
24325
5c29e8822f50 make HOL-ex earlier;
wenzelm
parents: 24288
diff changeset
    32
  HOL-ex \
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    33
  HOL-Auth \
14031
3240066af013 Added Bali to test
schirmer
parents: 14029
diff changeset
    34
  HOL-Bali \
33439
f5d95787224f more accurate dependencies;
wenzelm
parents: 33437
diff changeset
    35
  HOL-Boogie-Examples \
29823
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
    36
  HOL-Decision_Procs \
31795
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 31771
diff changeset
    37
  HOL-Hahn_Banach \
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    38
  HOL-Hoare \
32621
a073cb249a06 theory entry point for session Hoare_Parallel (now also with proper underscore)
haftmann
parents: 32618
diff changeset
    39
  HOL-Hoare_Parallel \
40774
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF;
huffman
parents: 40676
diff changeset
    40
      HOLCF-FOCUS \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF;
huffman
parents: 40676
diff changeset
    41
      HOLCF-IMP \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF;
huffman
parents: 40676
diff changeset
    42
      HOLCF-Library \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF;
huffman
parents: 40676
diff changeset
    43
      HOLCF-Tutorial \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF;
huffman
parents: 40676
diff changeset
    44
      HOLCF-ex \
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    45
  HOL-IMP \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    46
  HOL-IMPP \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    47
  HOL-IOA \
40774
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF;
huffman
parents: 40676
diff changeset
    48
      IOA-ABP \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF;
huffman
parents: 40676
diff changeset
    49
      IOA-NTP \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF;
huffman
parents: 40676
diff changeset
    50
      IOA-Storage \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF;
huffman
parents: 40676
diff changeset
    51
      IOA-ex \
29399
ebcd69a00872 split of Imperative_HOL theories from HOL-Library
haftmann
parents: 29197
diff changeset
    52
  HOL-Imperative_HOL \
33210
94ae82a4452f recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents: 33204
diff changeset
    53
  HOL-Import \
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    54
  HOL-Induct \
33026
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
    55
  HOL-Isar_Examples \
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    56
  HOL-Lattice \
37747
3a699743bcba more accurate dependencies
haftmann
parents: 37742
diff changeset
    57
  HOL-Library-Codegenerator_Test \
28637
7aabaf1ba263 reactivated HOL-Matrix;
wenzelm
parents: 28612
diff changeset
    58
  HOL-Matrix \
33027
9cf389429f6d modernized session Metis_Examples;
wenzelm
parents: 33026
diff changeset
    59
  HOL-Metis_Examples \
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    60
  HOL-MicroJava \
32496
4ab00a2642c3 moved Mirabelle from HOL/Tools to HOL,
boehmes
parents: 32479
diff changeset
    61
  HOL-Mirabelle \
35536
1f980bbc6ad8 adding HOL-Mutabelle to tests
bulwahn
parents: 35502
diff changeset
    62
  HOL-Mutabelle \
11376
bf98ad1c22c6 added NanoJava
oheimb
parents: 11370
diff changeset
    63
  HOL-NanoJava \
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents: 33192
diff changeset
    64
  HOL-Nitpick_Examples \
19497
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
    65
  HOL-Nominal-Examples \
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
    66
  HOL-Number_Theory \
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
    67
  HOL-Old_Number_Theory \
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35151
diff changeset
    68
  HOL-Quotient_Examples \
35950
791ce568d40a moved examples for the predicate compiler into its own session Predicate_Compile_Examples to slenderise the HOL-ex session
bulwahn
parents: 35931
diff changeset
    69
  HOL-Predicate_Compile_Examples \
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    70
  HOL-Prolog \
39157
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
    71
  HOL-Proofs-ex \
34205
f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents: 34126
diff changeset
    72
  HOL-Proofs-Extraction \
f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents: 34126
diff changeset
    73
  HOL-Proofs-Lambda \
33028
9aa8bfb1649d modernized session SET_Protocol;
wenzelm
parents: 33027
diff changeset
    74
  HOL-SET_Protocol \
41569
98f59921c420 Also added SPARK to test and clean targets.
berghofe
parents: 41566
diff changeset
    75
  HOL-SPARK-Examples \
36933
705b58fde476 more precise dependencies for HOL-Word-SMT_Examples;
wenzelm
parents: 36916
diff changeset
    76
  HOL-Word-SMT_Examples \
25171
4a9c25bffc9b added Statespace library
schirmer
parents: 24994
diff changeset
    77
  HOL-Statespace \
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    78
  HOL-Subst \
33210
94ae82a4452f recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents: 33204
diff changeset
    79
      TLA-Buffer \
94ae82a4452f recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents: 33204
diff changeset
    80
      TLA-Inc \
94ae82a4452f recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents: 33204
diff changeset
    81
      TLA-Memory \
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    82
  HOL-UNITY \
10966
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
    83
  HOL-Unix \
24442
39e29972cb96 HOL-Word-Examples
huffman
parents: 24411
diff changeset
    84
  HOL-Word-Examples \
24325
5c29e8822f50 make HOL-ex earlier;
wenzelm
parents: 24288
diff changeset
    85
  HOL-ZF
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    86
    # ^ this is the sort position
10614
d5c14e205c24 added Library/Rational_Numbers.thy;
wenzelm
parents: 10574
diff changeset
    87
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    88
all: test images
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
    89
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
    90
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
    91
## global settings
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
    92
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
    93
SRC = $(ISABELLE_HOME)/src
3118
24dae6222579 fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?);
wenzelm
parents: 3079
diff changeset
    94
OUT = $(ISABELLE_OUTPUT)
4447
b7ee449eb345 log files;
wenzelm
parents: 4289
diff changeset
    95
LOG = $(OUT)/log
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    96
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
    97
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
    98
## HOL
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
    99
28393
30ba169e8c45 HOL no longer depends on HOL-Plain;
wenzelm
parents: 28376
diff changeset
   100
HOL: Pure $(OUT)/HOL
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   101
29505
c6d2d23909d1 added HOL-Base image
haftmann
parents: 29463
diff changeset
   102
HOL-Base: Pure $(OUT)/HOL-Base
c6d2d23909d1 added HOL-Base image
haftmann
parents: 29463
diff changeset
   103
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   104
HOL-Plain: Pure $(OUT)/HOL-Plain
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   105
28401
d5f39173444c separate HOL-Main image
haftmann
parents: 28393
diff changeset
   106
HOL-Main: Pure $(OUT)/HOL-Main
d5f39173444c separate HOL-Main image
haftmann
parents: 28393
diff changeset
   107
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   108
Pure:
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   109
	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
3232
19a2b853ba7b Removal of ex/LexProd; TFL files; new treatment of Prover files
paulson
parents: 3222
diff changeset
   110
27694
31a8e0908b9f corrected Pure dependency
haftmann
parents: 27679
diff changeset
   111
$(OUT)/Pure: Pure
31a8e0908b9f corrected Pure dependency
haftmann
parents: 27679
diff changeset
   112
36073
54a9f56fae7c slightly more standard dependencies;
wenzelm
parents: 36066
diff changeset
   113
BASE_DEPENDENCIES = $(OUT)/Pure \
30160
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 30101
diff changeset
   114
  $(SRC)/Provers/blast.ML \
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 30101
diff changeset
   115
  $(SRC)/Provers/clasimp.ML \
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 30101
diff changeset
   116
  $(SRC)/Provers/classical.ML \
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 30101
diff changeset
   117
  $(SRC)/Provers/hypsubst.ML \
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 30101
diff changeset
   118
  $(SRC)/Provers/quantifier1.ML \
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 30101
diff changeset
   119
  $(SRC)/Provers/splitter.ML \
37818
dd65033fed78 load cache_io before code generator; moved adhoc-overloading to generic tools
haftmann
parents: 37790
diff changeset
   120
  $(SRC)/Tools/cache_io.ML \
31771
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   121
  $(SRC)/Tools/Code/code_haskell.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   122
  $(SRC)/Tools/Code/code_ml.ML \
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents: 38965
diff changeset
   123
  $(SRC)/Tools/Code/code_namespace.ML \
31771
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   124
  $(SRC)/Tools/Code/code_preproc.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   125
  $(SRC)/Tools/Code/code_printer.ML \
39402
24d70f4e690d more accurate dependencies
haftmann
parents: 39394
diff changeset
   126
  $(SRC)/Tools/Code/code_runtime.ML \
34945
478f31081a78 more accurate dependencies
haftmann
parents: 34228
diff changeset
   127
  $(SRC)/Tools/Code/code_scala.ML \
37442
037ee7b712b2 added code_simp infrastructure
haftmann
parents: 37296
diff changeset
   128
  $(SRC)/Tools/Code/code_simp.ML \
31771
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   129
  $(SRC)/Tools/Code/code_target.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   130
  $(SRC)/Tools/Code/code_thingol.ML \
32733
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents: 32674
diff changeset
   131
  $(SRC)/Tools/Code_Generator.thy \
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents: 32674
diff changeset
   132
  $(SRC)/Tools/IsaPlanner/isand.ML \
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents: 32674
diff changeset
   133
  $(SRC)/Tools/IsaPlanner/rw_inst.ML \
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents: 32674
diff changeset
   134
  $(SRC)/Tools/IsaPlanner/rw_tools.ML \
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents: 32674
diff changeset
   135
  $(SRC)/Tools/IsaPlanner/zipper.ML \
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents: 32674
diff changeset
   136
  $(SRC)/Tools/atomize_elim.ML \
39323
ce5c6a8b0359 start renaming "Auto_Counterexample" to "Auto_Tools";
blanchet
parents: 39271
diff changeset
   137
  $(SRC)/Tools/auto_tools.ML \
41827
98eda7ffde79 setup case_product attribute in HOL and FOL
noschinl
parents: 41655
diff changeset
   138
  $(SRC)/Tools/case_product.ML \
30160
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 30101
diff changeset
   139
  $(SRC)/Tools/coherent.ML \
32733
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents: 32674
diff changeset
   140
  $(SRC)/Tools/cong_tac.ML \
30160
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 30101
diff changeset
   141
  $(SRC)/Tools/eqsubst.ML \
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 30101
diff changeset
   142
  $(SRC)/Tools/induct.ML \
32733
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents: 32674
diff changeset
   143
  $(SRC)/Tools/induct_tacs.ML \
30165
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents: 30160
diff changeset
   144
  $(SRC)/Tools/intuitionistic.ML \
37781
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents: 37779
diff changeset
   145
  $(SRC)/Tools/misc_legacy.ML \
30160
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 30101
diff changeset
   146
  $(SRC)/Tools/nbe.ML \
32733
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents: 32674
diff changeset
   147
  $(SRC)/Tools/project_rule.ML \
30973
304ab57afa6e observe distinction between Pure/Tools and Tools more closely
haftmann
parents: 30954
diff changeset
   148
  $(SRC)/Tools/quickcheck.ML \
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 40067
diff changeset
   149
  $(SRC)/Tools/solve_direct.ML \
30160
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 30101
diff changeset
   150
  $(SRC)/Tools/value.ML \
29505
c6d2d23909d1 added HOL-Base image
haftmann
parents: 29463
diff changeset
   151
  HOL.thy \
c6d2d23909d1 added HOL-Base image
haftmann
parents: 29463
diff changeset
   152
  Tools/hologic.ML \
c6d2d23909d1 added HOL-Base image
haftmann
parents: 29463
diff changeset
   153
  Tools/recfun_codegen.ML \
36073
54a9f56fae7c slightly more standard dependencies;
wenzelm
parents: 36066
diff changeset
   154
  Tools/simpdata.ML
29505
c6d2d23909d1 added HOL-Base image
haftmann
parents: 29463
diff changeset
   155
c6d2d23909d1 added HOL-Base image
haftmann
parents: 29463
diff changeset
   156
$(OUT)/HOL-Base: base.ML $(BASE_DEPENDENCIES)
29523
f83dcdcee6b3 no document for HOL-Base
haftmann
parents: 29505
diff changeset
   157
	@$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base
29505
c6d2d23909d1 added HOL-Base image
haftmann
parents: 29463
diff changeset
   158
39157
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   159
PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES) \
40939
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   160
  $(SRC)/Provers/Arith/cancel_div_mod.ML \
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   161
  $(SRC)/Provers/Arith/cancel_sums.ML \
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   162
  $(SRC)/Provers/Arith/fast_lin_arith.ML \
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   163
  $(SRC)/Provers/order.ML \
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   164
  $(SRC)/Provers/trancl.ML \
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   165
  $(SRC)/Tools/Metis/metis.ML \
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   166
  $(SRC)/Tools/rat.ML \
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   167
  $(SRC)/Tools/subtyping.ML \
32139
e271a64f03ff moved complete_lattice &c. into separate theory
haftmann
parents: 31990
diff changeset
   168
  Complete_Lattice.thy \
40108
dbab949c2717 integrated partial_function into HOL-Plain
krauss
parents: 40104
diff changeset
   169
  Complete_Partial_Order.thy \
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   170
  Datatype.thy \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   171
  Extraction.thy \
35050
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 35039
diff changeset
   172
  Fields.thy \
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   173
  Finite_Set.thy \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   174
  Fun.thy \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   175
  FunDef.thy \
35050
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 35039
diff changeset
   176
  Groups.thy \
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   177
  Inductive.thy \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   178
  Lattices.thy \
39945
277addece9b7 added "Meson" theory to Makefile
blanchet
parents: 39940
diff changeset
   179
  Meson.thy \
39946
78faa9b31202 move Metis into Plain
blanchet
parents: 39945
diff changeset
   180
  Metis.thy \
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   181
  Nat.thy \
32733
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents: 32674
diff changeset
   182
  Option.thy \
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   183
  Orderings.thy \
40108
dbab949c2717 integrated partial_function into HOL-Plain
krauss
parents: 40104
diff changeset
   184
  Partial_Function.thy \
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   185
  Plain.thy \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   186
  Power.thy \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   187
  Predicate.thy \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   188
  Product_Type.thy \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   189
  Relation.thy \
35050
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 35039
diff changeset
   190
  Rings.thy \
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   191
  SAT.thy \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   192
  Set.thy \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   193
  Sum_Type.thy \
40939
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   194
  Tools/Datatype/datatype.ML \
31771
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   195
  Tools/Datatype/datatype_abs_proofs.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   196
  Tools/Datatype/datatype_aux.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   197
  Tools/Datatype/datatype_case.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   198
  Tools/Datatype/datatype_codegen.ML \
33963
977b94b64905 renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
haftmann
parents: 33954
diff changeset
   199
  Tools/Datatype/datatype_data.ML \
31771
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   200
  Tools/Datatype/datatype_prop.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   201
  Tools/Datatype/datatype_realizer.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   202
  Tools/Function/context_tree.ML \
40939
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   203
  Tools/Function/fun.ML \
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   204
  Tools/Function/function.ML \
33099
b8cdd3d73022 function package: more standard names for structures and files
krauss
parents: 33098
diff changeset
   205
  Tools/Function/function_common.ML \
b8cdd3d73022 function package: more standard names for structures and files
krauss
parents: 33098
diff changeset
   206
  Tools/Function/function_core.ML \
b8cdd3d73022 function package: more standard names for structures and files
krauss
parents: 33098
diff changeset
   207
  Tools/Function/function_lib.ML \
33471
5aef13872723 renamed method induct_scheme to induction_schema
krauss
parents: 33469
diff changeset
   208
  Tools/Function/induction_schema.ML \
31771
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   209
  Tools/Function/lexicographic_order.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   210
  Tools/Function/measure_functions.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   211
  Tools/Function/mutual.ML \
40108
dbab949c2717 integrated partial_function into HOL-Plain
krauss
parents: 40104
diff changeset
   212
  Tools/Function/partial_function.ML \
33083
1fad3160d873 pat_completeness gets its own file
krauss
parents: 33028
diff changeset
   213
  Tools/Function/pat_completeness.ML \
31771
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   214
  Tools/Function/pattern_split.ML \
33100
acc2bd3934ba renamed auto_term.ML -> relation.ML
krauss
parents: 33099
diff changeset
   215
  Tools/Function/relation.ML \
31771
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   216
  Tools/Function/scnp_reconstruct.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   217
  Tools/Function/scnp_solve.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   218
  Tools/Function/size.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   219
  Tools/Function/sum_tree.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   220
  Tools/Function/termination.ML \
39940
1f01c9b2b76b move MESON files together
blanchet
parents: 39889
diff changeset
   221
  Tools/Meson/meson.ML \
1f01c9b2b76b move MESON files together
blanchet
parents: 39889
diff changeset
   222
  Tools/Meson/meson_clausify.ML \
39948
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify"
blanchet
parents: 39946
diff changeset
   223
  Tools/Meson/meson_tactic.ML \
39946
78faa9b31202 move Metis into Plain
blanchet
parents: 39945
diff changeset
   224
  Tools/Metis/metis_reconstruct.ML \
40939
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   225
  Tools/Metis/metis_tactics.ML \
39946
78faa9b31202 move Metis into Plain
blanchet
parents: 39945
diff changeset
   226
  Tools/Metis/metis_translate.ML \
40939
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   227
  Tools/abel_cancel.ML \
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   228
  Tools/arith_data.ML \
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   229
  Tools/cnf_funcs.ML \
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   230
  Tools/dseq.ML \
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   231
  Tools/inductive.ML \
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   232
  Tools/inductive_codegen.ML \
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   233
  Tools/inductive_realizer.ML \
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   234
  Tools/inductive_set.ML \
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   235
  Tools/lin_arith.ML \
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 30457
diff changeset
   236
  Tools/nat_arith.ML \
31723
f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents: 31706
diff changeset
   237
  Tools/primrec.ML \
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   238
  Tools/prop_logic.ML \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   239
  Tools/refute.ML \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   240
  Tools/rewrite_hol_proof.ML \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   241
  Tools/sat_funcs.ML \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   242
  Tools/sat_solver.ML \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   243
  Tools/split_rule.ML \
38942
e10c11971fa7 "try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents: 38730
diff changeset
   244
  Tools/try.ML \
31723
f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents: 31706
diff changeset
   245
  Tools/typedef.ML \
41505
6d19301074cf "enriched_type" replaces less specific "type_lifting"
haftmann
parents: 41496
diff changeset
   246
  Tools/enriched_type.ML \
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   247
  Transitive_Closure.thy \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   248
  Typedef.thy \
40939
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   249
  Wellfounded.thy
28312
f0838044f034 different session branches for HOL-Plain vs. Plain
haftmann
parents: 28243
diff changeset
   250
f0838044f034 different session branches for HOL-Plain vs. Plain
haftmann
parents: 28243
diff changeset
   251
$(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES)
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   252
	@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   253
28401
d5f39173444c separate HOL-Main image
haftmann
parents: 28393
diff changeset
   254
MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
40178
00152d17855b reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
blanchet
parents: 40162
diff changeset
   255
  ATP.thy \
35725
4d7e3cc9c52c Big_Operators now in Main rather than Plain src/HOL/Wellfounded.thy
haftmann
parents: 35719
diff changeset
   256
  Big_Operators.thy \
32657
5f13912245ff Code_Eval(uation)
haftmann
parents: 32636
diff changeset
   257
  Code_Evaluation.thy \
31205
98370b26c2ce String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents: 31203
diff changeset
   258
  Code_Numeral.thy \
33296
a3924d1069e5 moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents: 33272
diff changeset
   259
  Divides.thy \
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34228
diff changeset
   260
  DSequence.thy \
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   261
  Equiv_Relations.thy \
40650
d40b347d5b0b adding Enum to HOL-Main image and removing it from HOL-Library
bulwahn
parents: 40634
diff changeset
   262
  Enum.thy \
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   263
  Groebner_Basis.thy \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   264
  Hilbert_Choice.thy \
32733
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents: 32674
diff changeset
   265
  Int.thy \
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34228
diff changeset
   266
  Lazy_Sequence.thy \
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   267
  List.thy \
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   268
  Main.thy \
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   269
  Map.thy \
30925
c38cbc0ac8d1 theory NatBin now named Nat_Numeral
haftmann
parents: 30689
diff changeset
   270
  Nat_Numeral.thy \
33318
ddd97d9dfbfb moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents: 33298
diff changeset
   271
  Nat_Transfer.thy \
39183
512c10416590 adding dependencies to IsaMakefile; increasing negative search limit for predicate_compile_quickcheck; adding tracing of introduction rules in code_prolog
bulwahn
parents: 39048
diff changeset
   272
  New_DSequence.thy \
512c10416590 adding dependencies to IsaMakefile; increasing negative search limit for predicate_compile_quickcheck; adding tracing of introduction rules in code_prolog
bulwahn
parents: 39048
diff changeset
   273
  New_Random_Sequence.thy \
36915
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   274
  Nitpick.thy \
33356
9157d0f9f00e moved Commutative_Ring into session Decision_Procs
haftmann
parents: 33348
diff changeset
   275
  Numeral_Simprocs.thy \
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   276
  Presburger.thy \
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33210
diff changeset
   277
  Predicate_Compile.thy \
31203
5c8fb4fd67e0 moved Code_Index, Random and Quickcheck before Main
haftmann
parents: 31186
diff changeset
   278
  Quickcheck.thy \
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35151
diff changeset
   279
  Quotient.thy \
31203
5c8fb4fd67e0 moved Code_Index, Random and Quickcheck before Main
haftmann
parents: 31186
diff changeset
   280
  Random.thy \
34948
2d5f2a9f7601 refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents: 34228
diff changeset
   281
  Random_Sequence.thy \
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   282
  Recdef.thy \
39271
436554f1beaa more correct dependencies
haftmann
parents: 39223
diff changeset
   283
  Record.thy \
36916
279074271b8e move Refute dependency from Plain to Main
blanchet
parents: 36915
diff changeset
   284
  Refute.thy \
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36700
diff changeset
   285
  Semiring_Normalization.thy \
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   286
  SetInterval.thy \
40178
00152d17855b reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
blanchet
parents: 40162
diff changeset
   287
  Sledgehammer.thy \
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents: 40355
diff changeset
   288
  Smallcheck.thy \
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
   289
  SMT.thy \
31048
ac146fc38b51 refined HOL string theories and corresponding ML fragments
haftmann
parents: 31036
diff changeset
   290
  String.thy \
31203
5c8fb4fd67e0 moved Code_Index, Random and Quickcheck before Main
haftmann
parents: 31186
diff changeset
   291
  Typerep.thy \
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   292
  $(SRC)/Provers/Arith/assoc_fold.ML \
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   293
  $(SRC)/Provers/Arith/cancel_numeral_factor.ML \
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   294
  $(SRC)/Provers/Arith/cancel_numerals.ML \
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   295
  $(SRC)/Provers/Arith/combine_numerals.ML \
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   296
  $(SRC)/Provers/Arith/extract_common_term.ML \
38047
9033c03cc214 consequence of directory renaming
blanchet
parents: 38021
diff changeset
   297
  Tools/ATP/atp_problem.ML \
39452
70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing;
blanchet
parents: 39432
diff changeset
   298
  Tools/ATP/atp_proof.ML \
38047
9033c03cc214 consequence of directory renaming
blanchet
parents: 38021
diff changeset
   299
  Tools/ATP/atp_systems.ML \
33318
ddd97d9dfbfb moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents: 33298
diff changeset
   300
  Tools/choice_specification.ML \
39564
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39505
diff changeset
   301
  Tools/code_evaluation.ML \
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31060
diff changeset
   302
  Tools/int_arith.ML \
36753
5cf4e9128f22 renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents: 36751
diff changeset
   303
  Tools/groebner.ML \
31055
2cf6efca6c71 proper structures for list and string code generation stuff
haftmann
parents: 31048
diff changeset
   304
  Tools/list_code.ML \
41463
edbf0a86fb1c adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents: 41426
diff changeset
   305
  Tools/list_to_set_comprehension.ML \
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31060
diff changeset
   306
  Tools/nat_numeral_simprocs.ML \
36915
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   307
  Tools/Nitpick/kodkod.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   308
  Tools/Nitpick/kodkod_sat.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   309
  Tools/Nitpick/nitpick.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   310
  Tools/Nitpick/nitpick_hol.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   311
  Tools/Nitpick/nitpick_isar.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   312
  Tools/Nitpick/nitpick_kodkod.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   313
  Tools/Nitpick/nitpick_model.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   314
  Tools/Nitpick/nitpick_mono.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   315
  Tools/Nitpick/nitpick_nut.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   316
  Tools/Nitpick/nitpick_peephole.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   317
  Tools/Nitpick/nitpick_preproc.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   318
  Tools/Nitpick/nitpick_rep.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   319
  Tools/Nitpick/nitpick_scope.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   320
  Tools/Nitpick/nitpick_tests.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   321
  Tools/Nitpick/nitpick_util.ML \
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   322
  Tools/numeral.ML \
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31060
diff changeset
   323
  Tools/numeral_simprocs.ML \
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   324
  Tools/numeral_syntax.ML \
40141
0e8a4e27a685 adding new predicate compiler files to the IsaMakefile
bulwahn
parents: 40123
diff changeset
   325
  Tools/Predicate_Compile/core_data.ML \
0e8a4e27a685 adding new predicate compiler files to the IsaMakefile
bulwahn
parents: 40123
diff changeset
   326
  Tools/Predicate_Compile/mode_inference.ML \
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33210
diff changeset
   327
  Tools/Predicate_Compile/predicate_compile_aux.ML \
36046
c3946372f556 putting compilation setup of predicate compiler in a separate file
bulwahn
parents: 36032
diff changeset
   328
  Tools/Predicate_Compile/predicate_compile_compilations.ML \
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33210
diff changeset
   329
  Tools/Predicate_Compile/predicate_compile_core.ML \
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33210
diff changeset
   330
  Tools/Predicate_Compile/predicate_compile_data.ML \
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33210
diff changeset
   331
  Tools/Predicate_Compile/predicate_compile_fun.ML \
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33210
diff changeset
   332
  Tools/Predicate_Compile/predicate_compile.ML \
40141
0e8a4e27a685 adding new predicate compiler files to the IsaMakefile
bulwahn
parents: 40123
diff changeset
   333
  Tools/Predicate_Compile/predicate_compile_proof.ML \
36032
dfd30b5b4e73 adding specialisation of predicates to the predicate compiler
bulwahn
parents: 35972
diff changeset
   334
  Tools/Predicate_Compile/predicate_compile_specialisation.ML \
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33210
diff changeset
   335
  Tools/Predicate_Compile/predicate_compile_pred.ML \
31260
4d273d043d59 separate module for quickcheck generators
haftmann
parents: 31205
diff changeset
   336
  Tools/quickcheck_generators.ML \
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   337
  Tools/Qelim/cooper.ML \
36803
2cad8904c4ff updated references to ML files
haftmann
parents: 36798
diff changeset
   338
  Tools/Qelim/cooper_procedure.ML \
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   339
  Tools/Qelim/qelim.ML \
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35151
diff changeset
   340
  Tools/Quotient/quotient_def.ML \
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35151
diff changeset
   341
  Tools/Quotient/quotient_info.ML \
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35151
diff changeset
   342
  Tools/Quotient/quotient_tacs.ML \
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35151
diff changeset
   343
  Tools/Quotient/quotient_term.ML \
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35151
diff changeset
   344
  Tools/Quotient/quotient_typ.ML \
31723
f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents: 31706
diff changeset
   345
  Tools/recdef.ML \
38394
3142c1e21a0e moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents: 38282
diff changeset
   346
  Tools/record.ML \
36753
5cf4e9128f22 renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents: 36751
diff changeset
   347
  Tools/semiring_normalizer.ML \
41042
8275f52ac991 load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents: 41023
diff changeset
   348
  Tools/Sledgehammer/async_manager.ML \
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41065
diff changeset
   349
  Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML \
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41065
diff changeset
   350
  Tools/Sledgehammer/sledgehammer_atp_translate.ML \
38986
e34c1b09bb5e shorten a few file names
blanchet
parents: 38942
diff changeset
   351
  Tools/Sledgehammer/sledgehammer_filter.ML \
e34c1b09bb5e shorten a few file names
blanchet
parents: 38942
diff changeset
   352
  Tools/Sledgehammer/sledgehammer_minimize.ML \
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35865
diff changeset
   353
  Tools/Sledgehammer/sledgehammer_isar.ML \
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41065
diff changeset
   354
  Tools/Sledgehammer/sledgehammer_provers.ML \
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41065
diff changeset
   355
  Tools/Sledgehammer/sledgehammer_run.ML \
35967
b9659daa5b4b add new file "sledgehammer_util.ML" to setup
blanchet
parents: 35892
diff changeset
   356
  Tools/Sledgehammer/sledgehammer_util.ML \
40420
552563ea3304 adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents: 40355
diff changeset
   357
  Tools/smallvalue_generators.ML \
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
   358
  Tools/SMT/smtlib_interface.ML \
40277
4e3a3461c1a6 added crafted list of SMT built-in constants
boehmes
parents: 40239
diff changeset
   359
  Tools/SMT/smt_builtin.ML \
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40420
diff changeset
   360
  Tools/SMT/smt_config.ML \
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41413
diff changeset
   361
  Tools/SMT/smt_datatypes.ML \
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40420
diff changeset
   362
  Tools/SMT/smt_failure.ML \
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
   363
  Tools/SMT/smt_monomorph.ML \
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
   364
  Tools/SMT/smt_normalize.ML \
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40141
diff changeset
   365
  Tools/SMT/smt_setup_solvers.ML \
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
   366
  Tools/SMT/smt_solver.ML \
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
   367
  Tools/SMT/smt_translate.ML \
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents: 40650
diff changeset
   368
  Tools/SMT/smt_utils.ML \
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
   369
  Tools/SMT/z3_interface.ML \
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
   370
  Tools/SMT/z3_model.ML \
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
   371
  Tools/SMT/z3_proof_literals.ML \
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents: 40650
diff changeset
   372
  Tools/SMT/z3_proof_methods.ML \
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
   373
  Tools/SMT/z3_proof_parser.ML \
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
   374
  Tools/SMT/z3_proof_reconstruction.ML \
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
   375
  Tools/SMT/z3_proof_tools.ML \
31055
2cf6efca6c71 proper structures for list and string code generation stuff
haftmann
parents: 31048
diff changeset
   376
  Tools/string_code.ML \
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   377
  Tools/string_syntax.ML \
33318
ddd97d9dfbfb moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents: 33298
diff changeset
   378
  Tools/transfer.ML \
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   379
  Tools/TFL/casesplit.ML \
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   380
  Tools/TFL/dcterm.ML \
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   381
  Tools/TFL/post.ML \
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   382
  Tools/TFL/rules.ML \
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   383
  Tools/TFL/tfl.ML \
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   384
  Tools/TFL/thms.ML \
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   385
  Tools/TFL/thry.ML \
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   386
  Tools/TFL/usyntax.ML \
28477
9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents: 28476
diff changeset
   387
  Tools/TFL/utils.ML
28401
d5f39173444c separate HOL-Main image
haftmann
parents: 28393
diff changeset
   388
d5f39173444c separate HOL-Main image
haftmann
parents: 28393
diff changeset
   389
$(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES)
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   390
	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
28401
d5f39173444c separate HOL-Main image
haftmann
parents: 28393
diff changeset
   391
34205
f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents: 34126
diff changeset
   392
HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \
30096
c5497842ee35 new theory of Archimedean fields
huffman
parents: 30049
diff changeset
   393
  Archimedean_Field.thy \
32733
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents: 32674
diff changeset
   394
  Complex.thy \
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28905
diff changeset
   395
  Complex_Main.thy \
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28905
diff changeset
   396
  Deriv.thy \
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28905
diff changeset
   397
  Fact.thy \
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   398
  GCD.thy \
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28905
diff changeset
   399
  Lim.thy \
31352
b3b534f06c2d add dependency on Limits.thy
huffman
parents: 31283
diff changeset
   400
  Limits.thy \
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28905
diff changeset
   401
  Ln.thy \
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28905
diff changeset
   402
  Log.thy \
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   403
  Lubs.thy \
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28905
diff changeset
   404
  MacLaurin.thy \
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28905
diff changeset
   405
  NthRoot.thy \
32733
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents: 32674
diff changeset
   406
  Parity.thy \
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents: 32674
diff changeset
   407
  RComplete.thy \
35372
ca158c7b1144 renamed theory Rational to Rat
haftmann
parents: 35329
diff changeset
   408
  Rat.thy \
32733
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents: 32674
diff changeset
   409
  Real.thy \
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents: 32674
diff changeset
   410
  RealDef.thy \
71618deaf777 moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents: 32674
diff changeset
   411
  RealVector.thy \
29197
6d4cb27ed19c adapted HOL source structure to distribution layout
haftmann
parents: 29181
diff changeset
   412
  SEQ.thy \
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28905
diff changeset
   413
  Series.thy \
33269
3b7e2dbbd684 New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents: 33083
diff changeset
   414
  SupInf.thy \
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28905
diff changeset
   415
  Taylor.thy \
40839
48e01d16dd17 activate subtyping/coercions in theory Complex_Main;
wenzelm
parents: 40837
diff changeset
   416
  Tools/SMT/smt_real.ML \
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28905
diff changeset
   417
  Tools/float_syntax.ML \
40839
48e01d16dd17 activate subtyping/coercions in theory Complex_Main;
wenzelm
parents: 40837
diff changeset
   418
  Transcendental.thy
34205
f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents: 34126
diff changeset
   419
f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents: 34126
diff changeset
   420
$(OUT)/HOL: ROOT.ML $(HOL_DEPENDENCIES)
f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents: 34126
diff changeset
   421
	@$(ISABELLE_TOOL) usedir -b -g true $(OUT)/Pure HOL
f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents: 34126
diff changeset
   422
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents: 7513
diff changeset
   423
10255
bb66874b4750 added HOL/Library, rearranged several files;
wenzelm
parents: 10214
diff changeset
   424
## HOL-Library
bb66874b4750 added HOL/Library, rearranged several files;
wenzelm
parents: 10214
diff changeset
   425
37691
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
   426
HOL-Library: HOL $(OUT)/HOL-Library
10255
bb66874b4750 added HOL/Library, rearranged several files;
wenzelm
parents: 10214
diff changeset
   427
38137
6fda94059baa renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents: 38119
diff changeset
   428
$(OUT)/HOL-Library: $(OUT)/HOL Library/ROOT.ML				\
37691
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
   429
  $(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML			\
37818
dd65033fed78 load cache_io before code generator; moved adhoc-overloading to generic tools
haftmann
parents: 37790
diff changeset
   430
  Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy		\
38137
6fda94059baa renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents: 38119
diff changeset
   431
  Library/AssocList.thy Library/BigO.thy Library/Binomial.thy		\
37968
52fdcb76c0af added Code_Natural.thy
haftmann
parents: 37921
diff changeset
   432
  Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy	\
37662
35c060043a5a repaired line ending
haftmann
parents: 37660
diff changeset
   433
  Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy	\
38137
6fda94059baa renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents: 38119
diff changeset
   434
  Library/Code_Integer.thy Library/Code_Natural.thy			\
38119
e00f970425e9 adding Code_Prolog theory to IsaMakefile and HOL-Library root file
bulwahn
parents: 38074
diff changeset
   435
  Library/Code_Prolog.thy Tools/Predicate_Compile/code_prolog.ML	\
37968
52fdcb76c0af added Code_Natural.thy
haftmann
parents: 37921
diff changeset
   436
  Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy	\
38137
6fda94059baa renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents: 38119
diff changeset
   437
  Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy	\
40650
d40b347d5b0b adding Enum to HOL-Main image and removing it from HOL-Library
bulwahn
parents: 40634
diff changeset
   438
  Library/Efficient_Nat.thy Library/Eval_Witness.thy 			\
37968
52fdcb76c0af added Code_Natural.thy
haftmann
parents: 37921
diff changeset
   439
  Library/Executable_Set.thy Library/Float.thy				\
52fdcb76c0af added Code_Natural.thy
haftmann
parents: 37921
diff changeset
   440
  Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
40672
abd4e7358847 replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents: 40582
diff changeset
   441
  Library/FrechetDeriv.thy Library/Cset.thy Library/FuncSet.thy		\
38622
86fc906dcd86 split and enriched theory SetsAndFunctions
haftmann
parents: 38539
diff changeset
   442
  Library/Function_Algebras.thy						\
37968
52fdcb76c0af added Code_Natural.thy
haftmann
parents: 37921
diff changeset
   443
  Library/Fundamental_Theorem_Algebra.thy Library/Glbs.thy		\
52fdcb76c0af added Code_Natural.thy
haftmann
parents: 37921
diff changeset
   444
  Library/Indicator_Function.thy Library/Infinite_Set.thy		\
52fdcb76c0af added Code_Natural.thy
haftmann
parents: 37921
diff changeset
   445
  Library/Inner_Product.thy Library/Kleene_Algebra.thy			\
37118
ccae4ecd67f4 eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML;
wenzelm
parents: 37024
diff changeset
   446
  Library/LaTeXsugar.thy Library/Lattice_Algebras.thy			\
ccae4ecd67f4 eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML;
wenzelm
parents: 37024
diff changeset
   447
  Library/Lattice_Syntax.thy Library/Library.thy			\
ccae4ecd67f4 eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML;
wenzelm
parents: 37024
diff changeset
   448
  Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy	\
37790
7fea92005066 uniform do notation for monads
krauss
parents: 37789
diff changeset
   449
  Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy	\
37818
dd65033fed78 load cache_io before code generator; moved adhoc-overloading to generic tools
haftmann
parents: 37790
diff changeset
   450
  Library/Multiset.thy Library/Nat_Bijection.thy			\
38137
6fda94059baa renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents: 38119
diff changeset
   451
  Library/Nat_Infinity.thy Library/Nested_Environment.thy		\
6fda94059baa renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents: 38119
diff changeset
   452
  Library/Numeral_Type.thy Library/OptionalSugar.thy			\
6fda94059baa renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents: 38119
diff changeset
   453
  Library/Order_Relation.thy Library/Permutation.thy			\
6fda94059baa renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents: 38119
diff changeset
   454
  Library/Permutations.thy Library/Poly_Deriv.thy			\
6fda94059baa renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents: 38119
diff changeset
   455
  Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy	\
6fda94059baa renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents: 38119
diff changeset
   456
  Library/Preorder.thy Library/Product_Vector.thy			\
6fda94059baa renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents: 38119
diff changeset
   457
  Library/Product_ord.thy Library/Product_plus.thy			\
40349
131cf8790a1c moved theory Quicksort from Library/ to ex/
haftmann
parents: 40281
diff changeset
   458
  Library/Quickcheck_Types.thy						\
37118
ccae4ecd67f4 eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML;
wenzelm
parents: 37024
diff changeset
   459
  Library/Quotient_List.thy Library/Quotient_Option.thy			\
ccae4ecd67f4 eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML;
wenzelm
parents: 37024
diff changeset
   460
  Library/Quotient_Product.thy Library/Quotient_Sum.thy			\
ccae4ecd67f4 eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML;
wenzelm
parents: 37024
diff changeset
   461
  Library/Quotient_Syntax.thy Library/Quotient_Type.thy			\
ccae4ecd67f4 eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML;
wenzelm
parents: 37024
diff changeset
   462
  Library/RBT.thy Library/RBT_Impl.thy Library/README.html		\
38622
86fc906dcd86 split and enriched theory SetsAndFunctions
haftmann
parents: 38539
diff changeset
   463
  Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy	\
86fc906dcd86 split and enriched theory SetsAndFunctions
haftmann
parents: 38539
diff changeset
   464
  Library/Reflection.thy Library/SML_Quickcheck.thy 			\
41474
60d091240485 renamed Sum_Of_Squares to Sum_of_Squares;
wenzelm
parents: 41465
diff changeset
   465
  Library/Sublist_Order.thy Library/Sum_of_Squares.thy			\
60d091240485 renamed Sum_Of_Squares to Sum_of_Squares;
wenzelm
parents: 41465
diff changeset
   466
  Library/Sum_of_Squares/sos_wrapper.ML					\
60d091240485 renamed Sum_Of_Squares to Sum_of_Squares;
wenzelm
parents: 41465
diff changeset
   467
  Library/Sum_of_Squares/sum_of_squares.ML				\
37118
ccae4ecd67f4 eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML;
wenzelm
parents: 37024
diff changeset
   468
  Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy		\
ccae4ecd67f4 eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML;
wenzelm
parents: 37024
diff changeset
   469
  Library/While_Combinator.thy Library/Zorn.thy				\
37818
dd65033fed78 load cache_io before code generator; moved adhoc-overloading to generic tools
haftmann
parents: 37790
diff changeset
   470
  $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML	\
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents: 37781
diff changeset
   471
  Library/reflection.ML Library/reify_data.ML				\
41906
e163d435ccf7 adding Lazysmallcheck prototype to HOL-Library
bulwahn
parents: 41892
diff changeset
   472
  Library/LSC.thy $(SRC)/HOL/Tools/LSC/lazysmallcheck.ML 		\
e163d435ccf7 adding Lazysmallcheck prototype to HOL-Library
bulwahn
parents: 41892
diff changeset
   473
  $(SRC)/HOL/Tools/LSC/LazySmallCheck.hs 				\
37691
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
   474
  Library/document/root.bib Library/document/root.tex
38137
6fda94059baa renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents: 38119
diff changeset
   475
	@cd Library; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL-Library
10255
bb66874b4750 added HOL/Library, rearranged several files;
wenzelm
parents: 10214
diff changeset
   476
bb66874b4750 added HOL/Library, rearranged several files;
wenzelm
parents: 10214
diff changeset
   477
31795
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 31771
diff changeset
   478
## HOL-Hahn_Banach
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   479
31795
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 31771
diff changeset
   480
HOL-Hahn_Banach: HOL $(LOG)/HOL-Hahn_Banach.gz
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   481
31795
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 31771
diff changeset
   482
$(LOG)/HOL-Hahn_Banach.gz: $(OUT)/HOL Hahn_Banach/Bounds.thy		\
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 31771
diff changeset
   483
  Hahn_Banach/Function_Norm.thy Hahn_Banach/Function_Order.thy		\
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 31771
diff changeset
   484
  Hahn_Banach/Hahn_Banach.thy Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	\
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 31771
diff changeset
   485
  Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Hahn_Banach/Linearform.thy	\
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 31771
diff changeset
   486
  Hahn_Banach/Normed_Space.thy Hahn_Banach/README.html			\
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 31771
diff changeset
   487
  Hahn_Banach/ROOT.ML Hahn_Banach/Subspace.thy				\
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 31771
diff changeset
   488
  Hahn_Banach/Vector_Space.thy Hahn_Banach/Zorn_Lemma.thy		\
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 31771
diff changeset
   489
  Hahn_Banach/document/root.bib Hahn_Banach/document/root.tex
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 31771
diff changeset
   490
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hahn_Banach
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   491
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   492
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   493
## HOL-Subst
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   494
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   495
HOL-Subst: HOL $(LOG)/HOL-Subst.gz
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   496
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   497
$(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.thy Subst/ROOT.ML		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   498
  Subst/Subst.thy Subst/UTerm.thy Subst/Unifier.thy Subst/Unify.thy
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   499
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Subst
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   500
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   501
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   502
## HOL-Induct
2473
3eb12c85846c minor tuning;
wenzelm
parents: 2448
diff changeset
   503
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   504
HOL-Induct: HOL $(LOG)/HOL-Induct.gz
3125
3f0ab2c306f7 Moved induction examples to directory Induct
paulson
parents: 3118
diff changeset
   505
33688
1a97dcd8dc6a moved old SList, LList, LFilter to AFP/Lazy-Lists-II;
wenzelm
parents: 33649
diff changeset
   506
$(LOG)/HOL-Induct.gz: $(OUT)/HOL Induct/Com.thy Induct/Comb.thy		\
1a97dcd8dc6a moved old SList, LList, LFilter to AFP/Lazy-Lists-II;
wenzelm
parents: 33649
diff changeset
   507
  Induct/Ordinals.thy Induct/PropLog.thy Induct/QuoNestedDataType.thy	\
1a97dcd8dc6a moved old SList, LList, LFilter to AFP/Lazy-Lists-II;
wenzelm
parents: 33649
diff changeset
   508
  Induct/QuoDataType.thy Induct/ROOT.ML Induct/Sexp.thy			\
35249
7024a8a8f36a more precise dependencies;
wenzelm
parents: 35222
diff changeset
   509
  Induct/Sigma_Algebra.thy Induct/ABexp.thy Induct/SList.thy		\
7024a8a8f36a more precise dependencies;
wenzelm
parents: 35222
diff changeset
   510
  Induct/Term.thy Induct/Tree.thy Induct/document/root.tex
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   511
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Induct
3125
3f0ab2c306f7 Moved induction examples to directory Induct
paulson
parents: 3118
diff changeset
   512
3f0ab2c306f7 Moved induction examples to directory Induct
paulson
parents: 3118
diff changeset
   513
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   514
## HOL-IMP
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   515
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   516
HOL-IMP: HOL $(LOG)/HOL-IMP.gz
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   517
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   518
$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Compiler0.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   519
  IMP/Compiler.thy IMP/Denotation.thy IMP/Expr.thy IMP/Hoare.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   520
  IMP/Natural.thy IMP/Examples.thy IMP/Transition.thy IMP/VC.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   521
  IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   522
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL IMP
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   523
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   524
8179
6a0b1037bab3 added forgotten rules to make IMPP
oheimb
parents: 8177
diff changeset
   525
## HOL-IMPP
6a0b1037bab3 added forgotten rules to make IMPP
oheimb
parents: 8177
diff changeset
   526
6a0b1037bab3 added forgotten rules to make IMPP
oheimb
parents: 8177
diff changeset
   527
HOL-IMPP: HOL $(LOG)/HOL-IMPP.gz
6a0b1037bab3 added forgotten rules to make IMPP
oheimb
parents: 8177
diff changeset
   528
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   529
$(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy		\
19803
aa2581752afb removed obsolete ML files;
wenzelm
parents: 19802
diff changeset
   530
  IMPP/Natural.thy IMPP/Hoare.thy IMPP/Misc.thy IMPP/EvenOdd.thy
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   531
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL IMPP
8179
6a0b1037bab3 added forgotten rules to make IMPP
oheimb
parents: 8177
diff changeset
   532
6a0b1037bab3 added forgotten rules to make IMPP
oheimb
parents: 8177
diff changeset
   533
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   534
## HOL-Import
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   535
19097
2fc1a6da9366 removed Import/lazy_scan.ML;
wenzelm
parents: 19085
diff changeset
   536
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
   537
  Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   538
  Import/HOL4Syntax.thy Import/HOL4Compat.thy Import/import_syntax.ML \
31723
f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents: 31706
diff changeset
   539
  Import/hol4rews.ML Import/import.ML Import/ROOT.ML
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   540
17323
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight
obua
parents: 17308
diff changeset
   541
IMPORTER_HOLLIGHT_FILES = Import/proof_kernel.ML Import/replay.ML \
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight
obua
parents: 17308
diff changeset
   542
  Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight
obua
parents: 17308
diff changeset
   543
  Import/HOL4Syntax.thy Import/HOLLightCompat.thy Import/import_syntax.ML \
31771
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   544
  Import/hol4rews.ML Import/import.ML Import/ROOT.ML
17323
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight
obua
parents: 17308
diff changeset
   545
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   546
HOL-Import: HOL $(LOG)/HOL-Import.gz
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   547
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   548
$(LOG)/HOL-Import.gz: $(OUT)/HOL $(IMPORTER_FILES)
37296
1fad5b94c0ae replaced ML pokes by explicit usedir -p;
wenzelm
parents: 37292
diff changeset
   549
	@$(ISABELLE_TOOL) usedir -p 0 $(OUT)/HOL Import
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   550
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   551
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   552
## HOL-Generate-HOL
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   553
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   554
HOL-Generate-HOL: HOL $(LOG)/HOL-Generate-HOL.gz
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   555
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   556
$(LOG)/HOL-Generate-HOL.gz: $(OUT)/HOL			\
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   557
  $(IMPORTER_FILES) Import/Generate-HOL/GenHOL4Base.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   558
  Import/Generate-HOL/GenHOL4Prob.thy					\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   559
  Import/Generate-HOL/GenHOL4Real.thy					\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   560
  Import/Generate-HOL/GenHOL4Vec.thy					\
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   561
  Import/Generate-HOL/GenHOL4Word32.thy Import/Generate-HOL/ROOT.ML
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   562
	@cd Import; $(ISABELLE_TOOL) usedir $(OUT)/HOL Generate-HOL
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   563
17460
7780d953598c generate: added HOL-Complex-Generate-HOLLight;
wenzelm
parents: 17430
diff changeset
   564
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   565
## HOL-Generate-HOLLight
17460
7780d953598c generate: added HOL-Complex-Generate-HOLLight;
wenzelm
parents: 17430
diff changeset
   566
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   567
HOL-Generate-HOLLight: HOL $(LOG)/HOL-Generate-HOLLight.gz
17323
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight
obua
parents: 17308
diff changeset
   568
37742
d8e7f473c3a1 tuned tabs
haftmann
parents: 37691
diff changeset
   569
$(LOG)/HOL-Generate-HOLLight.gz: $(OUT)/HOL				\
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   570
  $(IMPORTER_HOLLIGHT_FILES) Import/Generate-HOLLight/GenHOLLight.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   571
  Import/Generate-HOLLight/ROOT.ML
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   572
	@cd Import; $(ISABELLE_TOOL) usedir $(OUT)/HOL Generate-HOLLight
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   573
17460
7780d953598c generate: added HOL-Complex-Generate-HOLLight;
wenzelm
parents: 17430
diff changeset
   574
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   575
## HOL-Import-HOL
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   576
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   577
HOL4: HOL $(LOG)/HOL4.gz
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   578
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   579
HOL_IMPORT_FILES = arithmetic.imp bits.imp boolean_sequence.imp bool.imp \
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   580
  bword_arith.imp bword_bitop.imp bword_num.imp combin.imp divides.imp \
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   581
  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
   582
  numeral.imp num.imp one.imp operator.imp option.imp pair.imp poly.imp \
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   583
  powser.imp pred_set.imp prime.imp prim_rec.imp prob_algebra.imp \
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   584
  prob_canon.imp prob_extra.imp prob.imp prob_indep.imp prob_pseudo.imp \
23194
webertj
parents: 23193
diff changeset
   585
  prob_uniform.imp realax.imp real.imp relation.imp res_quan.imp \
webertj
parents: 23193
diff changeset
   586
  rich_list.imp \
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   587
  seq.imp state_transformer.imp sum.imp topology.imp transc.imp word32.imp \
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   588
  word_base.imp word_bitop.imp word_num.imp
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   589
37742
d8e7f473c3a1 tuned tabs
haftmann
parents: 37691
diff changeset
   590
$(LOG)/HOL4.gz: $(OUT)/HOL $(IMPORTER_FILES)				\
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   591
  $(HOL_IMPORT_FILES:%=Import/HOL/%) Import/HOL/HOL4Base.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   592
  Import/HOL/HOL4Prob.thy Import/HOL/HOL4Real.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   593
  Import/HOL/HOL4Vec.thy Import/HOL/HOL4Word32.thy Import/HOL/HOL4.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   594
  Import/HOL/ROOT.ML
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   595
	@cd Import/HOL; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL4
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   596
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   597
HOLLight: HOL $(LOG)/HOLLight.gz
17645
940371ea0ff3 added entry for running HOLLight
obua
parents: 17637
diff changeset
   598
37742
d8e7f473c3a1 tuned tabs
haftmann
parents: 37691
diff changeset
   599
$(LOG)/HOLLight.gz: $(OUT)/HOL $(IMPORTER_HOLLIGHT_FILES)		\
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   600
  Import/HOLLight/hollight.imp Import/HOLLight/HOLLight.thy		\
17645
940371ea0ff3 added entry for running HOLLight
obua
parents: 17637
diff changeset
   601
  Import/HOLLight/ROOT.ML
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   602
	@cd Import/HOLLight; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOLLight
17645
940371ea0ff3 added entry for running HOLLight
obua
parents: 17637
diff changeset
   603
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   604
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   605
## HOL-Number_Theory
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents: 31706
diff changeset
   606
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   607
HOL-Number_Theory: HOL $(LOG)/HOL-Number_Theory.gz
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents: 31706
diff changeset
   608
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   609
$(LOG)/HOL-Number_Theory.gz: $(OUT)/HOL $(ALGEBRA_DEPENDENCIES) \
31771
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   610
  Library/Multiset.thy \
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   611
  Number_Theory/Binomial.thy \
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   612
  Number_Theory/Cong.thy \
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   613
  Number_Theory/Fib.thy \
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   614
  Number_Theory/MiscAlgebra.thy \
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   615
  Number_Theory/Number_Theory.thy \
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   616
  Number_Theory/Residues.thy \
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   617
  Number_Theory/UniqueFactorization.thy  \
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   618
  Number_Theory/ROOT.ML
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   619
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Number_Theory
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents: 31706
diff changeset
   620
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents: 31706
diff changeset
   621
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   622
## HOL-Old_Number_Theory
9510
dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied
paulson
parents: 9481
diff changeset
   623
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   624
HOL-Old_Number_Theory: HOL $(LOG)/HOL-Old_Number_Theory.gz
9510
dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied
paulson
parents: 9481
diff changeset
   625
37021
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   626
$(LOG)/HOL-Old_Number_Theory.gz: $(OUT)/HOL Library/Permutation.thy	\
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   627
  Old_Number_Theory/Primes.thy Old_Number_Theory/Fib.thy		\
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   628
  Old_Number_Theory/Factorization.thy Old_Number_Theory/BijectionRel.thy\
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   629
  Old_Number_Theory/Chinese.thy Old_Number_Theory/EulerFermat.thy	\
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   630
  Old_Number_Theory/IntFact.thy Old_Number_Theory/IntPrimes.thy		\
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   631
  Old_Number_Theory/WilsonBij.thy Old_Number_Theory/WilsonRuss.thy	\
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   632
  Old_Number_Theory/Finite2.thy Old_Number_Theory/Int2.thy		\
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   633
  Old_Number_Theory/EvenOdd.thy Old_Number_Theory/Residues.thy		\
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   634
  Old_Number_Theory/Euler.thy Old_Number_Theory/Gauss.thy		\
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   635
  Old_Number_Theory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy	\
37021
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   636
  Old_Number_Theory/Legacy_GCD.thy Old_Number_Theory/Pocklington.thy	\
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   637
  Old_Number_Theory/ROOT.ML
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   638
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Old_Number_Theory
9510
dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied
paulson
parents: 9481
diff changeset
   639
dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied
paulson
parents: 9481
diff changeset
   640
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   641
## HOL-Hoare
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   642
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   643
HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   644
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   645
$(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.thy Hoare/Examples.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   646
  Hoare/Hoare.thy Hoare/hoare_tac.ML Hoare/Heap.thy			\
35319
4140f31b2ed2 dropped session W0; c.f. MiniML in AFP
haftmann
parents: 35249
diff changeset
   647
  Hoare/Hoare_Logic.thy	Hoare/Hoare_Logic_Abort.thy			\
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   648
  Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy Hoare/ROOT.ML		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   649
  Hoare/ExamplesAbort.thy Hoare/HeapSyntaxAbort.thy			\
35319
4140f31b2ed2 dropped session W0; c.f. MiniML in AFP
haftmann
parents: 35249
diff changeset
   650
  Hoare/SchorrWaite.thy Hoare/Separation.thy				\
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   651
  Hoare/SepLogHeap.thy Hoare/document/root.tex Hoare/document/root.bib
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   652
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Hoare
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   653
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   654
32621
a073cb249a06 theory entry point for session Hoare_Parallel (now also with proper underscore)
haftmann
parents: 32618
diff changeset
   655
## HOL-Hoare_Parallel
12996
7ac0a7e306db Completed annonce of HoareParallel
prensani
parents: 12951
diff changeset
   656
32621
a073cb249a06 theory entry point for session Hoare_Parallel (now also with proper underscore)
haftmann
parents: 32618
diff changeset
   657
HOL-Hoare_Parallel: HOL $(LOG)/HOL-Hoare_Parallel.gz
12996
7ac0a7e306db Completed annonce of HoareParallel
prensani
parents: 12951
diff changeset
   658
32621
a073cb249a06 theory entry point for session Hoare_Parallel (now also with proper underscore)
haftmann
parents: 32618
diff changeset
   659
$(LOG)/HOL-Hoare_Parallel.gz: $(OUT)/HOL Hoare_Parallel/Gar_Coll.thy	\
33439
f5d95787224f more accurate dependencies;
wenzelm
parents: 33437
diff changeset
   660
  Hoare_Parallel/Graph.thy Hoare_Parallel/Hoare_Parallel.thy		\
f5d95787224f more accurate dependencies;
wenzelm
parents: 33437
diff changeset
   661
  Hoare_Parallel/Mul_Gar_Coll.thy Hoare_Parallel/OG_Com.thy		\
f5d95787224f more accurate dependencies;
wenzelm
parents: 33437
diff changeset
   662
  Hoare_Parallel/OG_Examples.thy Hoare_Parallel/OG_Hoare.thy		\
f5d95787224f more accurate dependencies;
wenzelm
parents: 33437
diff changeset
   663
  Hoare_Parallel/OG_Syntax.thy Hoare_Parallel/OG_Tactics.thy		\
f5d95787224f more accurate dependencies;
wenzelm
parents: 33437
diff changeset
   664
  Hoare_Parallel/OG_Tran.thy Hoare_Parallel/Quote_Antiquote.thy		\
f5d95787224f more accurate dependencies;
wenzelm
parents: 33437
diff changeset
   665
  Hoare_Parallel/RG_Com.thy Hoare_Parallel/RG_Examples.thy		\
f5d95787224f more accurate dependencies;
wenzelm
parents: 33437
diff changeset
   666
  Hoare_Parallel/RG_Hoare.thy Hoare_Parallel/RG_Syntax.thy		\
f5d95787224f more accurate dependencies;
wenzelm
parents: 33437
diff changeset
   667
  Hoare_Parallel/RG_Tran.thy Hoare_Parallel/ROOT.ML			\
f5d95787224f more accurate dependencies;
wenzelm
parents: 33437
diff changeset
   668
  Hoare_Parallel/document/root.tex Hoare_Parallel/document/root.bib
32621
a073cb249a06 theory entry point for session Hoare_Parallel (now also with proper underscore)
haftmann
parents: 32618
diff changeset
   669
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hoare_Parallel
12996
7ac0a7e306db Completed annonce of HoareParallel
prensani
parents: 12951
diff changeset
   670
7ac0a7e306db Completed annonce of HoareParallel
prensani
parents: 12951
diff changeset
   671
37747
3a699743bcba more accurate dependencies
haftmann
parents: 37742
diff changeset
   672
## HOL-Library-Codegenerator_Test
37691
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
   673
37747
3a699743bcba more accurate dependencies
haftmann
parents: 37742
diff changeset
   674
HOL-Library-Codegenerator_Test: HOL-Library $(LOG)/HOL-Library-Codegenerator_Test.gz
37691
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
   675
37747
3a699743bcba more accurate dependencies
haftmann
parents: 37742
diff changeset
   676
$(LOG)/HOL-Library-Codegenerator_Test.gz: $(OUT)/HOL-Library		\
37742
d8e7f473c3a1 tuned tabs
haftmann
parents: 37691
diff changeset
   677
  Codegenerator_Test/ROOT.ML 						\
d8e7f473c3a1 tuned tabs
haftmann
parents: 37691
diff changeset
   678
  Codegenerator_Test/Candidates.thy					\
37691
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
   679
  Codegenerator_Test/Candidates_Pretty.thy				\
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
   680
  Codegenerator_Test/Generate.thy					\
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
   681
  Codegenerator_Test/Generate_Pretty.thy
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
   682
	@$(ISABELLE_TOOL) usedir -d false -g false -i false $(OUT)/HOL-Library Codegenerator_Test
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
   683
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
   684
33027
9cf389429f6d modernized session Metis_Examples;
wenzelm
parents: 33026
diff changeset
   685
## HOL-Metis_Examples
23449
dd874e6a3282 integration of Metis prover
paulson
parents: 23445
diff changeset
   686
33027
9cf389429f6d modernized session Metis_Examples;
wenzelm
parents: 33026
diff changeset
   687
HOL-Metis_Examples: HOL $(LOG)/HOL-Metis_Examples.gz
23449
dd874e6a3282 integration of Metis prover
paulson
parents: 23445
diff changeset
   688
41144
509e51b7509a example tuning
blanchet
parents: 41112
diff changeset
   689
$(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML \
509e51b7509a example tuning
blanchet
parents: 41112
diff changeset
   690
  Metis_Examples/Abstraction.thy Metis_Examples/BigO.thy \
509e51b7509a example tuning
blanchet
parents: 41112
diff changeset
   691
  Metis_Examples/BT.thy Metis_Examples/HO_Reas.thy \
509e51b7509a example tuning
blanchet
parents: 41112
diff changeset
   692
  Metis_Examples/Message.thy Metis_Examples/Tarski.thy \
509e51b7509a example tuning
blanchet
parents: 41112
diff changeset
   693
  Metis_Examples/TransClosure.thy Metis_Examples/set.thy
33027
9cf389429f6d modernized session Metis_Examples;
wenzelm
parents: 33026
diff changeset
   694
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples
23449
dd874e6a3282 integration of Metis prover
paulson
parents: 23445
diff changeset
   695
dd874e6a3282 integration of Metis prover
paulson
parents: 23445
diff changeset
   696
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents: 33192
diff changeset
   697
## HOL-Nitpick_Examples
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents: 33192
diff changeset
   698
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents: 33192
diff changeset
   699
HOL-Nitpick_Examples: HOL $(LOG)/HOL-Nitpick_Examples.gz
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents: 33192
diff changeset
   700
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34069
diff changeset
   701
$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34069
diff changeset
   702
  Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \
35076
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35070
diff changeset
   703
  Nitpick_Examples/Hotel_Nits.thy Nitpick_Examples/Induct_Nits.thy \
cc19e2aef17e added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents: 35070
diff changeset
   704
  Nitpick_Examples/Integer_Nits.thy Nitpick_Examples/Manual_Nits.thy \
39221
70fd4a3c41ed remove "minipick" (the toy version of Nitpick) and some tests;
blanchet
parents: 39048
diff changeset
   705
  Nitpick_Examples/Mono_Nits.thy Nitpick_Examples/Nitpick_Examples.thy \
70fd4a3c41ed remove "minipick" (the toy version of Nitpick) and some tests;
blanchet
parents: 39048
diff changeset
   706
  Nitpick_Examples/Pattern_Nits.thy Nitpick_Examples/Record_Nits.thy \
70fd4a3c41ed remove "minipick" (the toy version of Nitpick) and some tests;
blanchet
parents: 39048
diff changeset
   707
  Nitpick_Examples/Refute_Nits.thy Nitpick_Examples/Special_Nits.thy \
70fd4a3c41ed remove "minipick" (the toy version of Nitpick) and some tests;
blanchet
parents: 39048
diff changeset
   708
  Nitpick_Examples/Tests_Nits.thy Nitpick_Examples/Typedef_Nits.thy
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents: 33192
diff changeset
   709
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents: 33192
diff changeset
   710
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents: 33192
diff changeset
   711
7999
7acf6eb8eec1 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents: 7985
diff changeset
   712
## HOL-Algebra
7acf6eb8eec1 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents: 7985
diff changeset
   713
33439
f5d95787224f more accurate dependencies;
wenzelm
parents: 33437
diff changeset
   714
HOL-Algebra: HOL $(OUT)/HOL-Algebra
7999
7acf6eb8eec1 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents: 7985
diff changeset
   715
31771
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   716
ALGEBRA_DEPENDENCIES = $(OUT)/HOL \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   717
  Algebra/ROOT.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   718
  Library/Binomial.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   719
  Library/FuncSet.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   720
  Library/Multiset.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   721
  Library/Permutation.thy \
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   722
  Number_Theory/Primes.thy \
31771
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   723
  Algebra/AbelCoset.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   724
  Algebra/Bij.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   725
  Algebra/Congruence.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   726
  Algebra/Coset.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   727
  Algebra/Divisibility.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   728
  Algebra/Exponent.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   729
  Algebra/FiniteProduct.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   730
  Algebra/Group.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   731
  Algebra/Ideal.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   732
  Algebra/IntRing.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   733
  Algebra/Lattice.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   734
  Algebra/Module.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   735
  Algebra/QuotRing.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   736
  Algebra/Ring.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   737
  Algebra/RingHom.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   738
  Algebra/Sylow.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   739
  Algebra/UnivPoly.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   740
  Algebra/abstract/Abstract.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   741
  Algebra/abstract/Factor.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   742
  Algebra/abstract/Field.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   743
  Algebra/abstract/Ideal2.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   744
  Algebra/abstract/PID.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   745
  Algebra/abstract/Ring2.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   746
  Algebra/abstract/RingHomo.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   747
  Algebra/document/root.tex \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   748
  Algebra/document/root.tex \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   749
  Algebra/poly/LongDiv.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   750
  Algebra/poly/PolyHomo.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   751
  Algebra/poly/Polynomial.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   752
  Algebra/poly/UnivPoly2.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   753
  Algebra/ringsimp.ML
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   754
33448
7f716a975ada more accurate dependencies;
wenzelm
parents: 33439
diff changeset
   755
$(OUT)/HOL-Algebra: $(ALGEBRA_DEPENDENCIES)
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   756
	@cd Algebra; $(ISABELLE_TOOL) usedir -b -g true -V outline=/proof,/ML $(OUT)/HOL HOL-Algebra
7999
7acf6eb8eec1 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents: 7985
diff changeset
   757
27477
c64736fe2a1f more precise dependencies for HOL-Word and HOL-NSA;
wenzelm
parents: 27470
diff changeset
   758
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   759
## HOL-Auth
3819
5a6a6f18b109 added TLA stuff;
wenzelm
parents: 3616
diff changeset
   760
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   761
HOL-Auth: HOL $(LOG)/HOL-Auth.gz
3819
5a6a6f18b109 added TLA stuff;
wenzelm
parents: 3616
diff changeset
   762
28098
c92850d2d16c Replaced Library/NatPair by Nat_Int_Bij.
nipkow
parents: 28054
diff changeset
   763
$(LOG)/HOL-Auth.gz: $(OUT)/HOL 						\
37021
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   764
  Auth/Auth_Shared.thy Auth/Auth_Public.thy Auth/All_Symmetric.thy	\
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   765
  Auth/Guard/Auth_Guard_Shared.thy					\
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   766
  Auth/Guard/Auth_Guard_Public.thy					\
32632
8ae912371831 added session entry point theories
haftmann
parents: 32624
diff changeset
   767
  Auth/Smartcard/Auth_Smartcard.thy Auth/All_Symmetric.thy		\
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   768
  Auth/CertifiedEmail.thy Auth/Event.thy Auth/Message.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   769
  Auth/NS_Public.thy Auth/NS_Public_Bad.thy Auth/NS_Shared.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   770
  Auth/OtwayRees.thy Auth/OtwayReesBella.thy Auth/OtwayRees_AN.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   771
  Auth/OtwayRees_Bad.thy Auth/Public.thy Auth/ROOT.ML Auth/Recur.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   772
  Auth/Shared.thy Auth/TLS.thy Auth/WooLam.thy Auth/Kerberos_BAN.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   773
  Auth/Kerberos_BAN_Gets.thy Auth/KerberosIV.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   774
  Auth/KerberosIV_Gets.thy Auth/KerberosV.thy Auth/Yahalom.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   775
  Auth/Yahalom2.thy Auth/Yahalom_Bad.thy Auth/ZhouGollmann.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   776
  Auth/Guard/Analz.thy Auth/Guard/Extensions.thy Auth/Guard/GuardK.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   777
  Auth/Guard/Guard_Public.thy Auth/Guard/Guard_Shared.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   778
  Auth/Guard/Guard.thy Auth/Guard/List_Msg.thy				\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   779
  Auth/Guard/Guard_NS_Public.thy Auth/Guard/Guard_OtwayRees.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   780
  Auth/Guard/P1.thy Auth/Guard/P2.thy Auth/Guard/Proto.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   781
  Auth/Guard/Guard_Yahalom.thy Auth/Smartcard/EventSC.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   782
  Auth/Smartcard/ShoupRubinBella.thy Auth/Smartcard/ShoupRubin.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   783
  Auth/Smartcard/Smartcard.thy Auth/document/root.tex
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   784
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Auth
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   785
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   786
4777
379f32b0ae40 New target HOL-UNITY
paulson
parents: 4729
diff changeset
   787
## HOL-UNITY
379f32b0ae40 New target HOL-UNITY
paulson
parents: 4729
diff changeset
   788
379f32b0ae40 New target HOL-UNITY
paulson
parents: 4729
diff changeset
   789
HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz
379f32b0ae40 New target HOL-UNITY
paulson
parents: 4729
diff changeset
   790
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   791
$(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML	\
41892
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;
wenzelm
parents: 41854
diff changeset
   792
  UNITY/UNITY_Main.thy UNITY/UNITY_tactics.ML UNITY/Comp.thy		\
2386fb64feaf eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;
wenzelm
parents: 41854
diff changeset
   793
  UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy			\
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   794
  UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy UNITY/Guar.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   795
  UNITY/Lift_prog.thy UNITY/ListOrder.thy UNITY/ProgressSets.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   796
  UNITY/PPROD.thy UNITY/Project.thy UNITY/Rename.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   797
  UNITY/Transformers.thy UNITY/SubstAx.thy UNITY/UNITY.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   798
  UNITY/Union.thy UNITY/WFair.thy UNITY/Simple/Channel.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   799
  UNITY/Simple/Common.thy UNITY/Simple/Deadlock.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   800
  UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy				\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   801
  UNITY/Simple/NSP_Bad.thy UNITY/Simple/Network.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   802
  UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   803
  UNITY/Simple/Token.thy UNITY/Comp/Alloc.thy UNITY/Comp/AllocBase.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   804
  UNITY/Comp/AllocImpl.thy UNITY/Comp/Client.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   805
  UNITY/Comp/Counter.thy UNITY/Comp/Counterc.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   806
  UNITY/Comp/Handshake.thy UNITY/Comp/PriorityAux.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   807
  UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   808
  UNITY/Comp/TimerArray.thy UNITY/document/root.tex
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   809
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL UNITY
4777
379f32b0ae40 New target HOL-UNITY
paulson
parents: 4729
diff changeset
   810
379f32b0ae40 New target HOL-UNITY
paulson
parents: 4729
diff changeset
   811
10966
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
   812
## HOL-Unix
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
   813
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
   814
HOL-Unix: HOL $(LOG)/HOL-Unix.gz
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
   815
37742
d8e7f473c3a1 tuned tabs
haftmann
parents: 37691
diff changeset
   816
$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy		\
d8e7f473c3a1 tuned tabs
haftmann
parents: 37691
diff changeset
   817
  Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy			\
10966
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
   818
  Unix/document/root.bib Unix/document/root.tex
39156
b4f18ac786fa modernized session ROOT setup;
wenzelm
parents: 39048
diff changeset
   819
	@$(ISABELLE_TOOL) usedir -m no_brackets -m no_type_brackets $(OUT)/HOL Unix
10966
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
   820
27477
c64736fe2a1f more precise dependencies for HOL-Word and HOL-NSA;
wenzelm
parents: 27470
diff changeset
   821
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents: 19192
diff changeset
   822
## HOL-ZF
778507520684 Added HOL-ZF to Isabelle.
obua
parents: 19192
diff changeset
   823
778507520684 Added HOL-ZF to Isabelle.
obua
parents: 19192
diff changeset
   824
HOL-ZF: HOL $(LOG)/HOL-ZF.gz
778507520684 Added HOL-ZF to Isabelle.
obua
parents: 19192
diff changeset
   825
39306
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   826
$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/LProd.thy \
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   827
  ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   828
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF
10966
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
   829
27477
c64736fe2a1f more precise dependencies for HOL-Word and HOL-NSA;
wenzelm
parents: 27470
diff changeset
   830
29399
ebcd69a00872 split of Imperative_HOL theories from HOL-Library
haftmann
parents: 29197
diff changeset
   831
## HOL-Imperative_HOL
ebcd69a00872 split of Imperative_HOL theories from HOL-Library
haftmann
parents: 29197
diff changeset
   832
ebcd69a00872 split of Imperative_HOL theories from HOL-Library
haftmann
parents: 29197
diff changeset
   833
HOL-Imperative_HOL: HOL $(LOG)/HOL-Imperative_HOL.gz
ebcd69a00872 split of Imperative_HOL theories from HOL-Library
haftmann
parents: 29197
diff changeset
   834
39306
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   835
$(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   836
  Imperative_HOL/Array.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   837
  Imperative_HOL/Heap.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   838
  Imperative_HOL/Heap_Monad.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   839
  Imperative_HOL/Imperative_HOL.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   840
  Imperative_HOL/Imperative_HOL_ex.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   841
  Imperative_HOL/Mrec.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   842
  Imperative_HOL/Ref.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   843
  Imperative_HOL/ROOT.ML \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   844
  Imperative_HOL/ex/Imperative_Quicksort.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   845
  Imperative_HOL/ex/Imperative_Reverse.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   846
  Imperative_HOL/ex/Linked_Lists.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   847
  Imperative_HOL/ex/SatChecker.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   848
  Imperative_HOL/ex/Sorted_List.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   849
  Imperative_HOL/ex/Subarray.thy \
30689
b14b2cc4e25e moved Imperative_HOL examples to Imperative_HOL/ex
haftmann
parents: 30654
diff changeset
   850
  Imperative_HOL/ex/Sublist.thy
39306
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   851
	@$(ISABELLE_TOOL) usedir -g true -m iff -m no_brackets $(OUT)/HOL Imperative_HOL
29399
ebcd69a00872 split of Imperative_HOL theories from HOL-Library
haftmann
parents: 29197
diff changeset
   852
ebcd69a00872 split of Imperative_HOL theories from HOL-Library
haftmann
parents: 29197
diff changeset
   853
29823
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
   854
## HOL-Decision_Procs
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
   855
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
   856
HOL-Decision_Procs: HOL $(LOG)/HOL-Decision_Procs.gz
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
   857
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
   858
$(LOG)/HOL-Decision_Procs.gz: $(OUT)/HOL \
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
   859
  Decision_Procs/Approximation.thy \
33356
9157d0f9f00e moved Commutative_Ring into session Decision_Procs
haftmann
parents: 33348
diff changeset
   860
  Decision_Procs/Commutative_Ring.thy \
9157d0f9f00e moved Commutative_Ring into session Decision_Procs
haftmann
parents: 33348
diff changeset
   861
  Decision_Procs/Commutative_Ring_Complete.thy \
29823
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
   862
  Decision_Procs/Cooper.thy \
35053
43175817d83b more precise dependencies;
wenzelm
parents: 35050
diff changeset
   863
  Decision_Procs/Decision_Procs.thy \
29823
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
   864
  Decision_Procs/Dense_Linear_Order.thy \
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
   865
  Decision_Procs/Ferrack.thy \
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
   866
  Decision_Procs/MIR.thy \
35053
43175817d83b more precise dependencies;
wenzelm
parents: 35050
diff changeset
   867
  Decision_Procs/Parametric_Ferrante_Rackoff.thy \
43175817d83b more precise dependencies;
wenzelm
parents: 35050
diff changeset
   868
  Decision_Procs/Polynomial_List.thy \
37120
5df087c6ce94 moved ML files where they are actually used;
wenzelm
parents: 37118
diff changeset
   869
  Decision_Procs/ROOT.ML \
35053
43175817d83b more precise dependencies;
wenzelm
parents: 35050
diff changeset
   870
  Decision_Procs/Reflected_Multivariate_Polynomial.thy \
43175817d83b more precise dependencies;
wenzelm
parents: 35050
diff changeset
   871
  Decision_Procs/commutative_ring_tac.ML \
43175817d83b more precise dependencies;
wenzelm
parents: 35050
diff changeset
   872
  Decision_Procs/cooper_tac.ML \
30429
39acdf031548 moved Decision_Procs examples to Decision_Procs/ex
haftmann
parents: 30400
diff changeset
   873
  Decision_Procs/ex/Approximation_Ex.thy \
33356
9157d0f9f00e moved Commutative_Ring into session Decision_Procs
haftmann
parents: 33348
diff changeset
   874
  Decision_Procs/ex/Commutative_Ring_Ex.thy \
35053
43175817d83b more precise dependencies;
wenzelm
parents: 35050
diff changeset
   875
  Decision_Procs/ex/Dense_Linear_Order_Ex.thy \
43175817d83b more precise dependencies;
wenzelm
parents: 35050
diff changeset
   876
  Decision_Procs/ferrack_tac.ML \
37120
5df087c6ce94 moved ML files where they are actually used;
wenzelm
parents: 37118
diff changeset
   877
  Decision_Procs/ferrante_rackoff.ML \
5df087c6ce94 moved ML files where they are actually used;
wenzelm
parents: 37118
diff changeset
   878
  Decision_Procs/ferrante_rackoff_data.ML \
5df087c6ce94 moved ML files where they are actually used;
wenzelm
parents: 37118
diff changeset
   879
  Decision_Procs/langford.ML \
5df087c6ce94 moved ML files where they are actually used;
wenzelm
parents: 37118
diff changeset
   880
  Decision_Procs/langford_data.ML \
5df087c6ce94 moved ML files where they are actually used;
wenzelm
parents: 37118
diff changeset
   881
  Decision_Procs/mir_tac.ML
29823
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
   882
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Decision_Procs
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
   883
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
   884
39157
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   885
## HOL-Proofs
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   886
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   887
HOL-Proofs: Pure $(OUT)/HOL-Proofs
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   888
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   889
$(OUT)/HOL-Proofs: main.ML $(MAIN_DEPENDENCIES)
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   890
	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true -p 2 -q 0 $(OUT)/Pure HOL-Proofs
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   891
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   892
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   893
## HOL-Proofs-ex
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   894
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   895
HOL-Proofs-ex: HOL-Proofs $(LOG)/HOL-Proofs-ex.gz
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   896
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   897
$(LOG)/HOL-Proofs-ex.gz: $(OUT)/HOL-Proofs			\
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   898
  Proofs/ex/ROOT.ML Proofs/ex/Hilbert_Classical.thy
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   899
	@cd Proofs; $(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs ex
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   900
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   901
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   902
## HOL-Proofs-Extraction
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   903
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   904
HOL-Proofs-Extraction: HOL-Proofs $(LOG)/HOL-Proofs-Extraction.gz
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   905
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   906
$(LOG)/HOL-Proofs-Extraction.gz: $(OUT)/HOL-Proofs		\
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   907
  Library/Efficient_Nat.thy Proofs/Extraction/Euclid.thy	\
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   908
  Proofs/Extraction/Greatest_Common_Divisor.thy			\
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   909
  Proofs/Extraction/Higman.thy Proofs/Extraction/Pigeonhole.thy	\
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   910
  Proofs/Extraction/QuotRem.thy Proofs/Extraction/ROOT.ML	\
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   911
  Proofs/Extraction/Util.thy Proofs/Extraction/Warshall.thy	\
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   912
  Proofs/Extraction/document/root.tex				\
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   913
  Proofs/Extraction/document/root.bib
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   914
	@cd Proofs; $(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs Extraction
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   915
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   916
34205
f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents: 34126
diff changeset
   917
## HOL-Proofs-Lambda
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   918
34205
f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents: 34126
diff changeset
   919
HOL-Proofs-Lambda: HOL-Proofs $(LOG)/HOL-Proofs-Lambda.gz
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   920
39157
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   921
$(LOG)/HOL-Proofs-Lambda.gz: $(OUT)/HOL-Proofs				\
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   922
  Proofs/Lambda/Commutation.thy Proofs/Lambda/Eta.thy			\
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   923
  Proofs/Lambda/InductTermi.thy Proofs/Lambda/Lambda.thy		\
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   924
  Proofs/Lambda/ListApplication.thy Proofs/Lambda/ListBeta.thy		\
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   925
  Proofs/Lambda/ListOrder.thy Proofs/Lambda/NormalForm.thy		\
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   926
  Proofs/Lambda/ParRed.thy Proofs/Lambda/Standardization.thy		\
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   927
  Proofs/Lambda/StrongNorm.thy Proofs/Lambda/Type.thy			\
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   928
  Proofs/Lambda/WeakNorm.thy Proofs/Lambda/ROOT.ML			\
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   929
  Proofs/Lambda/document/root.bib Proofs/Lambda/document/root.tex
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
   930
	@cd Proofs; $(ISABELLE_TOOL) usedir -g true -m no_brackets -p 2 -q 0 $(OUT)/HOL-Proofs Lambda
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   931
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   932
9015
8006e9009621 added HOL/Prolog
oheimb
parents: 8958
diff changeset
   933
## HOL-Prolog
8006e9009621 added HOL/Prolog
oheimb
parents: 8958
diff changeset
   934
8006e9009621 added HOL/Prolog
oheimb
parents: 8958
diff changeset
   935
HOL-Prolog: HOL $(LOG)/HOL-Prolog.gz
8006e9009621 added HOL/Prolog
oheimb
parents: 8958
diff changeset
   936
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   937
$(LOG)/HOL-Prolog.gz: $(OUT)/HOL Prolog/ROOT.ML Prolog/prolog.ML	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   938
  Prolog/HOHH.thy Prolog/Test.thy Prolog/Func.thy Prolog/Type.thy
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   939
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Prolog
9015
8006e9009621 added HOL/Prolog
oheimb
parents: 8958
diff changeset
   940
8006e9009621 added HOL/Prolog
oheimb
parents: 8958
diff changeset
   941
8012
bbdf3c51c3b8 Added MicroJava
nipkow
parents: 8008
diff changeset
   942
## HOL-MicroJava
bbdf3c51c3b8 Added MicroJava
nipkow
parents: 8008
diff changeset
   943
bbdf3c51c3b8 Added MicroJava
nipkow
parents: 8008
diff changeset
   944
HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
bbdf3c51c3b8 Added MicroJava
nipkow
parents: 8008
diff changeset
   945
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   946
$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL Library/Executable_Set.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   947
  MicroJava/ROOT.ML MicroJava/Comp/AuxLemmas.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   948
  MicroJava/Comp/CorrComp.thy MicroJava/Comp/CorrCompTp.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   949
  MicroJava/Comp/DefsComp.thy MicroJava/Comp/Index.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   950
  MicroJava/Comp/LemmasComp.thy MicroJava/Comp/NatCanonify.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   951
  MicroJava/Comp/TranslComp.thy MicroJava/Comp/TranslCompTp.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   952
  MicroJava/Comp/TypeInf.thy MicroJava/J/Conform.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   953
  MicroJava/J/Eval.thy MicroJava/J/JBasis.thy				\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   954
  MicroJava/J/JTypeSafe.thy MicroJava/J/Decl.thy MicroJava/J/State.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   955
  MicroJava/J/Term.thy MicroJava/J/Type.thy MicroJava/J/TypeRel.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   956
  MicroJava/J/WellForm.thy MicroJava/J/Value.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   957
  MicroJava/J/WellType.thy MicroJava/J/Example.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   958
  MicroJava/J/JListExample.thy MicroJava/JVM/JVMExec.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   959
  MicroJava/JVM/JVMInstructions.thy MicroJava/JVM/JVMState.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   960
  MicroJava/JVM/JVMExecInstr.thy MicroJava/JVM/JVMListExample.thy	\
33954
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents: 33820
diff changeset
   961
  MicroJava/JVM/JVMExceptions.thy MicroJava/DFA/Abstract_BV.thy		\
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents: 33820
diff changeset
   962
  MicroJava/DFA/Err.thy MicroJava/DFA/Kildall.thy			\
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents: 33820
diff changeset
   963
  MicroJava/DFA/LBVComplete.thy MicroJava/DFA/LBVCorrect.thy		\
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents: 33820
diff changeset
   964
  MicroJava/DFA/LBVSpec.thy MicroJava/DFA/Listn.thy			\
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents: 33820
diff changeset
   965
  MicroJava/DFA/Opt.thy MicroJava/DFA/Product.thy			\
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents: 33820
diff changeset
   966
  MicroJava/DFA/SemilatAlg.thy MicroJava/DFA/Semilat.thy		\
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents: 33820
diff changeset
   967
  MicroJava/DFA/Semilattices.thy MicroJava/DFA/Typing_Framework_err.thy	\
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents: 33820
diff changeset
   968
  MicroJava/DFA/Typing_Framework.thy MicroJava/BV/BVSpec.thy		\
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   969
  MicroJava/BV/BVSpecTypeSafe.thy MicroJava/BV/Correct.thy		\
33954
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents: 33820
diff changeset
   970
  MicroJava/BV/JType.thy MicroJava/BV/JVM.thy MicroJava/BV/JVMType.thy	\
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   971
  MicroJava/BV/Effect.thy MicroJava/BV/EffectMono.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   972
  MicroJava/BV/Typing_Framework_JVM.thy MicroJava/BV/BVExample.thy	\
33954
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents: 33820
diff changeset
   973
  MicroJava/BV/LBVJVM.thy MicroJava/document/root.bib			\
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents: 33820
diff changeset
   974
  MicroJava/document/root.tex MicroJava/document/introduction.tex
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   975
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL MicroJava
11850
cdfc3fce577e document graphs for several sessions;
wenzelm
parents: 11837
diff changeset
   976
8012
bbdf3c51c3b8 Added MicroJava
nipkow
parents: 8008
diff changeset
   977
11376
bf98ad1c22c6 added NanoJava
oheimb
parents: 11370
diff changeset
   978
## HOL-NanoJava
bf98ad1c22c6 added NanoJava
oheimb
parents: 11370
diff changeset
   979
bf98ad1c22c6 added NanoJava
oheimb
parents: 11370
diff changeset
   980
HOL-NanoJava: HOL $(LOG)/HOL-NanoJava.gz
bf98ad1c22c6 added NanoJava
oheimb
parents: 11370
diff changeset
   981
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   982
$(LOG)/HOL-NanoJava.gz: $(OUT)/HOL NanoJava/ROOT.ML NanoJava/Term.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   983
  NanoJava/Decl.thy NanoJava/TypeRel.thy NanoJava/State.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   984
  NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy		\
11376
bf98ad1c22c6 added NanoJava
oheimb
parents: 11370
diff changeset
   985
  NanoJava/document/root.bib NanoJava/document/root.tex
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   986
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NanoJava
11850
cdfc3fce577e document graphs for several sessions;
wenzelm
parents: 11837
diff changeset
   987
8193
33e4ec7a2daa added MicroJava/document;
wenzelm
parents: 8179
diff changeset
   988
12855
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
   989
## HOL-Bali
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
   990
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
   991
HOL-Bali: HOL $(LOG)/HOL-Bali.gz
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
   992
33024
60a098883d81 more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents: 33010
diff changeset
   993
$(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/Bali.thy Bali/AxCompl.thy		\
60a098883d81 more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents: 33010
diff changeset
   994
  Bali/AxExample.thy Bali/AxSem.thy Bali/AxSound.thy Bali/Basis.thy	\
60a098883d81 more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents: 33010
diff changeset
   995
  Bali/Conform.thy Bali/Decl.thy Bali/DeclConcepts.thy Bali/Eval.thy	\
60a098883d81 more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents: 33010
diff changeset
   996
  Bali/Evaln.thy Bali/Example.thy Bali/Name.thy Bali/ROOT.ML		\
60a098883d81 more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents: 33010
diff changeset
   997
  Bali/State.thy Bali/Table.thy Bali/Term.thy Bali/Trans.thy		\
60a098883d81 more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents: 33010
diff changeset
   998
  Bali/Type.thy Bali/TypeRel.thy Bali/TypeSafe.thy Bali/Value.thy	\
60a098883d81 more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents: 33010
diff changeset
   999
  Bali/WellForm.thy Bali/DefiniteAssignment.thy				\
60a098883d81 more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents: 33010
diff changeset
  1000
  Bali/DefiniteAssignmentCorrect.thy Bali/WellType.thy			\
60a098883d81 more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents: 33010
diff changeset
  1001
  Bali/document/root.tex
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
  1002
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Bali
12855
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
  1003
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
  1004
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1005
## HOL-IOA
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1006
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1007
HOL-IOA: HOL $(LOG)/HOL-IOA.gz
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
  1008
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
  1009
$(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.thy IOA/IOA.thy IOA/ROOT.ML	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
  1010
  IOA/Solve.thy
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
  1011
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL IOA
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1012
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1013
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
  1014
## HOL-Lattice
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
  1015
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
  1016
HOL-Lattice: HOL $(LOG)/HOL-Lattice.gz
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
  1017
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
  1018
$(LOG)/HOL-Lattice.gz: $(OUT)/HOL Lattice/Bounds.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
  1019
  Lattice/CompleteLattice.thy Lattice/Lattice.thy Lattice/Orders.thy	\
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
  1020
  Lattice/ROOT.ML Lattice/document/root.tex
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
  1021
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Lattice
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
  1022
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
  1023
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1024
## HOL-ex
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
  1025
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1026
HOL-ex: HOL $(LOG)/HOL-ex.gz
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
  1027
33439
f5d95787224f more accurate dependencies;
wenzelm
parents: 33437
diff changeset
  1028
$(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy	\
39157
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
  1029
  Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy		\
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
  1030
  ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy ex/BT.thy	\
40837
dedb893dc692 more precise dependencies;
wenzelm
parents: 40777
diff changeset
  1031
  ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradoxon.thy ex/CTL.thy	\
41827
98eda7ffde79 setup case_product attribute in HOL and FOL
noschinl
parents: 41655
diff changeset
  1032
  ex/Case_Product.thy							\
40837
dedb893dc692 more precise dependencies;
wenzelm
parents: 40777
diff changeset
  1033
  ex/Chinese.thy ex/Classical.thy ex/CodegenSML_Test.thy		\
dedb893dc692 more precise dependencies;
wenzelm
parents: 40777
diff changeset
  1034
  ex/Coercion_Examples.thy ex/Coherent.thy ex/Dedekind_Real.thy		\
dedb893dc692 more precise dependencies;
wenzelm
parents: 40777
diff changeset
  1035
  ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy	\
dedb893dc692 more precise dependencies;
wenzelm
parents: 40777
diff changeset
  1036
  ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy	\
dedb893dc692 more precise dependencies;
wenzelm
parents: 40777
diff changeset
  1037
  ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy		\
dedb893dc692 more precise dependencies;
wenzelm
parents: 40777
diff changeset
  1038
  ex/Higher_Order_Logic.thy ex/Iff_Oracle.thy ex/Induction_Schema.thy	\
dedb893dc692 more precise dependencies;
wenzelm
parents: 40777
diff changeset
  1039
  ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy		\
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents: 41569
diff changeset
  1040
  ex/Interpretation_with_Defs.thy ex/Intuitionistic.thy ex/Lagrange.thy	\
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents: 41569
diff changeset
  1041
  ex/List_to_Set_Comprehension_Examples.thy ex/LocaleTest2.thy		\
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents: 41569
diff changeset
  1042
  ex/MT.thy ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy	\
40837
dedb893dc692 more precise dependencies;
wenzelm
parents: 40777
diff changeset
  1043
  ex/Multiquote.thy ex/NatSum.thy ex/Normalization_by_Evaluation.thy	\
dedb893dc692 more precise dependencies;
wenzelm
parents: 40777
diff changeset
  1044
  ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy		\
dedb893dc692 more precise dependencies;
wenzelm
parents: 40777
diff changeset
  1045
  ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy		\
dedb893dc692 more precise dependencies;
wenzelm
parents: 40777
diff changeset
  1046
  ex/Quicksort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy		\
dedb893dc692 more precise dependencies;
wenzelm
parents: 40777
diff changeset
  1047
  ex/ReflectionEx.thy ex/Refute_Examples.thy ex/SAT_Examples.thy	\
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents: 41569
diff changeset
  1048
  ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy ex/Sqrt.thy	\
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents: 41569
diff changeset
  1049
  ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy	\
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents: 41569
diff changeset
  1050
  ex/Transfer_Ex.thy ex/Tree23.thy ex/Unification.thy			\
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents: 41569
diff changeset
  1051
  ex/While_Combinator_Example.thy ex/document/root.bib			\
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents: 41569
diff changeset
  1052
  ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy	\
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents: 41569
diff changeset
  1053
  ../Tools/interpretation_with_defs.ML
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
  1054
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
  1055
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
  1056
33026
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
  1057
## HOL-Isar_Examples
6445
931fc1daa8b1 added Isar_examples;
wenzelm
parents: 6440
diff changeset
  1058
33026
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
  1059
HOL-Isar_Examples: HOL $(LOG)/HOL-Isar_Examples.gz
6445
931fc1daa8b1 added Isar_examples;
wenzelm
parents: 6440
diff changeset
  1060
33026
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
  1061
$(LOG)/HOL-Isar_Examples.gz: $(OUT)/HOL Isar_Examples/Basic_Logic.thy	\
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
  1062
  Isar_Examples/Cantor.thy Isar_Examples/Drinker.thy			\
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
  1063
  Isar_Examples/Expr_Compiler.thy Isar_Examples/Fibonacci.thy		\
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
  1064
  Isar_Examples/Group.thy Isar_Examples/Hoare.thy			\
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
  1065
  Isar_Examples/Hoare_Ex.thy Isar_Examples/Knaster_Tarski.thy		\
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
  1066
  Isar_Examples/Mutilated_Checkerboard.thy				\
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
  1067
  Isar_Examples/Nested_Datatype.thy Isar_Examples/Peirce.thy		\
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
  1068
  Isar_Examples/Puzzle.thy Isar_Examples/Summation.thy			\
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
  1069
  Isar_Examples/ROOT.ML Isar_Examples/document/proof.sty		\
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
  1070
  Isar_Examples/document/root.bib Isar_Examples/document/root.tex	\
37672
645eb9fec794 avoid Old_Number_Theory;
wenzelm
parents: 37665
diff changeset
  1071
  Isar_Examples/document/style.tex Hoare/hoare_tac.ML			\
645eb9fec794 avoid Old_Number_Theory;
wenzelm
parents: 37665
diff changeset
  1072
  Number_Theory/Primes.thy
33026
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
  1073
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Isar_Examples
6445
931fc1daa8b1 added Isar_examples;
wenzelm
parents: 6440
diff changeset
  1074
931fc1daa8b1 added Isar_examples;
wenzelm
parents: 6440
diff changeset
  1075
33028
9aa8bfb1649d modernized session SET_Protocol;
wenzelm
parents: 33027
diff changeset
  1076
## HOL-SET_Protocol
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
  1077
33028
9aa8bfb1649d modernized session SET_Protocol;
wenzelm
parents: 33027
diff changeset
  1078
HOL-SET_Protocol: HOL $(LOG)/HOL-SET_Protocol.gz
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
  1079
33028
9aa8bfb1649d modernized session SET_Protocol;
wenzelm
parents: 33027
diff changeset
  1080
$(LOG)/HOL-SET_Protocol.gz: $(OUT)/HOL SET_Protocol/ROOT.ML		\
9aa8bfb1649d modernized session SET_Protocol;
wenzelm
parents: 33027
diff changeset
  1081
  SET_Protocol/Message_SET.thy SET_Protocol/Event_SET.thy		\
9aa8bfb1649d modernized session SET_Protocol;
wenzelm
parents: 33027
diff changeset
  1082
  SET_Protocol/Public_SET.thy SET_Protocol/Cardholder_Registration.thy	\
9aa8bfb1649d modernized session SET_Protocol;
wenzelm
parents: 33027
diff changeset
  1083
  SET_Protocol/Merchant_Registration.thy SET_Protocol/Purchase.thy	\
39757
21423597a80d modernized session
haftmann
parents: 39720
diff changeset
  1084
  SET_Protocol/SET_Protocol.thy SET_Protocol/document/root.tex
33028
9aa8bfb1649d modernized session SET_Protocol;
wenzelm
parents: 33027
diff changeset
  1085
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL SET_Protocol
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
  1086
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
  1087
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
  1088
## HOL-Matrix
14610
9c2e31e483b2 added HOL-Matrix, added HOL/Matrix/ROOT.ML
kleing
parents: 14603
diff changeset
  1089
28637
7aabaf1ba263 reactivated HOL-Matrix;
wenzelm
parents: 28612
diff changeset
  1090
HOL-Matrix: HOL $(LOG)/HOL-Matrix.gz
17323
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight
obua
parents: 17308
diff changeset
  1091
37872
d83659570337 moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway;
wenzelm
parents: 37818
diff changeset
  1092
$(LOG)/HOL-Matrix.gz: $(OUT)/HOL Matrix/ComputeFloat.thy		\
d83659570337 moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway;
wenzelm
parents: 37818
diff changeset
  1093
  Matrix/ComputeHOL.thy Matrix/ComputeNumeral.thy			\
d83659570337 moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway;
wenzelm
parents: 37818
diff changeset
  1094
  Matrix/Compute_Oracle/Compute_Oracle.thy Matrix/Compute_Oracle/am.ML	\
d83659570337 moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway;
wenzelm
parents: 37818
diff changeset
  1095
  Matrix/Compute_Oracle/am_compiler.ML Matrix/Compute_Oracle/am_ghc.ML	\
d83659570337 moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway;
wenzelm
parents: 37818
diff changeset
  1096
  Matrix/Compute_Oracle/am_interpreter.ML				\
d83659570337 moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway;
wenzelm
parents: 37818
diff changeset
  1097
  Matrix/Compute_Oracle/am_sml.ML Matrix/Compute_Oracle/compute.ML	\
d83659570337 moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway;
wenzelm
parents: 37818
diff changeset
  1098
  Matrix/Compute_Oracle/linker.ML Matrix/Cplex.thy			\
37764
3489daf839d5 more regular session structure
haftmann
parents: 37747
diff changeset
  1099
  Matrix/CplexMatrixConverter.ML Matrix/Cplex_tools.ML			\
37872
d83659570337 moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway;
wenzelm
parents: 37818
diff changeset
  1100
  Matrix/FloatSparseMatrixBuilder.ML Matrix/LP.thy Matrix/Matrix.thy	\
d83659570337 moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway;
wenzelm
parents: 37818
diff changeset
  1101
  Matrix/ROOT.ML Matrix/SparseMatrix.thy Matrix/document/root.tex	\
d83659570337 moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway;
wenzelm
parents: 37818
diff changeset
  1102
  Matrix/fspmlp.ML Matrix/matrixlp.ML Tools/float_arith.ML
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
  1103
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Matrix
16873
9ed940a1bebb proving bounds for real linear programs
obua
parents: 16784
diff changeset
  1104
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
  1105
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1106
## TLA
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1107
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1108
TLA: HOL $(OUT)/TLA
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1109
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
  1110
$(OUT)/TLA: $(OUT)/HOL TLA/Action.thy TLA/Init.thy TLA/Intensional.thy	\
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 21542
diff changeset
  1111
  TLA/ROOT.ML TLA/Stfun.thy TLA/TLA.thy
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
  1112
	@cd TLA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL TLA
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1113
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1114
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1115
## TLA-Inc
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1116
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1117
TLA-Inc: TLA $(LOG)/TLA-Inc.gz
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1118
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 21542
diff changeset
  1119
$(LOG)/TLA-Inc.gz: $(OUT)/TLA TLA/Inc/Inc.thy
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
  1120
	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Inc
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1121
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1122
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1123
## TLA-Buffer
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1124
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1125
TLA-Buffer: TLA $(LOG)/TLA-Buffer.gz
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
  1126
33024
60a098883d81 more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents: 33010
diff changeset
  1127
$(LOG)/TLA-Buffer.gz: $(OUT)/TLA TLA/Buffer/Buffer.thy	\
60a098883d81 more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents: 33010
diff changeset
  1128
  TLA/Buffer/DBuffer.thy
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
  1129
	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Buffer
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1130
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1131
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1132
## TLA-Memory
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1133
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1134
TLA-Memory: TLA $(LOG)/TLA-Memory.gz
4447
b7ee449eb345 log files;
wenzelm
parents: 4289
diff changeset
  1135
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
  1136
$(LOG)/TLA-Memory.gz: $(OUT)/TLA TLA/Memory/MemClerk.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
  1137
  TLA/Memory/MemClerkParameters.thy TLA/Memory/Memory.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
  1138
  TLA/Memory/MemoryImplementation.thy TLA/Memory/MemoryParameters.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
  1139
  TLA/Memory/ProcedureInterface.thy TLA/Memory/RPC.thy			\
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 21542
diff changeset
  1140
  TLA/Memory/RPCMemoryParams.thy TLA/Memory/RPCParameters.thy
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
  1141
	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Memory
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1142
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1143
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents: 33083
diff changeset
  1144
## HOL-Multivariate_Analysis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents: 33083
diff changeset
  1145
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
  1146
HOL-Multivariate_Analysis: HOL $(OUT)/HOL-Multivariate_Analysis
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents: 33083
diff changeset
  1147
36937
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1148
$(OUT)/HOL-Multivariate_Analysis: $(OUT)/HOL				\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1149
  Multivariate_Analysis/Brouwer_Fixpoint.thy				\
37522
0246a314b57d more accurate dependencies;
wenzelm
parents: 37509
diff changeset
  1150
  Multivariate_Analysis/Cartesian_Euclidean_Space.thy                   \
36937
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1151
  Multivariate_Analysis/Convex_Euclidean_Space.thy			\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1152
  Multivariate_Analysis/Derivative.thy					\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1153
  Multivariate_Analysis/Determinants.thy				\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1154
  Multivariate_Analysis/Euclidean_Space.thy				\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1155
  Multivariate_Analysis/Fashoda.thy					\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1156
  Multivariate_Analysis/Finite_Cartesian_Product.thy			\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1157
  Multivariate_Analysis/Integration.certs				\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1158
  Multivariate_Analysis/Integration.thy					\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1159
  Multivariate_Analysis/L2_Norm.thy					\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1160
  Multivariate_Analysis/Multivariate_Analysis.thy			\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1161
  Multivariate_Analysis/Operator_Norm.thy				\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1162
  Multivariate_Analysis/Path_Connected.thy				\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1163
  Multivariate_Analysis/ROOT.ML						\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1164
  Multivariate_Analysis/Real_Integration.thy				\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1165
  Multivariate_Analysis/Topology_Euclidean_Space.thy			\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1166
  Multivariate_Analysis/document/root.tex				\
37742
d8e7f473c3a1 tuned tabs
haftmann
parents: 37691
diff changeset
  1167
  Multivariate_Analysis/normarith.ML Library/Glbs.thy			\
40860
a6df324752da More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
hoelzl
parents: 40839
diff changeset
  1168
  Library/Indicator_Function.thy Library/Inner_Product.thy		\
a6df324752da More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
hoelzl
parents: 40839
diff changeset
  1169
  Library/Numeral_Type.thy Library/Convex.thy Library/FrechetDeriv.thy	\
36649
bfd8c550faa6 Corrected imports; better approximation of dependencies.
hoelzl
parents: 36648
diff changeset
  1170
  Library/Product_Vector.thy Library/Product_plus.thy
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
  1171
	@cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Multivariate_Analysis
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents: 33083
diff changeset
  1172
33285
wenzelm
parents: 33272
diff changeset
  1173
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents: 33270
diff changeset
  1174
## HOL-Probability
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents: 33270
diff changeset
  1175
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38622
diff changeset
  1176
HOL-Probability: HOL-Multivariate_Analysis $(OUT)/HOL-Probability
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents: 33270
diff changeset
  1177
40863
ab83ba2cd5d1 Corrected IsaMakefile
hoelzl
parents: 40862
diff changeset
  1178
$(OUT)/HOL-Probability: $(OUT)/HOL-Multivariate_Analysis		\
40860
a6df324752da More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
hoelzl
parents: 40839
diff changeset
  1179
  Probability/Borel_Space.thy Probability/Caratheodory.thy		\
a6df324752da More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
hoelzl
parents: 40839
diff changeset
  1180
  Probability/Complete_Measure.thy					\
a6df324752da More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
hoelzl
parents: 40839
diff changeset
  1181
  Probability/ex/Dining_Cryptographers.thy				\
a6df324752da More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
hoelzl
parents: 40839
diff changeset
  1182
  Probability/ex/Koepf_Duermuth_Countermeasure.thy			\
a6df324752da More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
hoelzl
parents: 40839
diff changeset
  1183
  Probability/Information.thy Probability/Lebesgue_Integration.thy	\
a6df324752da More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
hoelzl
parents: 40839
diff changeset
  1184
  Probability/Lebesgue_Measure.thy Probability/Measure.thy		\
41023
9118eb4eb8dc it is known as the extended reals, not the infinite reals
hoelzl
parents: 40969
diff changeset
  1185
  Probability/Positive_Extended_Real.thy				\
40860
a6df324752da More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
hoelzl
parents: 40839
diff changeset
  1186
  Probability/Probability_Space.thy Probability/Probability.thy		\
a6df324752da More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
hoelzl
parents: 40839
diff changeset
  1187
  Probability/Product_Measure.thy Probability/Radon_Nikodym.thy		\
a6df324752da More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
hoelzl
parents: 40839
diff changeset
  1188
  Probability/ROOT.ML Probability/Sigma_Algebra.thy			\
a6df324752da More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
hoelzl
parents: 40839
diff changeset
  1189
  Library/Countable.thy Library/FuncSet.thy				\
a6df324752da More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
hoelzl
parents: 40839
diff changeset
  1190
  Library/Nat_Bijection.thy
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38622
diff changeset
  1191
	@cd Probability; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Multivariate_Analysis HOL-Probability
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents: 33270
diff changeset
  1192
39157
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
  1193
19497
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
  1194
## HOL-Nominal
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
  1195
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
  1196
HOL-Nominal: HOL $(OUT)/HOL-Nominal
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
  1197
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents: 22167
diff changeset
  1198
$(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
  1199
  Nominal/Nominal.thy \
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents: 22167
diff changeset
  1200
  Nominal/nominal_atoms.ML \
31936
9466169dc8e0 nominal.ML is nominal_datatype.ML
haftmann
parents: 31849
diff changeset
  1201
  Nominal/nominal_datatype.ML \
22784
4637b69de71b Added datatype_case.ML and nominal_fresh_fun.ML.
berghofe
parents: 22657
diff changeset
  1202
  Nominal/nominal_fresh_fun.ML \
22247
5bad0d429694 corrected typo introduced by me
urbanc
parents: 22245
diff changeset
  1203
  Nominal/nominal_induct.ML \
22314
d541f13756a2 Added new file Nominal/nominal_inductive.ML
berghofe
parents: 22260
diff changeset
  1204
  Nominal/nominal_inductive.ML \
28652
659d64d59f16 Added nominal_inductive2.ML
berghofe
parents: 28637
diff changeset
  1205
  Nominal/nominal_inductive2.ML \
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents: 22167
diff changeset
  1206
  Nominal/nominal_permeq.ML \
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents: 22167
diff changeset
  1207
  Nominal/nominal_primrec.ML \
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents: 22167
diff changeset
  1208
  Nominal/nominal_thmdecls.ML \
21542
4462ee172ef0 Added nominal_primrec.ML
berghofe
parents: 21425
diff changeset
  1209
  Library/Infinite_Set.thy
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
  1210
	@cd Nominal; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Nominal
19497
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
  1211
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
  1212
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
  1213
## HOL-Nominal-Examples
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
  1214
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
  1215
HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
  1216
39157
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents: 39156
diff changeset
  1217
$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal \
32636
55a0be42327c added session theory for Bali and Nominal_Examples
haftmann
parents: 32632
diff changeset
  1218
  Nominal/Examples/Nominal_Examples.thy \
27163
587ad1fba128 added CK_Machine to the nominal section
urbanc
parents: 27127
diff changeset
  1219
  Nominal/Examples/CK_Machine.thy \
22073
c170dcbe6c9d formalisation of Crary's chapter on logical relations
urbanc
parents: 22067
diff changeset
  1220
  Nominal/Examples/CR.thy \
22821
15b2e7ec1f3b alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents: 22819
diff changeset
  1221
  Nominal/Examples/CR_Takahashi.thy \
36277
9be4ab2acc13 split Class.thy into parts to conserve a bit of memory and increase the chance of making it work on Cygwin with only 2 GB available;
wenzelm
parents: 36147
diff changeset
  1222
  Nominal/Examples/Class1.thy \
9be4ab2acc13 split Class.thy into parts to conserve a bit of memory and increase the chance of making it work on Cygwin with only 2 GB available;
wenzelm
parents: 36147
diff changeset
  1223
  Nominal/Examples/Class2.thy \
9be4ab2acc13 split Class.thy into parts to conserve a bit of memory and increase the chance of making it work on Cygwin with only 2 GB available;
wenzelm
parents: 36147
diff changeset
  1224
  Nominal/Examples/Class3.thy \
22073
c170dcbe6c9d formalisation of Crary's chapter on logical relations
urbanc
parents: 22067
diff changeset
  1225
  Nominal/Examples/Compile.thy \
25725
18bc59fb01b5 updated HOL-Nominal-Examples deps;
wenzelm
parents: 25600
diff changeset
  1226
  Nominal/Examples/Contexts.thy \
18bc59fb01b5 updated HOL-Nominal-Examples deps;
wenzelm
parents: 25600
diff changeset
  1227
  Nominal/Examples/Crary.thy \
22073
c170dcbe6c9d formalisation of Crary's chapter on logical relations
urbanc
parents: 22067
diff changeset
  1228
  Nominal/Examples/Fsub.thy \
25725
18bc59fb01b5 updated HOL-Nominal-Examples deps;
wenzelm
parents: 25600
diff changeset
  1229
  Nominal/Examples/Height.thy \
18bc59fb01b5 updated HOL-Nominal-Examples deps;
wenzelm
parents: 25600
diff changeset
  1230
  Nominal/Examples/Lam_Funs.thy \
22073
c170dcbe6c9d formalisation of Crary's chapter on logical relations
urbanc
parents: 22067
diff changeset
  1231
  Nominal/Examples/Lambda_mu.thy \
25725
18bc59fb01b5 updated HOL-Nominal-Examples deps;
wenzelm
parents: 25600
diff changeset
  1232
  Nominal/Examples/LocalWeakening.thy \
33189
82a40677c1f8 Added Pattern.thy to Nominal/Examples.
berghofe
parents: 33176
diff changeset
  1233
  Nominal/Examples/Pattern.thy \
25725
18bc59fb01b5 updated HOL-Nominal-Examples deps;
wenzelm
parents: 25600
diff changeset
  1234
  Nominal/Examples/ROOT.ML \
22073
c170dcbe6c9d formalisation of Crary's chapter on logical relations
urbanc
parents: 22067
diff changeset
  1235
  Nominal/Examples/SN.thy \
23144
4a9c9e260abf included new example in the compiling process
urbanc
parents: 23100
diff changeset
  1236
  Nominal/Examples/SOS.thy \
27624
a925aa66e17a Added Standardization theory to nominal examples.
berghofe
parents: 27484
diff changeset
  1237
  Nominal/Examples/Standardization.thy \
24896
70f238757695 added the two new examples from Nominal to the build process
urbanc
parents: 24830
diff changeset
  1238
  Nominal/Examples/Support.thy \
27032
6fd85edc403d new example
urbanc
parents: 26878
diff changeset
  1239
  Nominal/Examples/Type_Preservation.thy \
25725
18bc59fb01b5 updated HOL-Nominal-Examples deps;
wenzelm
parents: 25600
diff changeset
  1240
  Nominal/Examples/VC_Condition.thy \
26195
8292f8723e99 added new example
urbanc
parents: 26192
diff changeset
  1241
  Nominal/Examples/W.thy \
25725
18bc59fb01b5 updated HOL-Nominal-Examples deps;
wenzelm
parents: 25600
diff changeset
  1242
  Nominal/Examples/Weakening.thy
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
  1243
	@cd Nominal; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Nominal Examples
19497
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
  1244
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
  1245
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
  1246
## HOL-Word
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
  1247
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
  1248
HOL-Word: HOL $(OUT)/HOL-Word
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
  1249
33024
60a098883d81 more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents: 33010
diff changeset
  1250
$(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML Library/Boolean_Algebra.thy	\
37655
f4d616d41a59 more speaking theory names
haftmann
parents: 37583
diff changeset
  1251
  Library/Numeral_Type.thy Word/Misc_Numeric.thy Word/Misc_Typedef.thy	\
37659
14cabf5fa710 more speaking names
haftmann
parents: 37655
diff changeset
  1252
  Word/Type_Length.thy Word/Bit_Representation.thy Word/Bit_Int.thy	\
14cabf5fa710 more speaking names
haftmann
parents: 37655
diff changeset
  1253
  Word/Bool_List_Representation.thy Word/Bit_Operations.thy		\
37660
56e3520b68b2 one unified Word theory
haftmann
parents: 37659
diff changeset
  1254
  Word/Word.thy Word/document/root.tex					\
41060
4199fdcfa3c0 moved smt_word.ML into the directory of the Word library
boehmes
parents: 40969
diff changeset
  1255
  Word/document/root.bib Word/Tools/smt_word.ML
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
  1256
	@cd Word; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Word
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
  1257
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
  1258
24442
39e29972cb96 HOL-Word-Examples
huffman
parents: 24411
diff changeset
  1259
## HOL-Word-Examples
39e29972cb96 HOL-Word-Examples
huffman
parents: 24411
diff changeset
  1260
39e29972cb96 HOL-Word-Examples
huffman
parents: 24411
diff changeset
  1261
HOL-Word-Examples: HOL-Word $(LOG)/HOL-Word-Examples.gz
39e29972cb96 HOL-Word-Examples
huffman
parents: 24411
diff changeset
  1262
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
  1263
$(LOG)/HOL-Word-Examples.gz: $(OUT)/HOL-Word Word/Examples/ROOT.ML	\
24442
39e29972cb96 HOL-Word-Examples
huffman
parents: 24411
diff changeset
  1264
  Word/Examples/WordExamples.thy
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
  1265
	@cd Word; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Word Examples
24442
39e29972cb96 HOL-Word-Examples
huffman
parents: 24411
diff changeset
  1266
27477
c64736fe2a1f more precise dependencies for HOL-Word and HOL-NSA;
wenzelm
parents: 27470
diff changeset
  1267
25171
4a9c25bffc9b added Statespace library
schirmer
parents: 24994
diff changeset
  1268
## HOL-Statespace
4a9c25bffc9b added Statespace library
schirmer
parents: 24994
diff changeset
  1269
4a9c25bffc9b added Statespace library
schirmer
parents: 24994
diff changeset
  1270
HOL-Statespace: HOL $(LOG)/HOL-Statespace.gz
4a9c25bffc9b added Statespace library
schirmer
parents: 24994
diff changeset
  1271
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
  1272
$(LOG)/HOL-Statespace.gz: $(OUT)/HOL Statespace/DistinctTreeProver.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
  1273
  Statespace/StateFun.thy Statespace/StateSpaceLocale.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
  1274
  Statespace/StateSpaceSyntax.thy Statespace/StateSpaceEx.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
  1275
  Statespace/distinct_tree_prover.ML Statespace/state_space.ML		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
  1276
  Statespace/state_fun.ML Statespace/document/root.tex
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
  1277
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Statespace
24442
39e29972cb96 HOL-Word-Examples
huffman
parents: 24411
diff changeset
  1278
27477
c64736fe2a1f more precise dependencies for HOL-Word and HOL-NSA;
wenzelm
parents: 27470
diff changeset
  1279
27470
84526c368a58 add HOL-NSA
huffman
parents: 27456
diff changeset
  1280
## HOL-NSA
84526c368a58 add HOL-NSA
huffman
parents: 27456
diff changeset
  1281
27477
c64736fe2a1f more precise dependencies for HOL-Word and HOL-NSA;
wenzelm
parents: 27470
diff changeset
  1282
HOL-NSA: HOL $(OUT)/HOL-NSA
27470
84526c368a58 add HOL-NSA
huffman
parents: 27456
diff changeset
  1283
33024
60a098883d81 more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents: 33010
diff changeset
  1284
$(OUT)/HOL-NSA: $(OUT)/HOL NSA/CLim.thy NSA/CStar.thy NSA/NSCA.thy	\