src/HOL/IsaMakefile
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 47325 ec6187036495
child 47474 214bfaae738d
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
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
33210
94ae82a4452f recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents: 33204
diff changeset
     8
94ae82a4452f recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents: 33204
diff changeset
     9
images: \
94ae82a4452f recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents: 33204
diff changeset
    10
  HOL \
37691
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
    11
  HOL-Library \
33210
94ae82a4452f recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents: 33204
diff changeset
    12
  HOL-Algebra \
33419
8ae45e87b992 added HOL-Boogie
boehmes
parents: 33356
diff changeset
    13
  HOL-Boogie \
43917
bce3de79c8ce build an image for HOL-IMP
kleing
parents: 43834
diff changeset
    14
  HOL-IMP \
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 \
34205
f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents: 34126
diff changeset
    18
  HOL-Proofs \
41566
676b32bea254 Added HOL-SPARK and removed old_primrec.ML
berghofe
parents: 41505
diff changeset
    19
  HOL-SPARK \
33210
94ae82a4452f recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents: 33204
diff changeset
    20
  HOL-Word \
40774
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF;
huffman
parents: 40676
diff changeset
    21
  HOLCF \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF;
huffman
parents: 40676
diff changeset
    22
  IOA \
37691
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
    23
  TLA \
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
    24
  HOL-Base \
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
    25
  HOL-Main \
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
    26
  HOL-Plain
10135
c2a4dccf6e67 reorganized AxClasses;
wenzelm
parents: 10094
diff changeset
    27
42138
e54a985daa61 added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
krauss
parents: 42071
diff changeset
    28
#Note: keep targets sorted
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    29
test: \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    30
  HOL-Auth \
14031
3240066af013 Added Bali to test
schirmer
parents: 14029
diff changeset
    31
  HOL-Bali \
33439
f5d95787224f more accurate dependencies;
wenzelm
parents: 33437
diff changeset
    32
  HOL-Boogie-Examples \
31795
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 31771
diff changeset
    33
  HOL-Hahn_Banach \
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    34
  HOL-Hoare \
32621
a073cb249a06 theory entry point for session Hoare_Parallel (now also with proper underscore)
haftmann
parents: 32618
diff changeset
    35
  HOL-Hoare_Parallel \
40774
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF;
huffman
parents: 40676
diff changeset
    36
      HOLCF-FOCUS \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF;
huffman
parents: 40676
diff changeset
    37
      HOLCF-IMP \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF;
huffman
parents: 40676
diff changeset
    38
      HOLCF-Library \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF;
huffman
parents: 40676
diff changeset
    39
      HOLCF-Tutorial \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF;
huffman
parents: 40676
diff changeset
    40
      HOLCF-ex \
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    41
  HOL-IMPP \
47264
6488c5efec49 renamed import session back to Import, conforming to directory name; NEWS
krauss
parents: 47260
diff changeset
    42
  HOL-Import \
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    43
  HOL-IOA \
40774
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF;
huffman
parents: 40676
diff changeset
    44
      IOA-ABP \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF;
huffman
parents: 40676
diff changeset
    45
      IOA-NTP \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF;
huffman
parents: 40676
diff changeset
    46
      IOA-Storage \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF;
huffman
parents: 40676
diff changeset
    47
      IOA-ex \
29399
ebcd69a00872 split of Imperative_HOL theories from HOL-Library
haftmann
parents: 29197
diff changeset
    48
  HOL-Imperative_HOL \
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    49
  HOL-Induct \
33026
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
    50
  HOL-Isar_Examples \
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    51
  HOL-Lattice \
37747
3a699743bcba more accurate dependencies
haftmann
parents: 37742
diff changeset
    52
  HOL-Library-Codegenerator_Test \
46988
9f492f5b0cec renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents: 46951
diff changeset
    53
  HOL-Matrix_LP \
33027
9cf389429f6d modernized session Metis_Examples;
wenzelm
parents: 33026
diff changeset
    54
  HOL-Metis_Examples \
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    55
  HOL-MicroJava \
32496
4ab00a2642c3 moved Mirabelle from HOL/Tools to HOL,
boehmes
parents: 32479
diff changeset
    56
  HOL-Mirabelle \
35536
1f980bbc6ad8 adding HOL-Mutabelle to tests
bulwahn
parents: 35502
diff changeset
    57
  HOL-Mutabelle \
11376
bf98ad1c22c6 added NanoJava
oheimb
parents: 11370
diff changeset
    58
  HOL-NanoJava \
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents: 33192
diff changeset
    59
  HOL-Nitpick_Examples \
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
    60
  HOL-Number_Theory \
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
    61
  HOL-Old_Number_Theory \
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35151
diff changeset
    62
  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
    63
  HOL-Predicate_Compile_Examples \
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    64
  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
    65
  HOL-Proofs-ex \
47128
d0d16b20b6ce revert changeset 500a5d97511a, re-enabling HOL-Proofs-Lambda
huffman
parents: 47120
diff changeset
    66
  HOL-Proofs-Lambda \
33028
9aa8bfb1649d modernized session SET_Protocol;
wenzelm
parents: 33027
diff changeset
    67
  HOL-SET_Protocol \
41569
98f59921c420 Also added SPARK to test and clean targets.
berghofe
parents: 41566
diff changeset
    68
  HOL-SPARK-Examples \
45044
2fae15f8984d Added documentation for HOL-SPARK
berghofe
parents: 45035
diff changeset
    69
  HOL-SPARK-Manual \
36933
705b58fde476 more precise dependencies for HOL-Word-SMT_Examples;
wenzelm
parents: 36916
diff changeset
    70
  HOL-Word-SMT_Examples \
25171
4a9c25bffc9b added Statespace library
schirmer
parents: 24994
diff changeset
    71
  HOL-Statespace \
33210
94ae82a4452f recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents: 33204
diff changeset
    72
      TLA-Buffer \
94ae82a4452f recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents: 33204
diff changeset
    73
      TLA-Inc \
94ae82a4452f recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents: 33204
diff changeset
    74
      TLA-Memory \
43804
eb9be23db2b7 cleanly separate TPTP related files from other examples
blanchet
parents: 43800
diff changeset
    75
  HOL-TPTP \
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    76
  HOL-UNITY \
10966
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
    77
  HOL-Unix \
24442
39e29972cb96 HOL-Word-Examples
huffman
parents: 24411
diff changeset
    78
  HOL-Word-Examples \
24325
5c29e8822f50 make HOL-ex earlier;
wenzelm
parents: 24288
diff changeset
    79
  HOL-ZF
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
    80
    # ^ this is the sort position
10614
d5c14e205c24 added Library/Rational_Numbers.thy;
wenzelm
parents: 10574
diff changeset
    81
45860
93eda35a8377 more visible benchmarks;
wenzelm
parents: 45812
diff changeset
    82
benchmark: \
93eda35a8377 more visible benchmarks;
wenzelm
parents: 45812
diff changeset
    83
  HOL-Datatype_Benchmark \
93eda35a8377 more visible benchmarks;
wenzelm
parents: 45812
diff changeset
    84
  HOL-Record_Benchmark
93eda35a8377 more visible benchmarks;
wenzelm
parents: 45812
diff changeset
    85
42138
e54a985daa61 added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
krauss
parents: 42071
diff changeset
    86
images-no-smlnj: \
e54a985daa61 added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
krauss
parents: 42071
diff changeset
    87
  HOL-Probability
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
    88
42138
e54a985daa61 added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
krauss
parents: 42071
diff changeset
    89
test-no-smlnj: \
e54a985daa61 added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
krauss
parents: 42071
diff changeset
    90
  HOL-ex \
e54a985daa61 added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
krauss
parents: 42071
diff changeset
    91
  HOL-Decision_Procs \
e54a985daa61 added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
krauss
parents: 42071
diff changeset
    92
  HOL-Proofs-Extraction \
e54a985daa61 added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
krauss
parents: 42071
diff changeset
    93
  HOL-Nominal-Examples
e54a985daa61 added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
krauss
parents: 42071
diff changeset
    94
e54a985daa61 added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
krauss
parents: 42071
diff changeset
    95
all: test-no-smlnj test images-no-smlnj images
46701
879f5c76ffb6 reactivated Find_Unused_Assms_Examples to avoid untested / dead stuff in the repository;
wenzelm
parents: 46664
diff changeset
    96
full: all benchmark HOL-Quickcheck_Examples
42138
e54a985daa61 added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
krauss
parents: 42071
diff changeset
    97
smlnj: test images
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
    98
45860
93eda35a8377 more visible benchmarks;
wenzelm
parents: 45812
diff changeset
    99
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   100
## global settings
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   101
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   102
SRC = $(ISABELLE_HOME)/src
3118
24dae6222579 fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?);
wenzelm
parents: 3079
diff changeset
   103
OUT = $(ISABELLE_OUTPUT)
4447
b7ee449eb345 log files;
wenzelm
parents: 4289
diff changeset
   104
LOG = $(OUT)/log
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   105
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   106
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   107
## HOL
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   108
28393
30ba169e8c45 HOL no longer depends on HOL-Plain;
wenzelm
parents: 28376
diff changeset
   109
HOL: Pure $(OUT)/HOL
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   110
29505
c6d2d23909d1 added HOL-Base image
haftmann
parents: 29463
diff changeset
   111
HOL-Base: Pure $(OUT)/HOL-Base
c6d2d23909d1 added HOL-Base image
haftmann
parents: 29463
diff changeset
   112
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   113
HOL-Plain: Pure $(OUT)/HOL-Plain
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   114
28401
d5f39173444c separate HOL-Main image
haftmann
parents: 28393
diff changeset
   115
HOL-Main: Pure $(OUT)/HOL-Main
d5f39173444c separate HOL-Main image
haftmann
parents: 28393
diff changeset
   116
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   117
Pure:
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   118
	@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
   119
27694
31a8e0908b9f corrected Pure dependency
haftmann
parents: 27679
diff changeset
   120
$(OUT)/Pure: Pure
31a8e0908b9f corrected Pure dependency
haftmann
parents: 27679
diff changeset
   121
36073
54a9f56fae7c slightly more standard dependencies;
wenzelm
parents: 36066
diff changeset
   122
BASE_DEPENDENCIES = $(OUT)/Pure \
30160
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 30101
diff changeset
   123
  $(SRC)/Provers/blast.ML \
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 30101
diff changeset
   124
  $(SRC)/Provers/clasimp.ML \
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 30101
diff changeset
   125
  $(SRC)/Provers/classical.ML \
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 30101
diff changeset
   126
  $(SRC)/Provers/hypsubst.ML \
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 30101
diff changeset
   127
  $(SRC)/Provers/quantifier1.ML \
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 30101
diff changeset
   128
  $(SRC)/Provers/splitter.ML \
31771
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   129
  $(SRC)/Tools/Code/code_haskell.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   130
  $(SRC)/Tools/Code/code_ml.ML \
38970
53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents: 38965
diff changeset
   131
  $(SRC)/Tools/Code/code_namespace.ML \
31771
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   132
  $(SRC)/Tools/Code/code_preproc.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   133
  $(SRC)/Tools/Code/code_printer.ML \
39402
24d70f4e690d more accurate dependencies
haftmann
parents: 39394
diff changeset
   134
  $(SRC)/Tools/Code/code_runtime.ML \
34945
478f31081a78 more accurate dependencies
haftmann
parents: 34228
diff changeset
   135
  $(SRC)/Tools/Code/code_scala.ML \
37442
037ee7b712b2 added code_simp infrastructure
haftmann
parents: 37296
diff changeset
   136
  $(SRC)/Tools/Code/code_simp.ML \
31771
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   137
  $(SRC)/Tools/Code/code_target.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   138
  $(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
   139
  $(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
   140
  $(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
   141
  $(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
   142
  $(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
   143
  $(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
   144
  $(SRC)/Tools/atomize_elim.ML \
44120
01de796250a0 moved old code generator to src/Tools/;
wenzelm
parents: 44087
diff changeset
   145
  $(SRC)/Tools/cache_io.ML \
41827
98eda7ffde79 setup case_product attribute in HOL and FOL
noschinl
parents: 41655
diff changeset
   146
  $(SRC)/Tools/case_product.ML \
30160
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 30101
diff changeset
   147
  $(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
   148
  $(SRC)/Tools/cong_tac.ML \
30160
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 30101
diff changeset
   149
  $(SRC)/Tools/eqsubst.ML \
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 30101
diff changeset
   150
  $(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
   151
  $(SRC)/Tools/induct_tacs.ML \
45014
0e847655b2d8 New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents: 44962
diff changeset
   152
  $(SRC)/Tools/induction.ML \
30165
6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents: 30160
diff changeset
   153
  $(SRC)/Tools/intuitionistic.ML \
37781
2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents: 37779
diff changeset
   154
  $(SRC)/Tools/misc_legacy.ML \
30160
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 30101
diff changeset
   155
  $(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
   156
  $(SRC)/Tools/project_rule.ML \
30973
304ab57afa6e observe distinction between Pure/Tools and Tools more closely
haftmann
parents: 30954
diff changeset
   157
  $(SRC)/Tools/quickcheck.ML \
40116
9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents: 40067
diff changeset
   158
  $(SRC)/Tools/solve_direct.ML \
43614
2c741b50d4b7 improving actual dependencies
bulwahn
parents: 43556
diff changeset
   159
  $(SRC)/Tools/subtyping.ML \
43018
121aa59b4d17 renamed "Auto_Tools" "Try"
blanchet
parents: 43016
diff changeset
   160
  $(SRC)/Tools/try.ML \
30160
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 30101
diff changeset
   161
  $(SRC)/Tools/value.ML \
29505
c6d2d23909d1 added HOL-Base image
haftmann
parents: 29463
diff changeset
   162
  HOL.thy \
c6d2d23909d1 added HOL-Base image
haftmann
parents: 29463
diff changeset
   163
  Tools/hologic.ML \
36073
54a9f56fae7c slightly more standard dependencies;
wenzelm
parents: 36066
diff changeset
   164
  Tools/simpdata.ML
29505
c6d2d23909d1 added HOL-Base image
haftmann
parents: 29463
diff changeset
   165
c6d2d23909d1 added HOL-Base image
haftmann
parents: 29463
diff changeset
   166
$(OUT)/HOL-Base: base.ML $(BASE_DEPENDENCIES)
29523
f83dcdcee6b3 no document for HOL-Base
haftmann
parents: 29505
diff changeset
   167
	@$(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
   168
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
   169
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
   170
  $(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
   171
  $(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
   172
  $(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
   173
  $(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
   174
  $(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
   175
  $(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
   176
  $(SRC)/Tools/rat.ML \
43691
c00febb8e39c moved ATP dependencies to HOL-Plain, where they belong
blanchet
parents: 43614
diff changeset
   177
  ATP.thy \
44860
56101fa00193 renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
haftmann
parents: 44818
diff changeset
   178
  Complete_Lattices.thy \
40108
dbab949c2717 integrated partial_function into HOL-Plain
krauss
parents: 40104
diff changeset
   179
  Complete_Partial_Order.thy \
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   180
  Datatype.thy \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   181
  Extraction.thy \
35050
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 35039
diff changeset
   182
  Fields.thy \
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   183
  Finite_Set.thy \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   184
  Fun.thy \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   185
  FunDef.thy \
35050
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 35039
diff changeset
   186
  Groups.thy \
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   187
  Inductive.thy \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   188
  Lattices.thy \
39945
277addece9b7 added "Meson" theory to Makefile
blanchet
parents: 39940
diff changeset
   189
  Meson.thy \
39946
78faa9b31202 move Metis into Plain
blanchet
parents: 39945
diff changeset
   190
  Metis.thy \
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   191
  Nat.thy \
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   192
  Num.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
   193
  Option.thy \
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   194
  Orderings.thy \
40108
dbab949c2717 integrated partial_function into HOL-Plain
krauss
parents: 40104
diff changeset
   195
  Partial_Function.thy \
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   196
  Plain.thy \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   197
  Power.thy \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   198
  Product_Type.thy \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   199
  Relation.thy \
35050
9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents: 35039
diff changeset
   200
  Rings.thy \
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   201
  SAT.thy \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   202
  Set.thy \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   203
  Sum_Type.thy \
43691
c00febb8e39c moved ATP dependencies to HOL-Plain, where they belong
blanchet
parents: 43614
diff changeset
   204
  Tools/ATP/atp_problem.ML \
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46319
diff changeset
   205
  Tools/ATP/atp_problem_generate.ML \
43691
c00febb8e39c moved ATP dependencies to HOL-Plain, where they belong
blanchet
parents: 43614
diff changeset
   206
  Tools/ATP/atp_proof.ML \
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46319
diff changeset
   207
  Tools/ATP/atp_proof_reconstruct.ML \
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46319
diff changeset
   208
  Tools/ATP/atp_proof_redirect.ML \
43691
c00febb8e39c moved ATP dependencies to HOL-Plain, where they belong
blanchet
parents: 43614
diff changeset
   209
  Tools/ATP/atp_systems.ML \
c00febb8e39c moved ATP dependencies to HOL-Plain, where they belong
blanchet
parents: 43614
diff changeset
   210
  Tools/ATP/atp_util.ML \
40939
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   211
  Tools/Datatype/datatype.ML \
31771
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   212
  Tools/Datatype/datatype_aux.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   213
  Tools/Datatype/datatype_case.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   214
  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
   215
  Tools/Datatype/datatype_data.ML \
31771
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   216
  Tools/Datatype/datatype_prop.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   217
  Tools/Datatype/datatype_realizer.ML \
45897
65cef0298158 clarified modules that contribute to datatype package;
wenzelm
parents: 45890
diff changeset
   218
  Tools/Datatype/primrec.ML \
45890
5f70aaecae26 separate rep_datatype.ML;
wenzelm
parents: 45886
diff changeset
   219
  Tools/Datatype/rep_datatype.ML \
31771
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   220
  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
   221
  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
   222
  Tools/Function/function.ML \
33099
b8cdd3d73022 function package: more standard names for structures and files
krauss
parents: 33098
diff changeset
   223
  Tools/Function/function_common.ML \
b8cdd3d73022 function package: more standard names for structures and files
krauss
parents: 33098
diff changeset
   224
  Tools/Function/function_core.ML \
b8cdd3d73022 function package: more standard names for structures and files
krauss
parents: 33098
diff changeset
   225
  Tools/Function/function_lib.ML \
33471
5aef13872723 renamed method induct_scheme to induction_schema
krauss
parents: 33469
diff changeset
   226
  Tools/Function/induction_schema.ML \
31771
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   227
  Tools/Function/lexicographic_order.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   228
  Tools/Function/measure_functions.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   229
  Tools/Function/mutual.ML \
40108
dbab949c2717 integrated partial_function into HOL-Plain
krauss
parents: 40104
diff changeset
   230
  Tools/Function/partial_function.ML \
33083
1fad3160d873 pat_completeness gets its own file
krauss
parents: 33028
diff changeset
   231
  Tools/Function/pat_completeness.ML \
31771
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   232
  Tools/Function/pattern_split.ML \
33100
acc2bd3934ba renamed auto_term.ML -> relation.ML
krauss
parents: 33099
diff changeset
   233
  Tools/Function/relation.ML \
31771
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   234
  Tools/Function/scnp_reconstruct.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   235
  Tools/Function/scnp_solve.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   236
  Tools/Function/size.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   237
  Tools/Function/sum_tree.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   238
  Tools/Function/termination.ML \
39940
1f01c9b2b76b move MESON files together
blanchet
parents: 39889
diff changeset
   239
  Tools/Meson/meson.ML \
1f01c9b2b76b move MESON files together
blanchet
parents: 39889
diff changeset
   240
  Tools/Meson/meson_clausify.ML \
39948
317010af8972 factor out "Meson_Tactic" from "Meson_Clausify"
blanchet
parents: 39946
diff changeset
   241
  Tools/Meson/meson_tactic.ML \
46320
0b8b73b49848 renamed two files to make room for a new file
blanchet
parents: 46319
diff changeset
   242
  Tools/Metis/metis_generate.ML \
39946
78faa9b31202 move Metis into Plain
blanchet
parents: 39945
diff changeset
   243
  Tools/Metis/metis_reconstruct.ML \
44651
5d6a11e166cf renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
blanchet
parents: 44516
diff changeset
   244
  Tools/Metis/metis_tactic.ML \
40939
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   245
  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
   246
  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
   247
  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
   248
  Tools/dseq.ML \
45890
5f70aaecae26 separate rep_datatype.ML;
wenzelm
parents: 45886
diff changeset
   249
  Tools/enriched_type.ML \
40939
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   250
  Tools/inductive.ML \
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   251
  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
   252
  Tools/inductive_set.ML \
44087
8e491cb8841c load lambda-lifting structure earlier, so it can be used in Metis
blanchet
parents: 44014
diff changeset
   253
  Tools/lambda_lifting.ML \
40939
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   254
  Tools/lin_arith.ML \
44087
8e491cb8841c load lambda-lifting structure earlier, so it can be used in Metis
blanchet
parents: 44014
diff changeset
   255
  Tools/monomorph.ML \
30496
7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents: 30457
diff changeset
   256
  Tools/nat_arith.ML \
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   257
  Tools/prop_logic.ML \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   258
  Tools/refute.ML \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   259
  Tools/rewrite_hol_proof.ML \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   260
  Tools/sat_funcs.ML \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   261
  Tools/sat_solver.ML \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   262
  Tools/split_rule.ML \
46641
8801a24f9e9a renamed 'try_methods' to 'try0'
blanchet
parents: 46638
diff changeset
   263
  Tools/try0.ML \
31723
f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents: 31706
diff changeset
   264
  Tools/typedef.ML \
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   265
  Transitive_Closure.thy \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   266
  Typedef.thy \
40939
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40863
diff changeset
   267
  Wellfounded.thy
28312
f0838044f034 different session branches for HOL-Plain vs. Plain
haftmann
parents: 28243
diff changeset
   268
f0838044f034 different session branches for HOL-Plain vs. Plain
haftmann
parents: 28243
diff changeset
   269
$(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES)
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   270
	@$(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
   271
28401
d5f39173444c separate HOL-Main image
haftmann
parents: 28393
diff changeset
   272
MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
35725
4d7e3cc9c52c Big_Operators now in Main rather than Plain src/HOL/Wellfounded.thy
haftmann
parents: 35719
diff changeset
   273
  Big_Operators.thy \
32657
5f13912245ff Code_Eval(uation)
haftmann
parents: 32636
diff changeset
   274
  Code_Evaluation.thy \
31205
98370b26c2ce String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents: 31203
diff changeset
   275
  Code_Numeral.thy \
33296
a3924d1069e5 moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents: 33272
diff changeset
   276
  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
   277
  DSequence.thy \
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   278
  Equiv_Relations.thy \
40650
d40b347d5b0b adding Enum to HOL-Main image and removing it from HOL-Library
bulwahn
parents: 40634
diff changeset
   279
  Enum.thy \
27368
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   280
  Groebner_Basis.thy \
9f90ac19e32b established Plain theory and image
haftmann
parents: 27326
diff changeset
   281
  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
   282
  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
   283
  Lazy_Sequence.thy \
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47267
diff changeset
   284
  Lifting.thy \
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   285
  List.thy \
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   286
  Main.thy \
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   287
  Map.thy \
33318
ddd97d9dfbfb moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents: 33298
diff changeset
   288
  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
   289
  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
   290
  New_Random_Sequence.thy \
36915
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   291
  Nitpick.thy \
33356
9157d0f9f00e moved Commutative_Ring into session Decision_Procs
haftmann
parents: 33348
diff changeset
   292
  Numeral_Simprocs.thy \
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   293
  Presburger.thy \
46664
1f6c140f9c72 moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents: 46650
diff changeset
   294
  Predicate.thy \
33250
5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents: 33210
diff changeset
   295
  Predicate_Compile.thy \
31203
5c8fb4fd67e0 moved Code_Index, Random and Quickcheck before Main
haftmann
parents: 31186
diff changeset
   296
  Quickcheck.thy \
41919
e180c2a9873b correcting dependencies after renaming
bulwahn
parents: 41911
diff changeset
   297
  Quickcheck_Exhaustive.thy \
43310
d1265a4d8ae1 adapting IsaMakefile
bulwahn
parents: 43242
diff changeset
   298
  Quickcheck_Narrowing.thy \
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35151
diff changeset
   299
  Quotient.thy \
31203
5c8fb4fd67e0 moved Code_Index, Random and Quickcheck before Main
haftmann
parents: 31186
diff changeset
   300
  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
   301
  Random_Sequence.thy \
39271
436554f1beaa more correct dependencies
haftmann
parents: 39223
diff changeset
   302
  Record.thy \
36916
279074271b8e move Refute dependency from Plain to Main
blanchet
parents: 36915
diff changeset
   303
  Refute.thy \
36751
7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents: 36700
diff changeset
   304
  Semiring_Normalization.thy \
47317
432b29a96f61 modernized obsolete old-style theory name with proper new-style underscore
huffman
parents: 47267
diff changeset
   305
  Set_Interval.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
   306
  Sledgehammer.thy \
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
   307
  SMT.thy \
31048
ac146fc38b51 refined HOL string theories and corresponding ML fragments
haftmann
parents: 31036
diff changeset
   308
  String.thy \
47325
ec6187036495 new transfer proof method
huffman
parents: 47324
diff changeset
   309
  Transfer.thy \
31203
5c8fb4fd67e0 moved Code_Index, Random and Quickcheck before Main
haftmann
parents: 31186
diff changeset
   310
  Typerep.thy \
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   311
  $(SRC)/Provers/Arith/assoc_fold.ML \
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   312
  $(SRC)/Provers/Arith/cancel_numeral_factor.ML \
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   313
  $(SRC)/Provers/Arith/cancel_numerals.ML \
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   314
  $(SRC)/Provers/Arith/combine_numerals.ML \
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   315
  $(SRC)/Provers/Arith/extract_common_term.ML \
33318
ddd97d9dfbfb moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents: 33298
diff changeset
   316
  Tools/choice_specification.ML \
39564
acfd10e38e80 Factored out ML into separate file
haftmann
parents: 39505
diff changeset
   317
  Tools/code_evaluation.ML \
41919
e180c2a9873b correcting dependencies after renaming
bulwahn
parents: 41911
diff changeset
   318
  Tools/groebner.ML \
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31060
diff changeset
   319
  Tools/int_arith.ML \
47324
ed2bad9b7c6a renamed Tools/transfer.ML to Tools/legacy_transfer.ML
huffman
parents: 47318
diff changeset
   320
  Tools/legacy_transfer.ML \
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47267
diff changeset
   321
  Tools/Lifting/lifting_def.ML \
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47267
diff changeset
   322
  Tools/Lifting/lifting_info.ML \
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47267
diff changeset
   323
  Tools/Lifting/lifting_term.ML \
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47267
diff changeset
   324
  Tools/Lifting/lifting_setup.ML \
31055
2cf6efca6c71 proper structures for list and string code generation stuff
haftmann
parents: 31048
diff changeset
   325
  Tools/list_code.ML \
41463
edbf0a86fb1c adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents: 41426
diff changeset
   326
  Tools/list_to_set_comprehension.ML \
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31060
diff changeset
   327
  Tools/nat_numeral_simprocs.ML \
36915
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   328
  Tools/Nitpick/kodkod.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   329
  Tools/Nitpick/kodkod_sat.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   330
  Tools/Nitpick/nitpick.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   331
  Tools/Nitpick/nitpick_hol.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   332
  Tools/Nitpick/nitpick_isar.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   333
  Tools/Nitpick/nitpick_kodkod.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   334
  Tools/Nitpick/nitpick_model.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   335
  Tools/Nitpick/nitpick_mono.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   336
  Tools/Nitpick/nitpick_nut.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   337
  Tools/Nitpick/nitpick_peephole.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   338
  Tools/Nitpick/nitpick_preproc.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   339
  Tools/Nitpick/nitpick_rep.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   340
  Tools/Nitpick/nitpick_scope.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   341
  Tools/Nitpick/nitpick_tests.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents: 36901
diff changeset
   342
  Tools/Nitpick/nitpick_util.ML \
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   343
  Tools/numeral.ML \
31068
f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents: 31060
diff changeset
   344
  Tools/numeral_simprocs.ML \
40141
0e8a4e27a685 adding new predicate compiler files to the IsaMakefile
bulwahn
parents: 40123
diff changeset
   345
  Tools/Predicate_Compile/core_data.ML \
0e8a4e27a685 adding new predicate compiler files to the IsaMakefile
bulwahn
parents: 40123
diff changeset
   346
  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
   347
  Tools/Predicate_Compile/predicate_compile_aux.ML \
36046
c3946372f556 putting compilation setup of predicate compiler in a separate file
bulwahn
parents: 36032
diff changeset
   348
  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
   349
  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
   350
  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
   351
  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
   352
  Tools/Predicate_Compile/predicate_compile.ML \
40141
0e8a4e27a685 adding new predicate compiler files to the IsaMakefile
bulwahn
parents: 40123
diff changeset
   353
  Tools/Predicate_Compile/predicate_compile_proof.ML \
36032
dfd30b5b4e73 adding specialisation of predicates to the predicate compiler
bulwahn
parents: 35972
diff changeset
   354
  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
   355
  Tools/Predicate_Compile/predicate_compile_pred.ML \
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   356
  Tools/Qelim/cooper.ML \
36803
2cad8904c4ff updated references to ML files
haftmann
parents: 36798
diff changeset
   357
  Tools/Qelim/cooper_procedure.ML \
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   358
  Tools/Qelim/qelim.ML \
41920
d4fb7a418152 moving exhaustive_generators.ML to Quickcheck directory
bulwahn
parents: 41919
diff changeset
   359
  Tools/Quickcheck/exhaustive_generators.ML \
41924
107bf5c959d3 correcting dependencies in IsaMakefile
bulwahn
parents: 41920
diff changeset
   360
  Tools/Quickcheck/random_generators.ML \
41928
05abcee548a1 adaptions in generators using the common functions
bulwahn
parents: 41927
diff changeset
   361
  Tools/Quickcheck/quickcheck_common.ML \
43310
d1265a4d8ae1 adapting IsaMakefile
bulwahn
parents: 43242
diff changeset
   362
  Tools/Quickcheck/narrowing_generators.ML \
d1265a4d8ae1 adapting IsaMakefile
bulwahn
parents: 43242
diff changeset
   363
  Tools/Quickcheck/Narrowing_Engine.hs \
d1265a4d8ae1 adapting IsaMakefile
bulwahn
parents: 43242
diff changeset
   364
  Tools/Quickcheck/PNF_Narrowing_Engine.hs \
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35151
diff changeset
   365
  Tools/Quotient/quotient_def.ML \
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35151
diff changeset
   366
  Tools/Quotient/quotient_info.ML \
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35151
diff changeset
   367
  Tools/Quotient/quotient_tacs.ML \
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35151
diff changeset
   368
  Tools/Quotient/quotient_term.ML \
45680
a61510361b89 more conventional file name;
wenzelm
parents: 45577
diff changeset
   369
  Tools/Quotient/quotient_type.ML \
38394
3142c1e21a0e moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents: 38282
diff changeset
   370
  Tools/record.ML \
36753
5cf4e9128f22 renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents: 36751
diff changeset
   371
  Tools/semiring_normalizer.ML \
41042
8275f52ac991 load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents: 41023
diff changeset
   372
  Tools/Sledgehammer/async_manager.ML \
38986
e34c1b09bb5e shorten a few file names
blanchet
parents: 38942
diff changeset
   373
  Tools/Sledgehammer/sledgehammer_filter.ML \
e34c1b09bb5e shorten a few file names
blanchet
parents: 38942
diff changeset
   374
  Tools/Sledgehammer/sledgehammer_minimize.ML \
35866
513074557e06 move the Sledgehammer Isar commands together into one file;
blanchet
parents: 35865
diff changeset
   375
  Tools/Sledgehammer/sledgehammer_isar.ML \
41087
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41065
diff changeset
   376
  Tools/Sledgehammer/sledgehammer_provers.ML \
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents: 41065
diff changeset
   377
  Tools/Sledgehammer/sledgehammer_run.ML \
35967
b9659daa5b4b add new file "sledgehammer_util.ML" to setup
blanchet
parents: 35892
diff changeset
   378
  Tools/Sledgehammer/sledgehammer_util.ML \
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
   379
  Tools/SMT/smtlib_interface.ML \
40277
4e3a3461c1a6 added crafted list of SMT built-in constants
boehmes
parents: 40239
diff changeset
   380
  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
   381
  Tools/SMT/smt_config.ML \
41426
09615ed31f04 re-implemented support for datatypes (including records and typedefs);
boehmes
parents: 41413
diff changeset
   382
  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
   383
  Tools/SMT/smt_failure.ML \
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
   384
  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
   385
  Tools/SMT/smt_setup_solvers.ML \
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
   386
  Tools/SMT/smt_solver.ML \
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
   387
  Tools/SMT/smt_translate.ML \
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents: 40650
diff changeset
   388
  Tools/SMT/smt_utils.ML \
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
   389
  Tools/SMT/z3_interface.ML \
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
   390
  Tools/SMT/z3_model.ML \
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
   391
  Tools/SMT/z3_proof_literals.ML \
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents: 40650
diff changeset
   392
  Tools/SMT/z3_proof_methods.ML \
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
   393
  Tools/SMT/z3_proof_parser.ML \
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
   394
  Tools/SMT/z3_proof_reconstruction.ML \
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
   395
  Tools/SMT/z3_proof_tools.ML \
31055
2cf6efca6c71 proper structures for list and string code generation stuff
haftmann
parents: 31048
diff changeset
   396
  Tools/string_code.ML \
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   397
  Tools/string_syntax.ML \
47325
ec6187036495 new transfer proof method
huffman
parents: 47324
diff changeset
   398
  Tools/transfer.ML \
28401
d5f39173444c separate HOL-Main image
haftmann
parents: 28393
diff changeset
   399
d5f39173444c separate HOL-Main image
haftmann
parents: 28393
diff changeset
   400
$(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES)
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   401
	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
28401
d5f39173444c separate HOL-Main image
haftmann
parents: 28393
diff changeset
   402
34205
f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents: 34126
diff changeset
   403
HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \
30096
c5497842ee35 new theory of Archimedean fields
huffman
parents: 30049
diff changeset
   404
  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
   405
  Complex.thy \
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28905
diff changeset
   406
  Complex_Main.thy \
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28905
diff changeset
   407
  Deriv.thy \
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28905
diff changeset
   408
  Fact.thy \
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   409
  GCD.thy \
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28905
diff changeset
   410
  Lim.thy \
31352
b3b534f06c2d add dependency on Limits.thy
huffman
parents: 31283
diff changeset
   411
  Limits.thy \
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28905
diff changeset
   412
  Ln.thy \
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28905
diff changeset
   413
  Log.thy \
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   414
  Lubs.thy \
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28905
diff changeset
   415
  MacLaurin.thy \
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28905
diff changeset
   416
  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
   417
  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
   418
  RComplete.thy \
35372
ca158c7b1144 renamed theory Rational to Rat
haftmann
parents: 35329
diff changeset
   419
  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
   420
  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
   421
  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
   422
  RealVector.thy \
29197
6d4cb27ed19c adapted HOL source structure to distribution layout
haftmann
parents: 29181
diff changeset
   423
  SEQ.thy \
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28905
diff changeset
   424
  Series.thy \
33269
3b7e2dbbd684 New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents: 33083
diff changeset
   425
  SupInf.thy \
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28905
diff changeset
   426
  Taylor.thy \
40839
48e01d16dd17 activate subtyping/coercions in theory Complex_Main;
wenzelm
parents: 40837
diff changeset
   427
  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
   428
  Tools/float_syntax.ML \
40839
48e01d16dd17 activate subtyping/coercions in theory Complex_Main;
wenzelm
parents: 40837
diff changeset
   429
  Transcendental.thy
34205
f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents: 34126
diff changeset
   430
f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents: 34126
diff changeset
   431
$(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
   432
	@$(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
   433
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents: 7513
diff changeset
   434
10255
bb66874b4750 added HOL/Library, rearranged several files;
wenzelm
parents: 10214
diff changeset
   435
## HOL-Library
bb66874b4750 added HOL/Library, rearranged several files;
wenzelm
parents: 10214
diff changeset
   436
37691
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
   437
HOL-Library: HOL $(OUT)/HOL-Library
10255
bb66874b4750 added HOL/Library, rearranged several files;
wenzelm
parents: 10214
diff changeset
   438
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
   439
$(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
   440
  $(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
   441
  Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy		\
46238
9ace9e5b79be renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)
bulwahn
parents: 46237
diff changeset
   442
  Library/AList.thy Library/AList_Mapping.thy 				\
44897
787983a08bfb moving connection of association lists to Mappings into a separate theory
bulwahn
parents: 44860
diff changeset
   443
  Library/BigO.thy Library/Binomial.thy 				\
37968
52fdcb76c0af added Code_Natural.thy
haftmann
parents: 37921
diff changeset
   444
  Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy	\
37662
35c060043a5a repaired line ending
haftmann
parents: 37660
diff changeset
   445
  Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy	\
43919
a7e4fb1a0502 rename Nat_Infinity (inat) to Extended_Nat (enat)
hoelzl
parents: 43834
diff changeset
   446
  Library/Code_Char_ord.thy Library/Code_Integer.thy			\
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   447
  Library/Code_Nat.thy Library/Code_Natural.thy				\
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   448
  Library/Efficient_Nat.thy Library/Code_Prolog.thy			\
45483
34d07cf7d207 add Code_Real_Approx_By_Float
hoelzl
parents: 45357
diff changeset
   449
  Library/Code_Real_Approx_By_Float.thy					\
43919
a7e4fb1a0502 rename Nat_Infinity (inat) to Extended_Nat (enat)
hoelzl
parents: 43834
diff changeset
   450
  Tools/Predicate_Compile/code_prolog.ML Library/ContNotDenum.thy	\
47232
e2f0176149d0 dropped now obsolete Cset theories
haftmann
parents: 47223
diff changeset
   451
  Library/Continuity.thy						\
45748
cf79cc09cab4 remove Library/Diagonalize.thy, because Library/Nat_Bijection.thy includes all the same functionality
huffman
parents: 45716
diff changeset
   452
  Library/Convex.thy Library/Countable.thy				\
47232
e2f0176149d0 dropped now obsolete Cset theories
haftmann
parents: 47223
diff changeset
   453
  Library/Dlist.thy Library/Eval_Witness.thy				\
e2f0176149d0 dropped now obsolete Cset theories
haftmann
parents: 47223
diff changeset
   454
  Library/DAList.thy Library/Dlist.thy					\
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   455
  Library/Eval_Witness.thy						\
44236
b73b7832b384 moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents: 44145
diff changeset
   456
  Library/Extended_Real.thy Library/Extended_Nat.thy Library/Float.thy	\
43919
a7e4fb1a0502 rename Nat_Infinity (inat) to Extended_Nat (enat)
hoelzl
parents: 43834
diff changeset
   457
  Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
47232
e2f0176149d0 dropped now obsolete Cset theories
haftmann
parents: 47223
diff changeset
   458
  Library/FrechetDeriv.thy Library/FuncSet.thy				\
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   459
  Library/Function_Algebras.thy Library/Fundamental_Theorem_Algebra.thy	\
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   460
  Library/Glbs.thy Library/Indicator_Function.thy			\
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   461
  Library/Infinite_Set.thy Library/Inner_Product.thy			\
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   462
  Library/Kleene_Algebra.thy Library/LaTeXsugar.thy			\
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   463
  Library/Lattice_Algebras.thy Library/Lattice_Syntax.thy		\
47232
e2f0176149d0 dropped now obsolete Cset theories
haftmann
parents: 47223
diff changeset
   464
  Library/Library.thy Library/List_Prefix.thy				\
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   465
  Library/List_lexord.thy Library/Mapping.thy Library/Monad_Syntax.thy	\
44236
b73b7832b384 moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents: 44145
diff changeset
   466
  Library/Multiset.thy Library/Nat_Bijection.thy			\
b73b7832b384 moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents: 44145
diff changeset
   467
  Library/Numeral_Type.thy Library/Old_Recdef.thy			\
b73b7832b384 moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents: 44145
diff changeset
   468
  Library/OptionalSugar.thy Library/Order_Relation.thy			\
b73b7832b384 moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents: 44145
diff changeset
   469
  Library/Permutation.thy Library/Permutations.thy			\
b73b7832b384 moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents: 44145
diff changeset
   470
  Library/Poly_Deriv.thy Library/Polynomial.thy				\
b73b7832b384 moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents: 44145
diff changeset
   471
  Library/Predicate_Compile_Quickcheck.thy Library/Preorder.thy		\
b73b7832b384 moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents: 44145
diff changeset
   472
  Library/Product_Vector.thy Library/Product_ord.thy			\
b73b7832b384 moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents: 44145
diff changeset
   473
  Library/Product_plus.thy Library/Product_Lattice.thy			\
b73b7832b384 moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents: 44145
diff changeset
   474
  Library/Quickcheck_Types.thy Library/Quotient_List.thy		\
b73b7832b384 moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents: 44145
diff changeset
   475
  Library/Quotient_Option.thy Library/Quotient_Product.thy		\
45074
04286b0fc856 Quotient_Set.thy is part of library
haftmann
parents: 45070
diff changeset
   476
  Library/Quotient_Set.thy Library/Quotient_Sum.thy			\
04286b0fc856 Quotient_Set.thy is part of library
haftmann
parents: 45070
diff changeset
   477
  Library/Quotient_Syntax.thy Library/Quotient_Type.thy Library/RBT.thy	\
04286b0fc856 Quotient_Set.thy is part of library
haftmann
parents: 45070
diff changeset
   478
  Library/RBT_Impl.thy Library/RBT_Mapping.thy Library/README.html	\
04286b0fc856 Quotient_Set.thy is part of library
haftmann
parents: 45070
diff changeset
   479
  Library/Saturated.thy Library/Set_Algebras.thy			\
04286b0fc856 Quotient_Set.thy is part of library
haftmann
parents: 45070
diff changeset
   480
  Library/State_Monad.thy Library/Ramsey.thy				\
44818
27ba81ad0890 theory of saturated naturals contributed by Peter Gammie
haftmann
parents: 44657
diff changeset
   481
  Library/Reflection.thy Library/Sublist_Order.thy			\
27ba81ad0890 theory of saturated naturals contributed by Peter Gammie
haftmann
parents: 44657
diff changeset
   482
  Library/Sum_of_Squares.thy Library/Sum_of_Squares/sos_wrapper.ML	\
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   483
  Library/Sum_of_Squares/sum_of_squares.ML Library/Target_Numeral.thy	\
42071
04577a7e0c51 move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents: 42064
diff changeset
   484
  Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy		\
44014
88bd7d74a2c1 moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef
krauss
parents: 44013
diff changeset
   485
  Library/Wfrec.thy 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
   486
  $(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML	\
37789
93f6dcf9ec02 generic ad-hoc overloading via check/uncheck
krauss
parents: 37781
diff changeset
   487
  Library/reflection.ML Library/reify_data.ML				\
44013
5cfc1c36ae97 moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents: 44006
diff changeset
   488
  Library/document/root.bib Library/document/root.tex			\
5cfc1c36ae97 moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents: 44006
diff changeset
   489
  Tools/TFL/casesplit.ML Tools/TFL/dcterm.ML Tools/TFL/post.ML		\
5cfc1c36ae97 moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents: 44006
diff changeset
   490
  Tools/TFL/rules.ML Tools/TFL/tfl.ML Tools/TFL/thms.ML			\
5cfc1c36ae97 moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents: 44006
diff changeset
   491
  Tools/TFL/thry.ML Tools/TFL/usyntax.ML Tools/TFL/utils.ML		\
5cfc1c36ae97 moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents: 44006
diff changeset
   492
  Tools/recdef.ML
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
   493
	@cd Library; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL-Library
10255
bb66874b4750 added HOL/Library, rearranged several files;
wenzelm
parents: 10214
diff changeset
   494
bb66874b4750 added HOL/Library, rearranged several files;
wenzelm
parents: 10214
diff changeset
   495
31795
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 31771
diff changeset
   496
## HOL-Hahn_Banach
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   497
31795
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 31771
diff changeset
   498
HOL-Hahn_Banach: HOL $(LOG)/HOL-Hahn_Banach.gz
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   499
31795
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 31771
diff changeset
   500
$(LOG)/HOL-Hahn_Banach.gz: $(OUT)/HOL Hahn_Banach/Bounds.thy		\
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 31771
diff changeset
   501
  Hahn_Banach/Function_Norm.thy Hahn_Banach/Function_Order.thy		\
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 31771
diff changeset
   502
  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
   503
  Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Hahn_Banach/Linearform.thy	\
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 31771
diff changeset
   504
  Hahn_Banach/Normed_Space.thy Hahn_Banach/README.html			\
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 31771
diff changeset
   505
  Hahn_Banach/ROOT.ML Hahn_Banach/Subspace.thy				\
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 31771
diff changeset
   506
  Hahn_Banach/Vector_Space.thy Hahn_Banach/Zorn_Lemma.thy		\
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 31771
diff changeset
   507
  Hahn_Banach/document/root.bib Hahn_Banach/document/root.tex
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 31771
diff changeset
   508
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hahn_Banach
27421
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   509
7e458bd56860 HOL += HOL-Complex
haftmann
parents: 27396
diff changeset
   510
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   511
## HOL-Induct
2473
3eb12c85846c minor tuning;
wenzelm
parents: 2448
diff changeset
   512
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   513
HOL-Induct: HOL $(LOG)/HOL-Induct.gz
3125
3f0ab2c306f7 Moved induction examples to directory Induct
paulson
parents: 3118
diff changeset
   514
33688
1a97dcd8dc6a moved old SList, LList, LFilter to AFP/Lazy-Lists-II;
wenzelm
parents: 33649
diff changeset
   515
$(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
   516
  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
   517
  Induct/QuoDataType.thy Induct/ROOT.ML Induct/Sexp.thy			\
35249
7024a8a8f36a more precise dependencies;
wenzelm
parents: 35222
diff changeset
   518
  Induct/Sigma_Algebra.thy Induct/ABexp.thy Induct/SList.thy		\
7024a8a8f36a more precise dependencies;
wenzelm
parents: 35222
diff changeset
   519
  Induct/Term.thy Induct/Tree.thy Induct/document/root.tex
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   520
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Induct
3125
3f0ab2c306f7 Moved induction examples to directory Induct
paulson
parents: 3118
diff changeset
   521
3f0ab2c306f7 Moved induction examples to directory Induct
paulson
parents: 3118
diff changeset
   522
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   523
## HOL-IMP
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   524
43917
bce3de79c8ce build an image for HOL-IMP
kleing
parents: 43834
diff changeset
   525
HOL-IMP: HOL $(OUT)/HOL-IMP
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   526
45112
32c90199df2e Added dependecies
nipkow
parents: 45111
diff changeset
   527
$(OUT)/HOL-IMP: $(OUT)/HOL \
45747
8b05cda62000 missing dependency
nipkow
parents: 45716
diff changeset
   528
  IMP/ACom.thy IMP/Abs_Int0_fun.thy IMP/Abs_State.thy IMP/Abs_Int0.thy \
45112
32c90199df2e Added dependecies
nipkow
parents: 45111
diff changeset
   529
  IMP/Abs_Int0_const.thy IMP/Abs_Int1.thy IMP/Abs_Int1_ivl.thy \
32c90199df2e Added dependecies
nipkow
parents: 45111
diff changeset
   530
  IMP/Abs_Int2.thy IMP/Abs_Int_Den/Abs_Int_den0_fun.thy \
45111
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents: 45110
diff changeset
   531
  IMP/Abs_Int_Den/Abs_State_den.thy  IMP/Abs_Int_Den/Abs_Int_den0.thy \
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents: 45110
diff changeset
   532
  IMP/Abs_Int_Den/Abs_Int_den0_const.thy IMP/Abs_Int_Den/Abs_Int_den1.thy \
054a9ac0d7ef Added Hoare-like Abstract Interpretation
nipkow
parents: 45110
diff changeset
   533
  IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy IMP/Abs_Int_Den/Abs_Int_den2.thy \
45885
nipkow
parents: 45812
diff changeset
   534
  IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy	IMP/Big_Step.thy IMP/C_like.thy \
46232
dc5f5cfe6a09 missing dependency
nipkow
parents: 46167
diff changeset
   535
  IMP/Collecting.thy IMP/Collecting_list.thy IMP/Collecting1.thy IMP/Com.thy \
dc5f5cfe6a09 missing dependency
nipkow
parents: 46167
diff changeset
   536
  IMP/Compiler.thy IMP/Comp_Rev.thy \
dc5f5cfe6a09 missing dependency
nipkow
parents: 46167
diff changeset
   537
  IMP/Def_Ass.thy IMP/Def_Ass_Big.thy IMP/Def_Ass_Exp.thy \
43158
686fa0a0696e imported rest of new IMP
kleing
parents: 43150
diff changeset
   538
  IMP/Def_Ass_Small.thy IMP/Def_Ass_Sound_Big.thy \
686fa0a0696e imported rest of new IMP
kleing
parents: 43150
diff changeset
   539
  IMP/Def_Ass_Sound_Small.thy IMP/Denotation.thy IMP/Hoare.thy \
686fa0a0696e imported rest of new IMP
kleing
parents: 43150
diff changeset
   540
  IMP/HoareT.thy IMP/Hoare_Examples.thy IMP/Hoare_Sound_Complete.thy \
45812
0b02adadf384 added IMP/Live_True.thy
nipkow
parents: 45800
diff changeset
   541
  IMP/Live.thy IMP/Live_True.thy IMP/OO.thy IMP/Poly_Types.thy IMP/Procs.thy \
43158
686fa0a0696e imported rest of new IMP
kleing
parents: 43150
diff changeset
   542
  IMP/Procs_Dyn_Vars_Dyn.thy IMP/Procs_Stat_Vars_Dyn.thy \
686fa0a0696e imported rest of new IMP
kleing
parents: 43150
diff changeset
   543
  IMP/Procs_Stat_Vars_Stat.thy IMP/Sec_Type_Expr.thy IMP/Sec_Typing.thy \
686fa0a0696e imported rest of new IMP
kleing
parents: 43150
diff changeset
   544
  IMP/Sec_TypingT.thy IMP/Small_Step.thy IMP/Star.thy IMP/Types.thy \
45716
ccf2cbe86d70 merged IMP/Util into IMP/Vars
nipkow
parents: 45680
diff changeset
   545
  IMP/VC.thy IMP/Vars.thy \
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   546
  IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib
45320
9d7b52c8eb01 moved latex generation for HOL-IMP out of distribution
kleing
parents: 45319
diff changeset
   547
	@cd IMP && $(ISABELLE_TOOL) usedir -g true -b $(OUT)/HOL HOL-IMP
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   548
8179
6a0b1037bab3 added forgotten rules to make IMPP
oheimb
parents: 8177
diff changeset
   549
## HOL-IMPP
6a0b1037bab3 added forgotten rules to make IMPP
oheimb
parents: 8177
diff changeset
   550
6a0b1037bab3 added forgotten rules to make IMPP
oheimb
parents: 8177
diff changeset
   551
HOL-IMPP: HOL $(LOG)/HOL-IMPP.gz
6a0b1037bab3 added forgotten rules to make IMPP
oheimb
parents: 8177
diff changeset
   552
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   553
$(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy		\
19803
aa2581752afb removed obsolete ML files;
wenzelm
parents: 19802
diff changeset
   554
  IMPP/Natural.thy IMPP/Hoare.thy IMPP/Misc.thy IMPP/EvenOdd.thy
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   555
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL IMPP
8179
6a0b1037bab3 added forgotten rules to make IMPP
oheimb
parents: 8177
diff changeset
   556
6a0b1037bab3 added forgotten rules to make IMPP
oheimb
parents: 8177
diff changeset
   557
47267
4c7548e7df86 merged, manually resolving conflicts due to session renaming (cf. 6488c5efec49)
krauss
parents: 47264 47263
diff changeset
   558
## HOL-Import
46785
150f37dad503 formal infrastructure for import sessions
haftmann
parents: 46722
diff changeset
   559
47264
6488c5efec49 renamed import session back to Import, conforming to directory name; NEWS
krauss
parents: 47260
diff changeset
   560
HOL-Import: $(LOG)/HOL-Import.gz
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   561
47264
6488c5efec49 renamed import session back to Import, conforming to directory name; NEWS
krauss
parents: 47260
diff changeset
   562
$(LOG)/HOL-Import.gz: $(OUT)/HOL \
47258
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents: 47232
diff changeset
   563
  Import/ROOT.ML \
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents: 47232
diff changeset
   564
  Import/Import_Setup.thy \
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents: 47232
diff changeset
   565
  Import/import_data.ML \
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents: 47232
diff changeset
   566
  Import/import_rule.ML \
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents: 47232
diff changeset
   567
  Import/HOL_Light_Maps.thy \
880e587eee9f Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents: 47232
diff changeset
   568
  Import/HOL_Light_Import.thy
47264
6488c5efec49 renamed import session back to Import, conforming to directory name; NEWS
krauss
parents: 47260
diff changeset
   569
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Import
14516
a183dec876ab Added HOL proof importer.
skalberg
parents: 14515
diff changeset
   570
47263
434d9dd99523 more precise IsaMakefile (eg. see HOL-Algebra);
wenzelm
parents: 47260
diff changeset
   571
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   572
## HOL-Number_Theory
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents: 31706
diff changeset
   573
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   574
HOL-Number_Theory: HOL $(LOG)/HOL-Number_Theory.gz
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents: 31706
diff changeset
   575
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   576
$(LOG)/HOL-Number_Theory.gz: $(OUT)/HOL $(ALGEBRA_DEPENDENCIES) \
31771
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   577
  Library/Multiset.thy \
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   578
  Number_Theory/Binomial.thy \
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   579
  Number_Theory/Cong.thy \
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   580
  Number_Theory/Fib.thy \
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   581
  Number_Theory/MiscAlgebra.thy \
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   582
  Number_Theory/Number_Theory.thy \
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   583
  Number_Theory/Residues.thy \
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   584
  Number_Theory/UniqueFactorization.thy  \
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   585
  Number_Theory/ROOT.ML
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   586
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Number_Theory
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents: 41973
diff changeset
   587
31719
29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad
nipkow
parents: 31706
diff changeset
   588
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   589
## HOL-Old_Number_Theory
9510
dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied
paulson
parents: 9481
diff changeset
   590
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   591
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
   592
37021
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   593
$(LOG)/HOL-Old_Number_Theory.gz: $(OUT)/HOL Library/Permutation.thy	\
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   594
  Old_Number_Theory/Primes.thy Old_Number_Theory/Fib.thy		\
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   595
  Old_Number_Theory/Factorization.thy Old_Number_Theory/BijectionRel.thy\
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   596
  Old_Number_Theory/Chinese.thy Old_Number_Theory/EulerFermat.thy	\
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   597
  Old_Number_Theory/IntFact.thy Old_Number_Theory/IntPrimes.thy		\
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   598
  Old_Number_Theory/WilsonBij.thy Old_Number_Theory/WilsonRuss.thy	\
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   599
  Old_Number_Theory/Finite2.thy Old_Number_Theory/Int2.thy		\
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   600
  Old_Number_Theory/EvenOdd.thy Old_Number_Theory/Residues.thy		\
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   601
  Old_Number_Theory/Euler.thy Old_Number_Theory/Gauss.thy		\
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   602
  Old_Number_Theory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy	\
37021
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   603
  Old_Number_Theory/Legacy_GCD.thy Old_Number_Theory/Pocklington.thy	\
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   604
  Old_Number_Theory/ROOT.ML
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   605
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Old_Number_Theory
9510
dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied
paulson
parents: 9481
diff changeset
   606
dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied
paulson
parents: 9481
diff changeset
   607
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   608
## HOL-Hoare
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   609
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   610
HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   611
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   612
$(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.thy Hoare/Examples.thy	\
42153
fa108629d132 use shared copy of hoare_syntax.ML;
wenzelm
parents: 42148
diff changeset
   613
  Hoare/Hoare.thy Hoare/hoare_syntax.ML Hoare/hoare_tac.ML		\
fa108629d132 use shared copy of hoare_syntax.ML;
wenzelm
parents: 42148
diff changeset
   614
  Hoare/Heap.thy Hoare/Hoare_Logic.thy Hoare/Hoare_Logic_Abort.thy	\
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   615
  Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy Hoare/ROOT.ML		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   616
  Hoare/ExamplesAbort.thy Hoare/HeapSyntaxAbort.thy			\
42153
fa108629d132 use shared copy of hoare_syntax.ML;
wenzelm
parents: 42148
diff changeset
   617
  Hoare/SchorrWaite.thy Hoare/Separation.thy Hoare/SepLogHeap.thy	\
fa108629d132 use shared copy of hoare_syntax.ML;
wenzelm
parents: 42148
diff changeset
   618
  Hoare/document/root.tex Hoare/document/root.bib
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   619
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Hoare
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   620
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   621
32621
a073cb249a06 theory entry point for session Hoare_Parallel (now also with proper underscore)
haftmann
parents: 32618
diff changeset
   622
## HOL-Hoare_Parallel
12996
7ac0a7e306db Completed annonce of HoareParallel
prensani
parents: 12951
diff changeset
   623
32621
a073cb249a06 theory entry point for session Hoare_Parallel (now also with proper underscore)
haftmann
parents: 32618
diff changeset
   624
HOL-Hoare_Parallel: HOL $(LOG)/HOL-Hoare_Parallel.gz
12996
7ac0a7e306db Completed annonce of HoareParallel
prensani
parents: 12951
diff changeset
   625
32621
a073cb249a06 theory entry point for session Hoare_Parallel (now also with proper underscore)
haftmann
parents: 32618
diff changeset
   626
$(LOG)/HOL-Hoare_Parallel.gz: $(OUT)/HOL Hoare_Parallel/Gar_Coll.thy	\
33439
f5d95787224f more accurate dependencies;
wenzelm
parents: 33437
diff changeset
   627
  Hoare_Parallel/Graph.thy Hoare_Parallel/Hoare_Parallel.thy		\
f5d95787224f more accurate dependencies;
wenzelm
parents: 33437
diff changeset
   628
  Hoare_Parallel/Mul_Gar_Coll.thy Hoare_Parallel/OG_Com.thy		\
f5d95787224f more accurate dependencies;
wenzelm
parents: 33437
diff changeset
   629
  Hoare_Parallel/OG_Examples.thy Hoare_Parallel/OG_Hoare.thy		\
f5d95787224f more accurate dependencies;
wenzelm
parents: 33437
diff changeset
   630
  Hoare_Parallel/OG_Syntax.thy Hoare_Parallel/OG_Tactics.thy		\
f5d95787224f more accurate dependencies;
wenzelm
parents: 33437
diff changeset
   631
  Hoare_Parallel/OG_Tran.thy Hoare_Parallel/Quote_Antiquote.thy		\
f5d95787224f more accurate dependencies;
wenzelm
parents: 33437
diff changeset
   632
  Hoare_Parallel/RG_Com.thy Hoare_Parallel/RG_Examples.thy		\
f5d95787224f more accurate dependencies;
wenzelm
parents: 33437
diff changeset
   633
  Hoare_Parallel/RG_Hoare.thy Hoare_Parallel/RG_Syntax.thy		\
f5d95787224f more accurate dependencies;
wenzelm
parents: 33437
diff changeset
   634
  Hoare_Parallel/RG_Tran.thy Hoare_Parallel/ROOT.ML			\
f5d95787224f more accurate dependencies;
wenzelm
parents: 33437
diff changeset
   635
  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
   636
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hoare_Parallel
12996
7ac0a7e306db Completed annonce of HoareParallel
prensani
parents: 12951
diff changeset
   637
7ac0a7e306db Completed annonce of HoareParallel
prensani
parents: 12951
diff changeset
   638
37747
3a699743bcba more accurate dependencies
haftmann
parents: 37742
diff changeset
   639
## HOL-Library-Codegenerator_Test
37691
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
   640
37747
3a699743bcba more accurate dependencies
haftmann
parents: 37742
diff changeset
   641
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
   642
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   643
$(LOG)/HOL-Library-Codegenerator_Test.gz: $(OUT)/HOL-Library \
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   644
  Codegenerator_Test/ROOT.ML \
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   645
  Codegenerator_Test/Candidates.thy \
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   646
  Codegenerator_Test/Candidates_Pretty.thy \
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   647
  Codegenerator_Test/Generate.thy \
37691
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
   648
  Codegenerator_Test/Generate_Pretty.thy
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
   649
	@$(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
   650
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents: 37672
diff changeset
   651
33027
9cf389429f6d modernized session Metis_Examples;
wenzelm
parents: 33026
diff changeset
   652
## HOL-Metis_Examples
23449
dd874e6a3282 integration of Metis prover
paulson
parents: 23445
diff changeset
   653
33027
9cf389429f6d modernized session Metis_Examples;
wenzelm
parents: 33026
diff changeset
   654
HOL-Metis_Examples: HOL $(LOG)/HOL-Metis_Examples.gz
23449
dd874e6a3282 integration of Metis prover
paulson
parents: 23445
diff changeset
   655
41144
509e51b7509a example tuning
blanchet
parents: 41112
diff changeset
   656
$(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML \
43197
c71657bbdbc0 tuned Metis examples
blanchet
parents: 43162
diff changeset
   657
  Metis_Examples/Abstraction.thy Metis_Examples/Big_O.thy \
c71657bbdbc0 tuned Metis examples
blanchet
parents: 43162
diff changeset
   658
  Metis_Examples/Binary_Tree.thy Metis_Examples/Clausification.thy \
c71657bbdbc0 tuned Metis examples
blanchet
parents: 43162
diff changeset
   659
  Metis_Examples/Message.thy Metis_Examples/Proxies.thy \
c71657bbdbc0 tuned Metis examples
blanchet
parents: 43162
diff changeset
   660
  Metis_Examples/Sets.thy Metis_Examples/Tarski.thy \
c71657bbdbc0 tuned Metis examples
blanchet
parents: 43162
diff changeset
   661
  Metis_Examples/Trans_Closure.thy Metis_Examples/Type_Encodings.thy
33027
9cf389429f6d modernized session Metis_Examples;
wenzelm
parents: 33026
diff changeset
   662
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples
23449
dd874e6a3282 integration of Metis prover
paulson
parents: 23445
diff changeset
   663
dd874e6a3282 integration of Metis prover
paulson
parents: 23445
diff changeset
   664
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents: 33192
diff changeset
   665
## HOL-Nitpick_Examples
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents: 33192
diff changeset
   666
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents: 33192
diff changeset
   667
HOL-Nitpick_Examples: HOL $(LOG)/HOL-Nitpick_Examples.gz
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents: 33192
diff changeset
   668
34126
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34069
diff changeset
   669
$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \
8a2c5d7aff51 polished Nitpick's binary integer support etc.;
blanchet
parents: 34069
diff changeset
   670
  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
   671
  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
   672
  Nitpick_Examples/Integer_Nits.thy Nitpick_Examples/Manual_Nits.thy \
45035
60d2c03d5c70 reintroduced Minipick as Nitpick example
blanchet
parents: 45021
diff changeset
   673
  Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy \
60d2c03d5c70 reintroduced Minipick as Nitpick example
blanchet
parents: 45021
diff changeset
   674
  Nitpick_Examples/Nitpick_Examples.thy Nitpick_Examples/Pattern_Nits.thy \
60d2c03d5c70 reintroduced Minipick as Nitpick example
blanchet
parents: 45021
diff changeset
   675
  Nitpick_Examples/Record_Nits.thy Nitpick_Examples/Refute_Nits.thy \
60d2c03d5c70 reintroduced Minipick as Nitpick example
blanchet
parents: 45021
diff changeset
   676
  Nitpick_Examples/Special_Nits.thy Nitpick_Examples/Tests_Nits.thy \
60d2c03d5c70 reintroduced Minipick as Nitpick example
blanchet
parents: 45021
diff changeset
   677
  Nitpick_Examples/Typedef_Nits.thy Nitpick_Examples/minipick.ML
33197
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents: 33192
diff changeset
   678
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents: 33192
diff changeset
   679
de6285ebcc05 continuation of Nitpick's integration into Isabelle;
blanchet
parents: 33192
diff changeset
   680
7999
7acf6eb8eec1 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents: 7985
diff changeset
   681
## HOL-Algebra
7acf6eb8eec1 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents: 7985
diff changeset
   682
33439
f5d95787224f more accurate dependencies;
wenzelm
parents: 33437
diff changeset
   683
HOL-Algebra: HOL $(OUT)/HOL-Algebra
7999
7acf6eb8eec1 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents: 7985
diff changeset
   684
31771
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   685
ALGEBRA_DEPENDENCIES = $(OUT)/HOL \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   686
  Algebra/ROOT.ML \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   687
  Library/Binomial.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   688
  Library/FuncSet.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   689
  Library/Multiset.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   690
  Library/Permutation.thy \
32479
521cc9bf2958 some reorganization of number theory
haftmann
parents: 32402
diff changeset
   691
  Number_Theory/Primes.thy \
31771
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   692
  Algebra/AbelCoset.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   693
  Algebra/Bij.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   694
  Algebra/Congruence.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   695
  Algebra/Coset.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   696
  Algebra/Divisibility.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   697
  Algebra/Exponent.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   698
  Algebra/FiniteProduct.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   699
  Algebra/Group.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   700
  Algebra/Ideal.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   701
  Algebra/IntRing.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   702
  Algebra/Lattice.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   703
  Algebra/Module.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   704
  Algebra/QuotRing.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   705
  Algebra/Ring.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   706
  Algebra/RingHom.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   707
  Algebra/Sylow.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   708
  Algebra/UnivPoly.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   709
  Algebra/abstract/Abstract.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   710
  Algebra/abstract/Factor.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   711
  Algebra/abstract/Field.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   712
  Algebra/abstract/Ideal2.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   713
  Algebra/abstract/PID.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   714
  Algebra/abstract/Ring2.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   715
  Algebra/abstract/RingHomo.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   716
  Algebra/document/root.tex \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   717
  Algebra/document/root.tex \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   718
  Algebra/poly/LongDiv.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   719
  Algebra/poly/PolyHomo.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   720
  Algebra/poly/Polynomial.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   721
  Algebra/poly/UnivPoly2.thy \
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   722
  Algebra/ringsimp.ML
1a92eb45060f NewNumberTheory depends on Algebra
haftmann
parents: 31761
diff changeset
   723
33448
7f716a975ada more accurate dependencies;
wenzelm
parents: 33439
diff changeset
   724
$(OUT)/HOL-Algebra: $(ALGEBRA_DEPENDENCIES)
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   725
	@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
   726
27477
c64736fe2a1f more precise dependencies for HOL-Word and HOL-NSA;
wenzelm
parents: 27470
diff changeset
   727
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   728
## HOL-Auth
3819
5a6a6f18b109 added TLA stuff;
wenzelm
parents: 3616
diff changeset
   729
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   730
HOL-Auth: HOL $(LOG)/HOL-Auth.gz
3819
5a6a6f18b109 added TLA stuff;
wenzelm
parents: 3616
diff changeset
   731
28098
c92850d2d16c Replaced Library/NatPair by Nat_Int_Bij.
nipkow
parents: 28054
diff changeset
   732
$(LOG)/HOL-Auth.gz: $(OUT)/HOL 						\
37021
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   733
  Auth/Auth_Shared.thy Auth/Auth_Public.thy Auth/All_Symmetric.thy	\
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   734
  Auth/Guard/Auth_Guard_Shared.thy					\
87c696bfe839 adjusted
haftmann
parents: 36962
diff changeset
   735
  Auth/Guard/Auth_Guard_Public.thy					\
32632
8ae912371831 added session entry point theories
haftmann
parents: 32624
diff changeset
   736
  Auth/Smartcard/Auth_Smartcard.thy Auth/All_Symmetric.thy		\
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   737
  Auth/CertifiedEmail.thy Auth/Event.thy Auth/Message.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   738
  Auth/NS_Public.thy Auth/NS_Public_Bad.thy Auth/NS_Shared.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   739
  Auth/OtwayRees.thy Auth/OtwayReesBella.thy Auth/OtwayRees_AN.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   740
  Auth/OtwayRees_Bad.thy Auth/Public.thy Auth/ROOT.ML Auth/Recur.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   741
  Auth/Shared.thy Auth/TLS.thy Auth/WooLam.thy Auth/Kerberos_BAN.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   742
  Auth/Kerberos_BAN_Gets.thy Auth/KerberosIV.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   743
  Auth/KerberosIV_Gets.thy Auth/KerberosV.thy Auth/Yahalom.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   744
  Auth/Yahalom2.thy Auth/Yahalom_Bad.thy Auth/ZhouGollmann.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   745
  Auth/Guard/Analz.thy Auth/Guard/Extensions.thy Auth/Guard/GuardK.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   746
  Auth/Guard/Guard_Public.thy Auth/Guard/Guard_Shared.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   747
  Auth/Guard/Guard.thy Auth/Guard/List_Msg.thy				\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   748
  Auth/Guard/Guard_NS_Public.thy Auth/Guard/Guard_OtwayRees.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   749
  Auth/Guard/P1.thy Auth/Guard/P2.thy Auth/Guard/Proto.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   750
  Auth/Guard/Guard_Yahalom.thy Auth/Smartcard/EventSC.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   751
  Auth/Smartcard/ShoupRubinBella.thy Auth/Smartcard/ShoupRubin.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   752
  Auth/Smartcard/Smartcard.thy Auth/document/root.tex
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   753
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Auth
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   754
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   755
4777
379f32b0ae40 New target HOL-UNITY
paulson
parents: 4729
diff changeset
   756
## HOL-UNITY
379f32b0ae40 New target HOL-UNITY
paulson
parents: 4729
diff changeset
   757
379f32b0ae40 New target HOL-UNITY
paulson
parents: 4729
diff changeset
   758
HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz
379f32b0ae40 New target HOL-UNITY
paulson
parents: 4729
diff changeset
   759
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   760
$(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
   761
  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
   762
  UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy			\
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   763
  UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy UNITY/Guar.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   764
  UNITY/Lift_prog.thy UNITY/ListOrder.thy UNITY/ProgressSets.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   765
  UNITY/PPROD.thy UNITY/Project.thy UNITY/Rename.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   766
  UNITY/Transformers.thy UNITY/SubstAx.thy UNITY/UNITY.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   767
  UNITY/Union.thy UNITY/WFair.thy UNITY/Simple/Channel.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   768
  UNITY/Simple/Common.thy UNITY/Simple/Deadlock.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   769
  UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy				\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   770
  UNITY/Simple/NSP_Bad.thy UNITY/Simple/Network.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   771
  UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   772
  UNITY/Simple/Token.thy UNITY/Comp/Alloc.thy UNITY/Comp/AllocBase.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   773
  UNITY/Comp/AllocImpl.thy UNITY/Comp/Client.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   774
  UNITY/Comp/Counter.thy UNITY/Comp/Counterc.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   775
  UNITY/Comp/Handshake.thy UNITY/Comp/PriorityAux.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   776
  UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   777
  UNITY/Comp/TimerArray.thy UNITY/document/root.tex
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   778
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL UNITY
4777
379f32b0ae40 New target HOL-UNITY
paulson
parents: 4729
diff changeset
   779
379f32b0ae40 New target HOL-UNITY
paulson
parents: 4729
diff changeset
   780
10966
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
   781
## HOL-Unix
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
   782
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
   783
HOL-Unix: HOL $(LOG)/HOL-Unix.gz
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
   784
44236
b73b7832b384 moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents: 44145
diff changeset
   785
$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/List_Prefix.thy Unix/ROOT.ML	\
b73b7832b384 moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents: 44145
diff changeset
   786
  Unix/Nested_Environment.thy Unix/Unix.thy Unix/document/root.bib	\
b73b7832b384 moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents: 44145
diff changeset
   787
  Unix/document/root.tex
39156
b4f18ac786fa modernized session ROOT setup;
wenzelm
parents: 39048
diff changeset
   788
	@$(ISABELLE_TOOL) usedir -m no_brackets -m no_type_brackets $(OUT)/HOL Unix
10966
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
   789
27477
c64736fe2a1f more precise dependencies for HOL-Word and HOL-NSA;
wenzelm
parents: 27470
diff changeset
   790
19203
778507520684 Added HOL-ZF to Isabelle.
obua
parents: 19192
diff changeset
   791
## HOL-ZF
778507520684 Added HOL-ZF to Isabelle.
obua
parents: 19192
diff changeset
   792
778507520684 Added HOL-ZF to Isabelle.
obua
parents: 19192
diff changeset
   793
HOL-ZF: HOL $(LOG)/HOL-ZF.gz
778507520684 Added HOL-ZF to Isabelle.
obua
parents: 19192
diff changeset
   794
39306
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   795
$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/LProd.thy \
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   796
  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
   797
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF
10966
8f2c27041a8e added HOL-Unix example;
wenzelm
parents: 10945
diff changeset
   798
27477
c64736fe2a1f more precise dependencies for HOL-Word and HOL-NSA;
wenzelm
parents: 27470
diff changeset
   799
29399
ebcd69a00872 split of Imperative_HOL theories from HOL-Library
haftmann
parents: 29197
diff changeset
   800
## HOL-Imperative_HOL
ebcd69a00872 split of Imperative_HOL theories from HOL-Library
haftmann
parents: 29197
diff changeset
   801
ebcd69a00872 split of Imperative_HOL theories from HOL-Library
haftmann
parents: 29197
diff changeset
   802
HOL-Imperative_HOL: HOL $(LOG)/HOL-Imperative_HOL.gz
ebcd69a00872 split of Imperative_HOL theories from HOL-Library
haftmann
parents: 29197
diff changeset
   803
39306
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   804
$(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL \
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   805
  Library/Code_Integer.thy \
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   806
  Library/Code_Nat.thy \
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   807
  Library/Code_Natural.thy \
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   808
  Library/Efficient_Nat.thy \
39306
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   809
  Imperative_HOL/Array.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   810
  Imperative_HOL/Heap.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   811
  Imperative_HOL/Heap_Monad.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   812
  Imperative_HOL/Imperative_HOL.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   813
  Imperative_HOL/Imperative_HOL_ex.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   814
  Imperative_HOL/Mrec.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   815
  Imperative_HOL/Ref.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   816
  Imperative_HOL/ROOT.ML \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   817
  Imperative_HOL/ex/Imperative_Quicksort.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   818
  Imperative_HOL/ex/Imperative_Reverse.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   819
  Imperative_HOL/ex/Linked_Lists.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   820
  Imperative_HOL/ex/SatChecker.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   821
  Imperative_HOL/ex/Sorted_List.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   822
  Imperative_HOL/ex/Subarray.thy \
30689
b14b2cc4e25e moved Imperative_HOL examples to Imperative_HOL/ex
haftmann
parents: 30654
diff changeset
   823
  Imperative_HOL/ex/Sublist.thy
39306
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents: 39271
diff changeset
   824
	@$(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
   825
ebcd69a00872 split of Imperative_HOL theories from HOL-Library
haftmann
parents: 29197
diff changeset
   826
29823
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
   827
## HOL-Decision_Procs
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
   828
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
   829
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
   830
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
   831
$(LOG)/HOL-Decision_Procs.gz: $(OUT)/HOL \
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   832
  Library/Code_Integer.thy \
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   833
  Library/Code_Nat.thy \
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   834
  Library/Code_Natural.thy \
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   835
  Library/Efficient_Nat.thy \
29823
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
   836
  Decision_Procs/Approximation.thy \
33356
9157d0f9f00e moved Commutative_Ring into session Decision_Procs
haftmann
parents: 33348
diff changeset
   837
  Decision_Procs/Commutative_Ring.thy \
9157d0f9f00e moved Commutative_Ring into session Decision_Procs
haftmann
parents: 33348
diff changeset
   838
  Decision_Procs/Commutative_Ring_Complete.thy \
29823
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
   839
  Decision_Procs/Cooper.thy \
35053
43175817d83b more precise dependencies;
wenzelm
parents: 35050
diff changeset
   840
  Decision_Procs/Decision_Procs.thy \
29823
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
   841
  Decision_Procs/Dense_Linear_Order.thy \
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
   842
  Decision_Procs/Ferrack.thy \
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
   843
  Decision_Procs/MIR.thy \
35053
43175817d83b more precise dependencies;
wenzelm
parents: 35050
diff changeset
   844
  Decision_Procs/Parametric_Ferrante_Rackoff.thy \
43175817d83b more precise dependencies;
wenzelm
parents: 35050
diff changeset
   845
  Decision_Procs/Polynomial_List.thy \
37120
5df087c6ce94 moved ML files where they are actually used;
wenzelm
parents: 37118
diff changeset
   846
  Decision_Procs/ROOT.ML \
35053
43175817d83b more precise dependencies;
wenzelm
parents: 35050
diff changeset
   847
  Decision_Procs/Reflected_Multivariate_Polynomial.thy \
43175817d83b more precise dependencies;
wenzelm
parents: 35050
diff changeset
   848
  Decision_Procs/commutative_ring_tac.ML \
43175817d83b more precise dependencies;
wenzelm
parents: 35050
diff changeset
   849
  Decision_Procs/cooper_tac.ML \
30429
39acdf031548 moved Decision_Procs examples to Decision_Procs/ex
haftmann
parents: 30400
diff changeset
   850
  Decision_Procs/ex/Approximation_Ex.thy \
33356
9157d0f9f00e moved Commutative_Ring into session Decision_Procs
haftmann
parents: 33348
diff changeset
   851
  Decision_Procs/ex/Commutative_Ring_Ex.thy \
35053
43175817d83b more precise dependencies;
wenzelm
parents: 35050
diff changeset
   852
  Decision_Procs/ex/Dense_Linear_Order_Ex.thy \
43175817d83b more precise dependencies;
wenzelm
parents: 35050
diff changeset
   853
  Decision_Procs/ferrack_tac.ML \
37120
5df087c6ce94 moved ML files where they are actually used;
wenzelm
parents: 37118
diff changeset
   854
  Decision_Procs/ferrante_rackoff.ML \
5df087c6ce94 moved ML files where they are actually used;
wenzelm
parents: 37118
diff changeset
   855
  Decision_Procs/ferrante_rackoff_data.ML \
5df087c6ce94 moved ML files where they are actually used;
wenzelm
parents: 37118
diff changeset
   856
  Decision_Procs/langford.ML \
5df087c6ce94 moved ML files where they are actually used;
wenzelm
parents: 37118
diff changeset
   857
  Decision_Procs/langford_data.ML \
5df087c6ce94 moved ML files where they are actually used;
wenzelm
parents: 37118
diff changeset
   858
  Decision_Procs/mir_tac.ML
29823
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
   859
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Decision_Procs
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
   860
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents: 29813
diff changeset
   861
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
   862
## 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
   863
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
   864
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
   865
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
   866
$(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
   867
	@$(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
   868
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
   869
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
   870
## 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
   871
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
   872
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
   873
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
   874
$(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
   875
  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
   876
	@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
   877
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
   878
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
   879
## 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
   880
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
   881
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
   882
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
   883
$(LOG)/HOL-Proofs-Extraction.gz: $(OUT)/HOL-Proofs		\
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   884
  Library/Code_Integer.thy Library/Code_Nat.thy			\
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   885
  Library/Code_Natural.thy Library/Efficient_Nat.thy		\
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   886
  Proofs/Extraction/Euclid.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
   887
  Proofs/Extraction/Greatest_Common_Divisor.thy			\
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   888
  Proofs/Extraction/Higman.thy					\
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
   889
  Proofs/Extraction/Higman_Extraction.thy			\
45047
3aa8d3c391a4 Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents: 45044
diff changeset
   890
  Proofs/Extraction/Pigeonhole.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
   891
  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
   892
  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
   893
  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
   894
  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
   895
	@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
   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
34205
f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents: 34126
diff changeset
   898
## HOL-Proofs-Lambda
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   899
34205
f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents: 34126
diff changeset
   900
HOL-Proofs-Lambda: HOL-Proofs $(LOG)/HOL-Proofs-Lambda.gz
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   901
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
   902
$(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
   903
  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
   904
  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
   905
  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
   906
  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
   907
  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
   908
  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
   909
  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
   910
  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
   911
	@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
   912
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   913
9015
8006e9009621 added HOL/Prolog
oheimb
parents: 8958
diff changeset
   914
## HOL-Prolog
8006e9009621 added HOL/Prolog
oheimb
parents: 8958
diff changeset
   915
8006e9009621 added HOL/Prolog
oheimb
parents: 8958
diff changeset
   916
HOL-Prolog: HOL $(LOG)/HOL-Prolog.gz
8006e9009621 added HOL/Prolog
oheimb
parents: 8958
diff changeset
   917
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   918
$(LOG)/HOL-Prolog.gz: $(OUT)/HOL Prolog/ROOT.ML Prolog/prolog.ML	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   919
  Prolog/HOHH.thy Prolog/Test.thy Prolog/Func.thy Prolog/Type.thy
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   920
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Prolog
9015
8006e9009621 added HOL/Prolog
oheimb
parents: 8958
diff changeset
   921
8006e9009621 added HOL/Prolog
oheimb
parents: 8958
diff changeset
   922
8012
bbdf3c51c3b8 Added MicroJava
nipkow
parents: 8008
diff changeset
   923
## HOL-MicroJava
bbdf3c51c3b8 Added MicroJava
nipkow
parents: 8008
diff changeset
   924
bbdf3c51c3b8 Added MicroJava
nipkow
parents: 8008
diff changeset
   925
HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
bbdf3c51c3b8 Added MicroJava
nipkow
parents: 8008
diff changeset
   926
46722
d0491ab69c84 removed dead code (cf. a34d89ce6097);
wenzelm
parents: 46701
diff changeset
   927
$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL MicroJava/ROOT.ML			\
d0491ab69c84 removed dead code (cf. a34d89ce6097);
wenzelm
parents: 46701
diff changeset
   928
  MicroJava/Comp/AuxLemmas.thy MicroJava/Comp/CorrComp.thy		\
d0491ab69c84 removed dead code (cf. a34d89ce6097);
wenzelm
parents: 46701
diff changeset
   929
  MicroJava/Comp/CorrCompTp.thy MicroJava/Comp/DefsComp.thy		\
d0491ab69c84 removed dead code (cf. a34d89ce6097);
wenzelm
parents: 46701
diff changeset
   930
  MicroJava/Comp/Index.thy MicroJava/Comp/LemmasComp.thy		\
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   931
  MicroJava/Comp/TranslComp.thy MicroJava/Comp/TranslCompTp.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   932
  MicroJava/Comp/TypeInf.thy MicroJava/J/Conform.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   933
  MicroJava/J/Eval.thy MicroJava/J/JBasis.thy				\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   934
  MicroJava/J/JTypeSafe.thy MicroJava/J/Decl.thy MicroJava/J/State.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   935
  MicroJava/J/Term.thy MicroJava/J/Type.thy MicroJava/J/TypeRel.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   936
  MicroJava/J/WellForm.thy MicroJava/J/Value.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   937
  MicroJava/J/WellType.thy MicroJava/J/Example.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   938
  MicroJava/J/JListExample.thy MicroJava/JVM/JVMExec.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   939
  MicroJava/JVM/JVMInstructions.thy MicroJava/JVM/JVMState.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   940
  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
   941
  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
   942
  MicroJava/DFA/Err.thy MicroJava/DFA/Kildall.thy			\
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents: 33820
diff changeset
   943
  MicroJava/DFA/LBVComplete.thy MicroJava/DFA/LBVCorrect.thy		\
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents: 33820
diff changeset
   944
  MicroJava/DFA/LBVSpec.thy MicroJava/DFA/Listn.thy			\
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents: 33820
diff changeset
   945
  MicroJava/DFA/Opt.thy MicroJava/DFA/Product.thy			\
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents: 33820
diff changeset
   946
  MicroJava/DFA/SemilatAlg.thy MicroJava/DFA/Semilat.thy		\
46722
d0491ab69c84 removed dead code (cf. a34d89ce6097);
wenzelm
parents: 46701
diff changeset
   947
  MicroJava/DFA/Semilattices.thy					\
d0491ab69c84 removed dead code (cf. a34d89ce6097);
wenzelm
parents: 46701
diff changeset
   948
  MicroJava/DFA/Typing_Framework_err.thy				\
33954
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents: 33820
diff changeset
   949
  MicroJava/DFA/Typing_Framework.thy MicroJava/BV/BVSpec.thy		\
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   950
  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
   951
  MicroJava/BV/JType.thy MicroJava/BV/JVM.thy MicroJava/BV/JVMType.thy	\
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   952
  MicroJava/BV/Effect.thy MicroJava/BV/EffectMono.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   953
  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
   954
  MicroJava/BV/LBVJVM.thy MicroJava/document/root.bib			\
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents: 33820
diff changeset
   955
  MicroJava/document/root.tex MicroJava/document/introduction.tex
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   956
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL MicroJava
11850
cdfc3fce577e document graphs for several sessions;
wenzelm
parents: 11837
diff changeset
   957
8012
bbdf3c51c3b8 Added MicroJava
nipkow
parents: 8008
diff changeset
   958
11376
bf98ad1c22c6 added NanoJava
oheimb
parents: 11370
diff changeset
   959
## HOL-NanoJava
bf98ad1c22c6 added NanoJava
oheimb
parents: 11370
diff changeset
   960
bf98ad1c22c6 added NanoJava
oheimb
parents: 11370
diff changeset
   961
HOL-NanoJava: HOL $(LOG)/HOL-NanoJava.gz
bf98ad1c22c6 added NanoJava
oheimb
parents: 11370
diff changeset
   962
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   963
$(LOG)/HOL-NanoJava.gz: $(OUT)/HOL NanoJava/ROOT.ML NanoJava/Term.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   964
  NanoJava/Decl.thy NanoJava/TypeRel.thy NanoJava/State.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   965
  NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy		\
11376
bf98ad1c22c6 added NanoJava
oheimb
parents: 11370
diff changeset
   966
  NanoJava/document/root.bib NanoJava/document/root.tex
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   967
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NanoJava
11850
cdfc3fce577e document graphs for several sessions;
wenzelm
parents: 11837
diff changeset
   968
8193
33e4ec7a2daa added MicroJava/document;
wenzelm
parents: 8179
diff changeset
   969
12855
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
   970
## HOL-Bali
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
   971
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
   972
HOL-Bali: HOL $(LOG)/HOL-Bali.gz
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
   973
41960
8a399da4cde1 eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;
wenzelm
parents: 41928
diff changeset
   974
$(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/AxCompl.thy Bali/AxExample.thy	\
8a399da4cde1 eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;
wenzelm
parents: 41928
diff changeset
   975
  Bali/AxSem.thy Bali/AxSound.thy Bali/Basis.thy Bali/Conform.thy	\
8a399da4cde1 eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;
wenzelm
parents: 41928
diff changeset
   976
  Bali/Decl.thy Bali/DeclConcepts.thy Bali/Eval.thy Bali/Evaln.thy	\
8a399da4cde1 eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;
wenzelm
parents: 41928
diff changeset
   977
  Bali/Example.thy Bali/Name.thy Bali/ROOT.ML Bali/State.thy		\
8a399da4cde1 eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;
wenzelm
parents: 41928
diff changeset
   978
  Bali/Table.thy Bali/Term.thy Bali/Trans.thy Bali/Type.thy		\
8a399da4cde1 eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;
wenzelm
parents: 41928
diff changeset
   979
  Bali/TypeRel.thy Bali/TypeSafe.thy Bali/Value.thy Bali/WellForm.thy	\
8a399da4cde1 eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;
wenzelm
parents: 41928
diff changeset
   980
  Bali/DefiniteAssignment.thy Bali/DefiniteAssignmentCorrect.thy	\
8a399da4cde1 eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;
wenzelm
parents: 41928
diff changeset
   981
  Bali/WellType.thy Bali/document/root.tex
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   982
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Bali
12855
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
   983
21225338f8db Bali added
schirmer
parents: 12816
diff changeset
   984
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   985
## HOL-IOA
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   986
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   987
HOL-IOA: HOL $(LOG)/HOL-IOA.gz
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
   988
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   989
$(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.thy IOA/IOA.thy IOA/ROOT.ML	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   990
  IOA/Solve.thy
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
   991
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL IOA
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   992
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
   993
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
   994
## HOL-Lattice
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
   995
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
   996
HOL-Lattice: HOL $(LOG)/HOL-Lattice.gz
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
   997
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   998
$(LOG)/HOL-Lattice.gz: $(OUT)/HOL Lattice/Bounds.thy			\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
   999
  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
  1000
  Lattice/ROOT.ML Lattice/document/root.tex
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
  1001
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Lattice
10157
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
  1002
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents: 10143
diff changeset
  1003
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1004
## HOL-ex
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
  1005
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1006
HOL-ex: HOL $(LOG)/HOL-ex.gz
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
  1007
33439
f5d95787224f more accurate dependencies;
wenzelm
parents: 33437
diff changeset
  1008
$(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy	\
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
  1009
  Library/Code_Integer.thy Library/Code_Nat.thy				\
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
  1010
  Library/Code_Natural.thy Library/Efficient_Nat.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
  1011
  Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy		\
47223
4fc34c628474 remove content-free theory ex/Arithmetic_Series_Complex.thy
huffman
parents: 47205
diff changeset
  1012
  ex/Arith_Examples.thy ex/BT.thy					\
44276
fe769a0fcc96 avoid case-sensitive name for example theory
haftmann
parents: 44256
diff changeset
  1013
  ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradox.thy ex/CTL.thy		\
fe769a0fcc96 avoid case-sensitive name for example theory
haftmann
parents: 44256
diff changeset
  1014
  ex/Case_Product.thy ex/Chinese.thy ex/Classical.thy			\
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
  1015
  ex/Code_Nat_examples.thy						\
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
  1016
  ex/Coercion_Examples.thy ex/Coherent.thy ex/Dedekind_Real.thy		\
46395
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents: 46324
diff changeset
  1017
  ex/Eval_Examples.thy ex/Executable_Relation.thy ex/Fundefs.thy	\
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents: 46324
diff changeset
  1018
  ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy	\
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46988
diff changeset
  1019
  ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy		\
46395
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents: 46324
diff changeset
  1020
  ex/Higher_Order_Logic.thy ex/Iff_Oracle.thy ex/Induction_Schema.thy	\
44962
5554ed48b13f finite sequences as useful as introductory example;
wenzelm
parents: 44913
diff changeset
  1021
  ex/Interpretation_with_Defs.thy ex/Intuitionistic.thy			\
5554ed48b13f finite sequences as useful as introductory example;
wenzelm
parents: 44913
diff changeset
  1022
  ex/Lagrange.thy ex/List_to_Set_Comprehension_Examples.thy		\
5554ed48b13f finite sequences as useful as introductory example;
wenzelm
parents: 44913
diff changeset
  1023
  ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy ex/Meson_Test.thy	\
5554ed48b13f finite sequences as useful as introductory example;
wenzelm
parents: 44913
diff changeset
  1024
  ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy			\
46558
fdb84c40e074 renamed ex/Numeral.thy to ex/Numeral_Representation.thy
huffman
parents: 46395
diff changeset
  1025
  ex/Normalization_by_Evaluation.thy ex/Numeral_Representation.thy	\
fdb84c40e074 renamed ex/Numeral.thy to ex/Numeral_Representation.thy
huffman
parents: 46395
diff changeset
  1026
  ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy				\
46585
f462e49eaf11 moving Quickcheck's example to its own session
bulwahn
parents: 46558
diff changeset
  1027
  ex/Quicksort.thy ex/ROOT.ML						\
44276
fe769a0fcc96 avoid case-sensitive name for example theory
haftmann
parents: 44256
diff changeset
  1028
  ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy		\
fe769a0fcc96 avoid case-sensitive name for example theory
haftmann
parents: 44256
diff changeset
  1029
  ex/SAT_Examples.thy ex/Serbian.thy ex/Set_Theory.thy			\
45224
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents: 45190
diff changeset
  1030
  ex/Set_Algebras.thy ex/Simproc_Tests.thy ex/SVC_Oracle.thy		\
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents: 45190
diff changeset
  1031
  ex/sledgehammer_tactics.ML ex/Seq.thy ex/Sqrt.thy ex/Sqrt_Script.thy 	\
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents: 45190
diff changeset
  1032
  ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy	\
b1d5b3820d82 add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents: 45190
diff changeset
  1033
  ex/Tree23.thy	ex/Unification.thy ex/While_Combinator_Example.thy	\
44276
fe769a0fcc96 avoid case-sensitive name for example theory
haftmann
parents: 44256
diff changeset
  1034
  ex/document/root.bib ex/document/root.tex ex/svc_funcs.ML		\
fe769a0fcc96 avoid case-sensitive name for example theory
haftmann
parents: 44256
diff changeset
  1035
  ex/svc_test.thy ../Tools/interpretation_with_defs.ML
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
  1036
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
  1037
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
  1038
33026
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
  1039
## HOL-Isar_Examples
6445
931fc1daa8b1 added Isar_examples;
wenzelm
parents: 6440
diff changeset
  1040
33026
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
  1041
HOL-Isar_Examples: HOL $(LOG)/HOL-Isar_Examples.gz
6445
931fc1daa8b1 added Isar_examples;
wenzelm
parents: 6440
diff changeset
  1042
33026
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
  1043
$(LOG)/HOL-Isar_Examples.gz: $(OUT)/HOL Isar_Examples/Basic_Logic.thy	\
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
  1044
  Isar_Examples/Cantor.thy Isar_Examples/Drinker.thy			\
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
  1045
  Isar_Examples/Expr_Compiler.thy Isar_Examples/Fibonacci.thy		\
47295
b77980afc975 some context examples;
wenzelm
parents: 47267
diff changeset
  1046
  Isar_Examples/Group.thy Isar_Examples/Group_Context.thy		\
b77980afc975 some context examples;
wenzelm
parents: 47267
diff changeset
  1047
  Isar_Examples/Group_Notepad.thy Isar_Examples/Hoare.thy		\
33026
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
  1048
  Isar_Examples/Hoare_Ex.thy Isar_Examples/Knaster_Tarski.thy		\
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
  1049
  Isar_Examples/Mutilated_Checkerboard.thy				\
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
  1050
  Isar_Examples/Nested_Datatype.thy Isar_Examples/Peirce.thy		\
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
  1051
  Isar_Examples/Puzzle.thy Isar_Examples/Summation.thy			\
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
  1052
  Isar_Examples/ROOT.ML Isar_Examples/document/proof.sty		\
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
  1053
  Isar_Examples/document/root.bib Isar_Examples/document/root.tex	\
37672
645eb9fec794 avoid Old_Number_Theory;
wenzelm
parents: 37665
diff changeset
  1054
  Isar_Examples/document/style.tex Hoare/hoare_tac.ML			\
645eb9fec794 avoid Old_Number_Theory;
wenzelm
parents: 37665
diff changeset
  1055
  Number_Theory/Primes.thy
33026
8f35633c4922 modernized session Isar_Examples;
wenzelm
parents: 33024
diff changeset
  1056
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Isar_Examples
6445
931fc1daa8b1 added Isar_examples;
wenzelm
parents: 6440
diff changeset
  1057
931fc1daa8b1 added Isar_examples;
wenzelm
parents: 6440
diff changeset
  1058
33028
9aa8bfb1649d modernized session SET_Protocol;
wenzelm
parents: 33027
diff changeset
  1059
## HOL-SET_Protocol
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
  1060
33028
9aa8bfb1649d modernized session SET_Protocol;
wenzelm
parents: 33027
diff changeset
  1061
HOL-SET_Protocol: HOL $(LOG)/HOL-SET_Protocol.gz
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
  1062
33028
9aa8bfb1649d modernized session SET_Protocol;
wenzelm
parents: 33027
diff changeset
  1063
$(LOG)/HOL-SET_Protocol.gz: $(OUT)/HOL SET_Protocol/ROOT.ML		\
9aa8bfb1649d modernized session SET_Protocol;
wenzelm
parents: 33027
diff changeset
  1064
  SET_Protocol/Message_SET.thy SET_Protocol/Event_SET.thy		\
9aa8bfb1649d modernized session SET_Protocol;
wenzelm
parents: 33027
diff changeset
  1065
  SET_Protocol/Public_SET.thy SET_Protocol/Cardholder_Registration.thy	\
9aa8bfb1649d modernized session SET_Protocol;
wenzelm
parents: 33027
diff changeset
  1066
  SET_Protocol/Merchant_Registration.thy SET_Protocol/Purchase.thy	\
39757
21423597a80d modernized session
haftmann
parents: 39720
diff changeset
  1067
  SET_Protocol/SET_Protocol.thy SET_Protocol/document/root.tex
33028
9aa8bfb1649d modernized session SET_Protocol;
wenzelm
parents: 33027
diff changeset
  1068
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL SET_Protocol
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
  1069
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
  1070
46988
9f492f5b0cec renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents: 46951
diff changeset
  1071
## HOL-Matrix_LP
14610
9c2e31e483b2 added HOL-Matrix, added HOL/Matrix/ROOT.ML
kleing
parents: 14603
diff changeset
  1072
46988
9f492f5b0cec renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents: 46951
diff changeset
  1073
HOL-Matrix_LP: HOL $(LOG)/HOL-Matrix_LP.gz
17323
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight
obua
parents: 17308
diff changeset
  1074
46988
9f492f5b0cec renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents: 46951
diff changeset
  1075
$(LOG)/HOL-Matrix_LP.gz: $(OUT)/HOL Matrix_LP/ComputeFloat.thy		\
9f492f5b0cec renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents: 46951
diff changeset
  1076
  Matrix_LP/ComputeHOL.thy Matrix_LP/ComputeNumeral.thy			\
9f492f5b0cec renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents: 46951
diff changeset
  1077
  Matrix_LP/Compute_Oracle/Compute_Oracle.thy				\
9f492f5b0cec renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents: 46951
diff changeset
  1078
  Matrix_LP/Compute_Oracle/am.ML					\
9f492f5b0cec renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents: 46951
diff changeset
  1079
  Matrix_LP/Compute_Oracle/am_compiler.ML				\
9f492f5b0cec renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents: 46951
diff changeset
  1080
  Matrix_LP/Compute_Oracle/am_ghc.ML					\
9f492f5b0cec renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents: 46951
diff changeset
  1081
  Matrix_LP/Compute_Oracle/am_interpreter.ML				\
9f492f5b0cec renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents: 46951
diff changeset
  1082
  Matrix_LP/Compute_Oracle/am_sml.ML					\
9f492f5b0cec renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents: 46951
diff changeset
  1083
  Matrix_LP/Compute_Oracle/compute.ML					\
9f492f5b0cec renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents: 46951
diff changeset
  1084
  Matrix_LP/Compute_Oracle/linker.ML Matrix_LP/Cplex.thy		\
9f492f5b0cec renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents: 46951
diff changeset
  1085
  Matrix_LP/CplexMatrixConverter.ML Matrix_LP/Cplex_tools.ML		\
9f492f5b0cec renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents: 46951
diff changeset
  1086
  Matrix_LP/FloatSparseMatrixBuilder.ML Matrix_LP/LP.thy		\
9f492f5b0cec renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents: 46951
diff changeset
  1087
  Matrix_LP/Matrix.thy Matrix_LP/ROOT.ML Matrix_LP/SparseMatrix.thy	\
9f492f5b0cec renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents: 46951
diff changeset
  1088
  Matrix_LP/document/root.tex Matrix_LP/fspmlp.ML			\
9f492f5b0cec renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents: 46951
diff changeset
  1089
  Matrix_LP/matrixlp.ML Tools/float_arith.ML
9f492f5b0cec renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents: 46951
diff changeset
  1090
	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Matrix_LP
16873
9ed940a1bebb proving bounds for real linear programs
obua
parents: 16784
diff changeset
  1091
14199
d3b8d972a488 new session HOL-SET-Protocol
paulson
parents: 14182
diff changeset
  1092
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1093
## TLA
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1094
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1095
TLA: HOL $(OUT)/TLA
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1096
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
  1097
$(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
  1098
  TLA/ROOT.ML TLA/Stfun.thy TLA/TLA.thy
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
  1099
	@cd TLA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL TLA
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1100
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1101
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1102
## TLA-Inc
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1103
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1104
TLA-Inc: TLA $(LOG)/TLA-Inc.gz
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1105
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 21542
diff changeset
  1106
$(LOG)/TLA-Inc.gz: $(OUT)/TLA TLA/Inc/Inc.thy
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
  1107
	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Inc
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1108
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1109
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1110
## TLA-Buffer
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1111
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1112
TLA-Buffer: TLA $(LOG)/TLA-Buffer.gz
2448
61337170db84 IsaMakefile for HOL;
wenzelm
parents:
diff changeset
  1113
33024
60a098883d81 more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents: 33010
diff changeset
  1114
$(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
  1115
  TLA/Buffer/DBuffer.thy
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
  1116
	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Buffer
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1117
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1118
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1119
## TLA-Memory
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1120
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1121
TLA-Memory: TLA $(LOG)/TLA-Memory.gz
4447
b7ee449eb345 log files;
wenzelm
parents: 4289
diff changeset
  1122
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
  1123
$(LOG)/TLA-Memory.gz: $(OUT)/TLA TLA/Memory/MemClerk.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
  1124
  TLA/Memory/MemClerkParameters.thy TLA/Memory/Memory.thy		\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
  1125
  TLA/Memory/MemoryImplementation.thy TLA/Memory/MemoryParameters.thy	\
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
  1126
  TLA/Memory/ProcedureInterface.thy TLA/Memory/RPC.thy			\
21624
6f79647cf536 TLA: converted legacy ML scripts;
wenzelm
parents: 21542
diff changeset
  1127
  TLA/Memory/RPCMemoryParams.thy TLA/Memory/RPCParameters.thy
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
  1128
	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Memory
4518
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1129
74c01296e818 improved targets;
wenzelm
parents: 4455
diff changeset
  1130
43804
eb9be23db2b7 cleanly separate TPTP related files from other examples
blanchet
parents: 43800
diff changeset
  1131
## HOL-TPTP
eb9be23db2b7 cleanly separate TPTP related files from other examples
blanchet
parents: 43800
diff changeset
  1132
eb9be23db2b7 cleanly separate TPTP related files from other examples
blanchet
parents: 43800
diff changeset
  1133
HOL-TPTP: HOL $(LOG)/HOL-TPTP.gz
eb9be23db2b7 cleanly separate TPTP related files from other examples
blanchet
parents: 43800
diff changeset
  1134
46951
4e032ac36134 more precise TPTP keywords and dependencies;
wenzelm
parents: 46827
diff changeset
  1135
$(LOG)/HOL-TPTP.gz: $(OUT)/HOL \
4e032ac36134 more precise TPTP keywords and dependencies;
wenzelm
parents: 46827
diff changeset
  1136
  TPTP/ATP_Problem_Import.thy \
4e032ac36134 more precise TPTP keywords and dependencies;
wenzelm
parents: 46827
diff changeset
  1137
  TPTP/ATP_Theory_Export.thy \
4e032ac36134 more precise TPTP keywords and dependencies;
wenzelm
parents: 46827
diff changeset
  1138
  TPTP/CASC_Setup.thy \
43804
eb9be23db2b7 cleanly separate TPTP related files from other examples
blanchet
parents: 43800
diff changeset
  1139
  TPTP/ROOT.ML \
46951
4e032ac36134 more precise TPTP keywords and dependencies;
wenzelm
parents: 46827
diff changeset
  1140
  TPTP/TPTP_Parser.thy \
4e032ac36134 more precise TPTP keywords and dependencies;
wenzelm
parents: 46827
diff changeset
  1141
  TPTP/TPTP_Parser/ml_yacc_lib.ML \
4e032ac36134 more precise TPTP keywords and dependencies;
wenzelm
parents: 46827
diff changeset
  1142
  TPTP/TPTP_Parser/tptp_interpret.ML \
4e032ac36134 more precise TPTP keywords and dependencies;
wenzelm
parents: 46827
diff changeset
  1143
  TPTP/TPTP_Parser/tptp_lexyacc.ML \
4e032ac36134 more precise TPTP keywords and dependencies;
wenzelm
parents: 46827
diff changeset
  1144
  TPTP/TPTP_Parser/tptp_parser.ML \
4e032ac36134 more precise TPTP keywords and dependencies;
wenzelm
parents: 46827
diff changeset
  1145
  TPTP/TPTP_Parser/tptp_problem_name.ML \
4e032ac36134 more precise TPTP keywords and dependencies;
wenzelm
parents: 46827
diff changeset
  1146
  TPTP/TPTP_Parser/tptp_syntax.ML \
4e032ac36134 more precise TPTP keywords and dependencies;
wenzelm
parents: 46827
diff changeset
  1147
  TPTP/TPTP_Parser_Test.thy \
46324
e4bccf5ec61e added problem importer
blanchet
parents: 46321
diff changeset
  1148
  TPTP/atp_problem_import.ML \
46951
4e032ac36134 more precise TPTP keywords and dependencies;
wenzelm
parents: 46827
diff changeset
  1149
  TPTP/atp_theory_export.ML
45087
3417c1b91e3c reverted 09cdc4209d25 for formal reasons: it did not say what was "broken" nor "fixed", but broke IsaMakefile dependencies;
wenzelm
parents: 45074
diff changeset
  1150
	@$(ISABELLE_TOOL) usedir $(OUT)/HOL TPTP
43804
eb9be23db2b7 cleanly separate TPTP related files from other examples
blanchet
parents: 43800
diff changeset
  1151
eb9be23db2b7 cleanly separate TPTP related files from other examples
blanchet
parents: 43800
diff changeset
  1152
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents: 33083
diff changeset
  1153
## HOL-Multivariate_Analysis
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents: 33083
diff changeset
  1154
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
  1155
HOL-Multivariate_Analysis: HOL $(OUT)/HOL-Multivariate_Analysis
33175
2083bde13ce1 distinguished session for multivariate analysis
himmelma
parents: 33083
diff changeset
  1156
36937
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1157
$(OUT)/HOL-Multivariate_Analysis: $(OUT)/HOL				\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1158
  Multivariate_Analysis/Brouwer_Fixpoint.thy				\
47232
e2f0176149d0 dropped now obsolete Cset theories
haftmann
parents: 47223
diff changeset
  1159
  Multivariate_Analysis/Cartesian_Euclidean_Space.thy			\
36937
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1160
  Multivariate_Analysis/Convex_Euclidean_Space.thy			\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1161
  Multivariate_Analysis/Derivative.thy					\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1162
  Multivariate_Analysis/Determinants.thy				\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1163
  Multivariate_Analysis/Euclidean_Space.thy				\
41980
28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents: 41973
diff changeset
  1164
  Multivariate_Analysis/Extended_Real_Limits.thy			\
36937
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1165
  Multivariate_Analysis/Fashoda.thy					\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1166
  Multivariate_Analysis/Finite_Cartesian_Product.thy			\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1167
  Multivariate_Analysis/Integration.certs				\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1168
  Multivariate_Analysis/Integration.thy					\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1169
  Multivariate_Analysis/L2_Norm.thy					\
44288
fe9c2398c330 add Multivariate_Analysis dependencies
huffman
parents: 44276
diff changeset
  1170
  Multivariate_Analysis/Linear_Algebra.thy				\
36937
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1171
  Multivariate_Analysis/Multivariate_Analysis.thy			\
44516
d9a496ae5d9d move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents: 44374
diff changeset
  1172
  Multivariate_Analysis/Norm_Arith.thy					\
36937
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1173
  Multivariate_Analysis/Operator_Norm.thy				\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1174
  Multivariate_Analysis/Path_Connected.thy				\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1175
  Multivariate_Analysis/ROOT.ML						\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1176
  Multivariate_Analysis/Real_Integration.thy				\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1177
  Multivariate_Analysis/Topology_Euclidean_Space.thy			\
a30e50d4aeeb moved normarith.ML where it is actually used;
wenzelm
parents: 36936
diff changeset
  1178
  Multivariate_Analysis/document/root.tex				\
37742
d8e7f473c3a1 tuned tabs
haftmann
parents: 37691
diff changeset
  1179
  Multivariate_Analysis/normarith.ML Library/Glbs.thy			\
43920
cedb5cb948fd Rename extreal => ereal
hoelzl
parents: 43919
diff changeset
  1180
  Library/Extended_Real.thy Library/Indicator_Function.thy		\
41981
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41980
diff changeset
  1181
  Library/Inner_Product.thy Library/Numeral_Type.thy Library/Convex.thy	\
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents: 41980
diff changeset
  1182
  Library/FrechetDeriv.thy Library/Product_Vector.thy			\
44288
fe9c2398c330 add Multivariate_Analysis dependencies
huffman
parents: 44276
diff changeset
  1183
  Library/Product_plus.thy Library/Sum_of_Squares.thy
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents: 36895
diff changeset
  1184
	@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
  1185
33285
wenzelm
parents: 33272
diff changeset
  1186
33271
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents: 33270
diff changeset
  1187
## HOL-Probability
7be66dee1a5a New theory Probability, which contains a development of measure theory
paulson
parents: 33270
diff changeset
  1188
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38622
diff changeset
  1189
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
  1190
40863
ab83ba2cd5d1 Corrected IsaMakefile
hoelzl
parents: 40862
diff changeset
  1191
$(OUT)/HOL-Probability: $(OUT)/HOL-Multivariate_Analysis		\
42146
5b52c6a9c627 split Product_Measure into Binary_Product_Measure and Finite_Product_Measure
hoelzl
parents: 42138
diff changeset
  1192
  Probability/Binary_Product_Measure.thy Probability/Borel_Space.thy	\
5b52c6a9c627 split Product_Measure into Binary_Product_Measure and Finite_Product_Measure
hoelzl
parents: 42138
diff changeset
  1193
  Probability/Caratheodory.thy Probability/Complete_Measure.thy		\
43556
0d78c8d31d0d move conditional expectation to its own theory file
hoelzl
parents: 43524
diff changeset
  1194
  Probability/Conditional_Probability.thy				\
40860
a6df324752da More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
hoelzl
parents: 40839
diff changeset
  1195
  Probability/ex/Dining_Cryptographers.thy				\
a6df324752da More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
hoelzl
parents: 40839
diff changeset
  1196
  Probability/ex/Koepf_Duermuth_Countermeasure.thy			\
42147
61d5d50ca74c add infinite product measure
hoelzl
parents: 42146
diff changeset
  1197
  Probability/Finite_Product_Measure.thy				\
47232
e2f0176149d0 dropped now obsolete Cset theories
haftmann
parents: 47223
diff changeset
  1198
  Probability/Independent_Family.thy					\
42147
61d5d50ca74c add infinite product measure
hoelzl
parents: 42146
diff changeset
  1199
  Probability/Infinite_Product_Measure.thy Probability/Information.thy	\
42146
5b52c6a9c627 split Product_Measure into Binary_Product_Measure and Finite_Product_Measure
hoelzl
parents: 42138
diff changeset
  1200
  Probability/Lebesgue_Integration.thy Probability/Lebesgue_Measure.thy \
42148
d596e7bb251f rename Probability_Space to Probability_Measure
hoelzl
parents: 42147
diff changeset
  1201
  Probability/Measure.thy Probability/Probability_Measure.thy		\
42146
5b52c6a9c627 split Product_Measure into Binary_Product_Measure and Finite_Product_Measure
hoelzl
parents: 42138
diff changeset
  1202
  Probability/Probability.thy Probability/Radon_Nikodym.thy		\
40860
a6df324752da More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
hoelzl
parents: 40839
diff changeset
  1203
  Probability/ROOT.ML Probability/Sigma_Algebra.thy			\
42146
5b52c6a9c627 split Product_Measure into Binary_Product_Measure and Finite_Product_Measure
hoelzl
parents: 42138
diff changeset
  1204
  Library/Countable.thy Library/FuncSet.thy Library/Nat_Bijection.thy
38656
d5d342611edb Rewrite the Probability theory.
hoelzl
parents: 38622
diff changeset
  1205
	@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
  1206
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
  1207
19497
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
  1208
## HOL-Nominal
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
  1209
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
  1210
HOL-Nominal: HOL $(OUT)/HOL-Nominal
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
  1211
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents: 22167
diff changeset
  1212
$(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
  1213
  Nominal/Nominal.thy \
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents: 22167
diff changeset
  1214
  Nominal/nominal_atoms.ML \
31936
9466169dc8e0 nominal.ML is nominal_datatype.ML
haftmann
parents: 31849
diff changeset
  1215
  Nominal/nominal_datatype.ML \
22784
4637b69de71b Added datatype_case.ML and nominal_fresh_fun.ML.
berghofe
parents: 22657
diff changeset
  1216
  Nominal/nominal_fresh_fun.ML \
22247
5bad0d429694 corrected typo introduced by me
urbanc
parents: 22245
diff changeset
  1217
  Nominal/nominal_induct.ML \
22314
d541f13756a2 Added new file Nominal/nominal_inductive.ML
berghofe
parents: 22260
diff changeset
  1218
  Nominal/nominal_inductive.ML \
28652
659d64d59f16 Added nominal_inductive2.ML
berghofe
parents: 28637
diff changeset
  1219
  Nominal/nominal_inductive2.ML \
22245
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents: 22167
diff changeset
  1220
  Nominal/nominal_permeq.ML \
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents: 22167
diff changeset
  1221
  Nominal/nominal_primrec.ML \
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents: 22167
diff changeset
  1222
  Nominal/nominal_thmdecls.ML \
21542
4462ee172ef0 Added nominal_primrec.ML
berghofe
parents: 21425
diff changeset
  1223
  Library/Infinite_Set.thy
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
  1224
	@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
  1225
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
  1226
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
  1227
## HOL-Nominal-Examples
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
  1228
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
  1229
HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
  1230
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
  1231
$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal \
32636
55a0be42327c added session theory for Bali and Nominal_Examples
haftmann
parents: 32632
diff changeset
  1232
  Nominal/Examples/Nominal_Examples.thy \
27163
587ad1fba128 added CK_Machine to the nominal section
urbanc
parents: 27127
diff changeset
  1233
  Nominal/Examples/CK_Machine.thy \
22073
c170dcbe6c9d formalisation of Crary's chapter on logical relations
urbanc
parents: 22067
diff changeset
  1234
  Nominal/Examples/CR.thy \
22821
15b2e7ec1f3b alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents: 22819
diff changeset
  1235
  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
  1236
  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
  1237
  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
  1238
  Nominal/Examples/Class3.thy \
22073
c170dcbe6c9d formalisation of Crary's chapter on logical relations
urbanc
parents: 22067
diff changeset
  1239
  Nominal/Examples/Compile.thy \
25725
18bc59fb01b5 updated HOL-Nominal-Examples deps;
wenzelm
parents: 25600
diff changeset
  1240
  Nominal/Examples/Contexts.thy \
18bc59fb01b5 updated HOL-Nominal-Examples deps;
wenzelm
parents: 25600
diff changeset
  1241
  Nominal/Examples/Crary.thy \
22073
c170dcbe6c9d formalisation of Crary's chapter on logical relations
urbanc
parents: 22067
diff changeset
  1242
  Nominal/Examples/Fsub.thy \
25725
18bc59fb01b5 updated HOL-Nominal-Examples deps;
wenzelm
parents: 25600
diff changeset
  1243
  Nominal/Examples/Height.thy \
18bc59fb01b5 updated HOL-Nominal-Examples deps;
wenzelm
parents: 25600
diff changeset
  1244
  Nominal/Examples/Lam_Funs.thy \
22073
c170dcbe6c9d formalisation of Crary's chapter on logical relations
urbanc
parents: 22067
diff changeset
  1245
  Nominal/Examples/Lambda_mu.thy \
25725
18bc59fb01b5 updated HOL-Nominal-Examples deps;
wenzelm
parents: 25600
diff changeset
  1246
  Nominal/Examples/LocalWeakening.thy \
33189
82a40677c1f8 Added Pattern.thy to Nominal/Examples.
berghofe
parents: 33176
diff changeset
  1247
  Nominal/Examples/Pattern.thy \
25725
18bc59fb01b5 updated HOL-Nominal-Examples deps;
wenzelm
parents: 25600
diff changeset
  1248
  Nominal/Examples/ROOT.ML \
22073
c170dcbe6c9d formalisation of Crary's chapter on logical relations
urbanc
parents: 22067
diff changeset
  1249
  Nominal/Examples/SN.thy \
23144
4a9c9e260abf included new example in the compiling process
urbanc
parents: 23100
diff changeset
  1250
  Nominal/Examples/SOS.thy \
27624
a925aa66e17a Added Standardization theory to nominal examples.
berghofe
parents: 27484
diff changeset
  1251
  Nominal/Examples/Standardization.thy \
24896
70f238757695 added the two new examples from Nominal to the build process
urbanc
parents: 24830
diff changeset
  1252
  Nominal/Examples/Support.thy \
27032
6fd85edc403d new example
urbanc
parents: 26878
diff changeset
  1253
  Nominal/Examples/Type_Preservation.thy \
25725
18bc59fb01b5 updated HOL-Nominal-Examples deps;
wenzelm
parents: 25600
diff changeset
  1254
  Nominal/Examples/VC_Condition.thy \
26195
8292f8723e99 added new example
urbanc
parents: 26192
diff changeset
  1255
  Nominal/Examples/W.thy \
25725
18bc59fb01b5 updated HOL-Nominal-Examples deps;
wenzelm
parents: 25600
diff changeset
  1256
  Nominal/Examples/Weakening.thy
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
  1257
	@cd Nominal; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Nominal Examples
19497
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
  1258
630073ef9212 Added new targets for nominal datatype package.
berghofe
parents: 19404
diff changeset
  1259
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
  1260
## HOL-Word
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
  1261
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
  1262
HOL-Word: HOL $(OUT)/HOL-Word
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
  1263
33024
60a098883d81 more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents: 33010
diff changeset
  1264
$(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML Library/Boolean_Algebra.thy	\
37655
f4d616d41a59 more speaking theory names
haftmann
parents: 37583
diff changeset
  1265
  Library/Numeral_Type.thy Word/Misc_Numeric.thy Word/Misc_Typedef.thy	\
37659
14cabf5fa710 more speaking names
haftmann
parents: 37655
diff changeset
  1266
  Word/Type_Length.thy Word/Bit_Representation.thy Word/Bit_Int.thy	\
14cabf5fa710 more speaking names
haftmann
parents: 37655
diff changeset
  1267
  Word/Bool_List_Representation.thy Word/Bit_Operations.thy		\
37660
56e3520b68b2 one unified Word theory
haftmann
parents: 37659
diff changeset
  1268
  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
  1269
  Word/document/root.bib Word/Tools/smt_word.ML
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
  1270
	@cd Word; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Word
24333
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
  1271
e77ea0ea7f2c * HOL-Word:
kleing
parents: 24332
diff changeset
  1272
24442
39e29972cb96 HOL-Word-Examples
huffman
parents: 24411
diff changeset
  1273
## HOL-Word-Examples
39e29972cb96 HOL-Word-Examples
huffman
parents: 24411
diff changeset
  1274
39e29972cb96 HOL-Word-Examples
huffman
parents: 24411
diff changeset
  1275
HOL-Word-Examples: HOL-Word $(LOG)/HOL-Word-Examples.gz
39e29972cb96 HOL-Word-Examples
huffman
parents: 24411
diff changeset
  1276
27164
81632fd4ff61 some reformatting;
wenzelm
parents: 27163
diff changeset
  1277
$(LOG)/HOL-Word-Examples.gz: $(OUT)/HOL-Word Word/Examples/ROOT.ML	\
24442
39e29972cb96 HOL-Word-Examples
huffman
parents: 24411
diff changeset
  1278
  Word/Examples/WordExamples.thy
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 28477
diff changeset
  1279
	@cd Word; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Word Examples