author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47325  ec6187036495 
child 47474  214bfaae738d 
permissions  rwrr 
2448  1 
# 
2 
# IsaMakefile for HOL 

3 
# 

4 

4518  5 
## targets 
2448  6 

4518  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 HOLLibrary; introduced distinct session HOLCodegenerator_Test
haftmann
parents:
37672
diff
changeset

11 
HOLLibrary \ 
33210
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset

12 
HOLAlgebra \ 
33419  13 
HOLBoogie \ 
43917  14 
HOLIMP \ 
33210
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset

15 
HOLMultivariate_Analysis \ 
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset

16 
HOLNSA \ 
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset

17 
HOLNominal \ 
34205
f69cd974bc4e
explicit session HOLProofs  avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset

18 
HOLProofs \ 
41566  19 
HOLSPARK \ 
33210
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset

20 
HOLWord \ 
40774  21 
HOLCF \ 
22 
IOA \ 

37691
4915de09b4d3
build image for session HOLLibrary; introduced distinct session HOLCodegenerator_Test
haftmann
parents:
37672
diff
changeset

23 
TLA \ 
4915de09b4d3
build image for session HOLLibrary; introduced distinct session HOLCodegenerator_Test
haftmann
parents:
37672
diff
changeset

24 
HOLBase \ 
4915de09b4d3
build image for session HOLLibrary; introduced distinct session HOLCodegenerator_Test
haftmann
parents:
37672
diff
changeset

25 
HOLMain \ 
4915de09b4d3
build image for session HOLLibrary; introduced distinct session HOLCodegenerator_Test
haftmann
parents:
37672
diff
changeset

26 
HOLPlain 
10135  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 
HOLAuth \ 
14031  31 
HOLBali \ 
33439  32 
HOLBoogieExamples \ 
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset

33 
HOLHahn_Banach \ 
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset

34 
HOLHoare \ 
32621
a073cb249a06
theory entry point for session Hoare_Parallel (now also with proper underscore)
haftmann
parents:
32618
diff
changeset

35 
HOLHoare_Parallel \ 
40774  36 
HOLCFFOCUS \ 
37 
HOLCFIMP \ 

38 
HOLCFLibrary \ 

39 
HOLCFTutorial \ 

40 
HOLCFex \ 

10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset

41 
HOLIMPP \ 
47264
6488c5efec49
renamed import session back to Import, conforming to directory name; NEWS
krauss
parents:
47260
diff
changeset

42 
HOLImport \ 
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset

43 
HOLIOA \ 
40774  44 
IOAABP \ 
45 
IOANTP \ 

46 
IOAStorage \ 

47 
IOAex \ 

29399
ebcd69a00872
split of Imperative_HOL theories from HOLLibrary
haftmann
parents:
29197
diff
changeset

48 
HOLImperative_HOL \ 
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset

49 
HOLInduct \ 
33026  50 
HOLIsar_Examples \ 
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset

51 
HOLLattice \ 
37747  52 
HOLLibraryCodegenerator_Test \ 
46988
9f492f5b0cec
renamed HOLMatrix to HOLMatrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset

53 
HOLMatrix_LP \ 
33027  54 
HOLMetis_Examples \ 
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset

55 
HOLMicroJava \ 
32496  56 
HOLMirabelle \ 
35536  57 
HOLMutabelle \ 
11376  58 
HOLNanoJava \ 
33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

59 
HOLNitpick_Examples \ 
32479  60 
HOLNumber_Theory \ 
61 
HOLOld_Number_Theory \ 

35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset

62 
HOLQuotient_Examples \ 
35950
791ce568d40a
moved examples for the predicate compiler into its own session Predicate_Compile_Examples to slenderise the HOLex session
bulwahn
parents:
35931
diff
changeset

63 
HOLPredicate_Compile_Examples \ 
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset

64 
HOLProlog \ 
39157
b98909faaea8
more explicit HOLProofs 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 
HOLProofsex \ 
47128
d0d16b20b6ce
revert changeset 500a5d97511a, reenabling HOLProofsLambda
huffman
parents:
47120
diff
changeset

66 
HOLProofsLambda \ 
33028  67 
HOLSET_Protocol \ 
41569  68 
HOLSPARKExamples \ 
45044  69 
HOLSPARKManual \ 
36933
705b58fde476
more precise dependencies for HOLWordSMT_Examples;
wenzelm
parents:
36916
diff
changeset

70 
HOLWordSMT_Examples \ 
25171  71 
HOLStatespace \ 
33210
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset

72 
TLABuffer \ 
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset

73 
TLAInc \ 
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset

74 
TLAMemory \ 
43804
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
43800
diff
changeset

75 
HOLTPTP \ 
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset

76 
HOLUNITY \ 
10966  77 
HOLUnix \ 
24442  78 
HOLWordExamples \ 
24325  79 
HOLZF 
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset

80 
# ^ this is the sort position 
10614  81 

45860  82 
benchmark: \ 
83 
HOLDatatype_Benchmark \ 

84 
HOLRecord_Benchmark 

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 
imagesnosmlnj: \ 
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 
HOLProbability 
4518  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 
testnosmlnj: \ 
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 
HOLex \ 
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 
HOLDecision_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 
HOLProofsExtraction \ 
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 
HOLNominalExamples 
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: testnosmlnj test imagesnosmlnj 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 HOLQuickcheck_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  98 

45860  99 

4518  100 
## global settings 
101 

102 
SRC = $(ISABELLE_HOME)/src 

3118  103 
OUT = $(ISABELLE_OUTPUT) 
4447  104 
LOG = $(OUT)/log 
2448  105 

4518  106 

107 
## HOL 

2448  108 

28393  109 
HOL: Pure $(OUT)/HOL 
27368  110 

29505  111 
HOLBase: Pure $(OUT)/HOLBase 
112 

27368  113 
HOLPlain: Pure $(OUT)/HOLPlain 
4518  114 

28401  115 
HOLMain: Pure $(OUT)/HOLMain 
116 

4518  117 
Pure: 
28500  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  120 
$(OUT)/Pure: Pure 
121 

36073  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  129 
$(SRC)/Tools/Code/code_haskell.ML \ 
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  132 
$(SRC)/Tools/Code/code_preproc.ML \ 
133 
$(SRC)/Tools/Code/code_printer.ML \ 

39402  134 
$(SRC)/Tools/Code/code_runtime.ML \ 
34945  135 
$(SRC)/Tools/Code/code_scala.ML \ 
37442  136 
$(SRC)/Tools/Code/code_simp.ML \ 
31771  137 
$(SRC)/Tools/Code/code_target.ML \ 
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  145 
$(SRC)/Tools/cache_io.ML \ 
41827  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  159 
$(SRC)/Tools/subtyping.ML \ 
43018  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  162 
HOL.thy \ 
163 
Tools/hologic.ML \ 

36073  164 
Tools/simpdata.ML 
29505  165 

166 
$(OUT)/HOLBase: base.ML $(BASE_DEPENDENCIES) 

29523  167 
@$(ISABELLE_TOOL) usedir b f base.ML d false g false $(OUT)/Pure HOLBase 
29505  168 

39157
b98909faaea8
more explicit HOLProofs 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 HOLPlain, 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  179 
Complete_Partial_Order.thy \ 
27368  180 
Datatype.thy \ 
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  183 
Finite_Set.thy \ 
184 
Fun.thy \ 

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  187 
Inductive.thy \ 
188 
Lattices.thy \ 

39945  189 
Meson.thy \ 
39946  190 
Metis.thy \ 
27368  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  194 
Orderings.thy \ 
40108  195 
Partial_Function.thy \ 
27368  196 
Plain.thy \ 
197 
Power.thy \ 

198 
Product_Type.thy \ 

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  201 
SAT.thy \ 
202 
Set.thy \ 

203 
Sum_Type.thy \ 

43691
c00febb8e39c
moved ATP dependencies to HOLPlain, where they belong
blanchet
parents:
43614
diff
changeset

204 
Tools/ATP/atp_problem.ML \ 
46320  205 
Tools/ATP/atp_problem_generate.ML \ 
43691
c00febb8e39c
moved ATP dependencies to HOLPlain, where they belong
blanchet
parents:
43614
diff
changeset

206 
Tools/ATP/atp_proof.ML \ 
46320  207 
Tools/ATP/atp_proof_reconstruct.ML \ 
208 
Tools/ATP/atp_proof_redirect.ML \ 

43691
c00febb8e39c
moved ATP dependencies to HOLPlain, where they belong
blanchet
parents:
43614
diff
changeset

209 
Tools/ATP/atp_systems.ML \ 
c00febb8e39c
moved ATP dependencies to HOLPlain, 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  212 
Tools/Datatype/datatype_aux.ML \ 
213 
Tools/Datatype/datatype_case.ML \ 

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  216 
Tools/Datatype/datatype_prop.ML \ 
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  219 
Tools/Datatype/rep_datatype.ML \ 
31771  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  226 
Tools/Function/induction_schema.ML \ 
31771  227 
Tools/Function/lexicographic_order.ML \ 
228 
Tools/Function/measure_functions.ML \ 

229 
Tools/Function/mutual.ML \ 

40108  230 
Tools/Function/partial_function.ML \ 
33083  231 
Tools/Function/pat_completeness.ML \ 
31771  232 
Tools/Function/pattern_split.ML \ 
33100  233 
Tools/Function/relation.ML \ 
31771  234 
Tools/Function/scnp_reconstruct.ML \ 
235 
Tools/Function/scnp_solve.ML \ 

236 
Tools/Function/size.ML \ 

237 
Tools/Function/sum_tree.ML \ 

238 
Tools/Function/termination.ML \ 

39940  239 
Tools/Meson/meson.ML \ 
240 
Tools/Meson/meson_clausify.ML \ 

39948  241 
Tools/Meson/meson_tactic.ML \ 
46320  242 
Tools/Metis/metis_generate.ML \ 
39946  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  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 lambdalifting 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 lambdalifting 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  257 
Tools/prop_logic.ML \ 
258 
Tools/refute.ML \ 

259 
Tools/rewrite_hol_proof.ML \ 

260 
Tools/sat_funcs.ML \ 

261 
Tools/sat_solver.ML \ 

262 
Tools/split_rule.ML \ 

46641  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  265 
Transitive_Closure.thy \ 
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 HOLPlain vs. Plain
haftmann
parents:
28243
diff
changeset

268 

f0838044f034
different session branches for HOLPlain vs. Plain
haftmann
parents:
28243
diff
changeset

269 
$(OUT)/HOLPlain: plain.ML $(PLAIN_DEPENDENCIES) 
28500  270 
@$(ISABELLE_TOOL) usedir b f plain.ML g true $(OUT)/Pure HOLPlain 
27368  271 

28401  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  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  278 
Equiv_Relations.thy \ 
40650
d40b347d5b0b
adding Enum to HOLMain image and removing it from HOLLibrary
bulwahn
parents:
40634
diff
changeset

279 
Enum.thy \ 
27368  280 
Groebner_Basis.thy \ 
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  284 
Lifting.thy \ 
27421  285 
List.thy \ 
286 
Main.thy \ 

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  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 HOLMain; 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  297 
Quickcheck_Exhaustive.thy \ 
43310  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  302 
Record.thy \ 
36916  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 oldstyle theory name with proper newstyle 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  307 
SMT.thy \ 
31048
ac146fc38b51
refined HOL string theories and corresponding ML fragments
haftmann
parents:
31036
diff
changeset

308 
String.thy \ 
47325  309 
Transfer.thy \ 
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31186
diff
changeset

310 
Typerep.thy \ 
27421  311 
$(SRC)/Provers/Arith/assoc_fold.ML \ 
312 
$(SRC)/Provers/Arith/cancel_numeral_factor.ML \ 

313 
$(SRC)/Provers/Arith/cancel_numerals.ML \ 

314 
$(SRC)/Provers/Arith/combine_numerals.ML \ 

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  317 
Tools/code_evaluation.ML \ 
41919  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  321 
Tools/Lifting/lifting_def.ML \ 
322 
Tools/Lifting/lifting_info.ML \ 

323 
Tools/Lifting/lifting_term.ML \ 

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  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 HOLMain; 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 HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33210
diff
changeset

349 
Tools/Predicate_Compile/predicate_compile_core.ML \ 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33210
diff
changeset

350 
Tools/Predicate_Compile/predicate_compile_data.ML \ 
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33210
diff
changeset

351 
Tools/Predicate_Compile/predicate_compile_fun.ML \ 
5c2af18a3237
including the predicate compiler in HOLMain; 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 HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33210
diff
changeset

355 
Tools/Predicate_Compile/predicate_compile_pred.ML \ 
27421  356 
Tools/Qelim/cooper.ML \ 
36803  357 
Tools/Qelim/cooper_procedure.ML \ 
27421  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  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  362 
Tools/Quickcheck/narrowing_generators.ML \ 
363 
Tools/Quickcheck/Narrowing_Engine.hs \ 

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  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  373 
Tools/Sledgehammer/sledgehammer_filter.ML \ 
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  378 
Tools/Sledgehammer/sledgehammer_util.ML \ 
36898  379 
Tools/SMT/smtlib_interface.ML \ 
40277  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
reimplemented 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  384 
Tools/SMT/smt_normalize.ML \ 
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3specific 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  386 
Tools/SMT/smt_solver.ML \ 
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  389 
Tools/SMT/z3_interface.ML \ 
390 
Tools/SMT/z3_model.ML \ 

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  393 
Tools/SMT/z3_proof_parser.ML \ 
394 
Tools/SMT/z3_proof_reconstruction.ML \ 

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  397 
Tools/string_syntax.ML \ 
47325  398 
Tools/transfer.ML \ 
28401  399 

400 
$(OUT)/HOLMain: main.ML $(MAIN_DEPENDENCIES) 

28500  401 
@$(ISABELLE_TOOL) usedir b f main.ML g true $(OUT)/Pure HOLMain 
28401  402 

34205
f69cd974bc4e
explicit session HOLProofs  avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset

403 
HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \ 
30096  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  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  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  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  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 HOLProofs  avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset

430 

f69cd974bc4e
explicit session HOLProofs  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 HOLProofs  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 HOLProofs  avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset

433 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
7513
diff
changeset

434 

10255  435 
## HOLLibrary 
436 

37691
4915de09b4d3
build image for session HOLLibrary; introduced distinct session HOLCodegenerator_Test
haftmann
parents:
37672
diff
changeset

437 
HOLLibrary: HOL $(OUT)/HOLLibrary 
10255  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)/HOLLibrary: $(OUT)/HOL Library/ROOT.ML \ 
37691
4915de09b4d3
build image for session HOLLibrary; introduced distinct session HOLCodegenerator_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 adhocoverloading 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  444 
Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy \ 
37662  445 
Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy \ 
43919  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  449 
Library/Code_Real_Approx_By_Float.thy \ 
43919  450 
Tools/Predicate_Compile/code_prolog.ML Library/ContNotDenum.thy \ 
47232  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  453 
Library/Dlist.thy Library/Eval_Witness.thy \ 
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 HOLUnix (a bit too specific for HOLLibrary);
wenzelm
parents:
44145
diff
changeset

456 
Library/Extended_Real.thy Library/Extended_Nat.thy Library/Float.thy \ 
43919  457 
Library/Formal_Power_Series.thy Library/Fraction_Field.thy \ 
47232  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  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 HOLUnix (a bit too specific for HOLLibrary);
wenzelm
parents:
44145
diff
changeset

466 
Library/Multiset.thy Library/Nat_Bijection.thy \ 
b73b7832b384
moved theory Nested_Environment to HOLUnix (a bit too specific for HOLLibrary);
wenzelm
parents:
44145
diff
changeset

467 
Library/Numeral_Type.thy Library/Old_Recdef.thy \ 
b73b7832b384
moved theory Nested_Environment to HOLUnix (a bit too specific for HOLLibrary);
wenzelm
parents:
44145
diff
changeset

468 
Library/OptionalSugar.thy Library/Order_Relation.thy \ 
b73b7832b384
moved theory Nested_Environment to HOLUnix (a bit too specific for HOLLibrary);
wenzelm
parents:
44145
diff
changeset

469 
Library/Permutation.thy Library/Permutations.thy \ 
b73b7832b384
moved theory Nested_Environment to HOLUnix (a bit too specific for HOLLibrary);
wenzelm
parents:
44145
diff
changeset

470 
Library/Poly_Deriv.thy Library/Polynomial.thy \ 
b73b7832b384
moved theory Nested_Environment to HOLUnix (a bit too specific for HOLLibrary);
wenzelm
parents:
44145
diff
changeset

471 
Library/Predicate_Compile_Quickcheck.thy Library/Preorder.thy \ 
b73b7832b384
moved theory Nested_Environment to HOLUnix (a bit too specific for HOLLibrary);
wenzelm
parents:
44145
diff
changeset

472 
Library/Product_Vector.thy Library/Product_ord.thy \ 
b73b7832b384
moved theory Nested_Environment to HOLUnix (a bit too specific for HOLLibrary);
wenzelm
parents:
44145
diff
changeset

473 
Library/Product_plus.thy Library/Product_Lattice.thy \ 
b73b7832b384
moved theory Nested_Environment to HOLUnix (a bit too specific for HOLLibrary);
wenzelm
parents:
44145
diff
changeset

474 
Library/Quickcheck_Types.thy Library/Quotient_List.thy \ 
b73b7832b384
moved theory Nested_Environment to HOLUnix (a bit too specific for HOLLibrary);
wenzelm
parents:
44145
diff
changeset

475 
Library/Quotient_Option.thy Library/Quotient_Product.thy \ 
45074  476 
Library/Quotient_Set.thy Library/Quotient_Sum.thy \ 
477 
Library/Quotient_Syntax.thy Library/Quotient_Type.thy Library/RBT.thy \ 

478 
Library/RBT_Impl.thy Library/RBT_Mapping.thy Library/README.html \ 

479 
Library/Saturated.thy Library/Set_Algebras.thy \ 

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 wellknown 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 adhocoverloading to generic tools
haftmann
parents:
37790
diff
changeset

486 
$(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML \ 
37789  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 HOLLibrary 
10255  494 

495 

31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset

496 
## HOLHahn_Banach 
27421  497 

31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset

498 
HOLHahn_Banach: HOL $(LOG)/HOLHahn_Banach.gz 
27421  499 

31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset

500 
$(LOG)/HOLHahn_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  509 

510 

4518  511 
## HOLInduct 
2473  512 

4518  513 
HOLInduct: HOL $(LOG)/HOLInduct.gz 
3125  514 

33688
1a97dcd8dc6a
moved old SList, LList, LFilter to AFP/LazyListsII;
wenzelm
parents:
33649
diff
changeset

515 
$(LOG)/HOLInduct.gz: $(OUT)/HOL Induct/Com.thy Induct/Comb.thy \ 
1a97dcd8dc6a
moved old SList, LList, LFilter to AFP/LazyListsII;
wenzelm
parents:
33649
diff
changeset

516 
Induct/Ordinals.thy Induct/PropLog.thy Induct/QuoNestedDataType.thy \ 
1a97dcd8dc6a
moved old SList, LList, LFilter to AFP/LazyListsII;
wenzelm
parents:
33649
diff
changeset

517 
Induct/QuoDataType.thy Induct/ROOT.ML Induct/Sexp.thy \ 
35249  518 
Induct/Sigma_Algebra.thy Induct/ABexp.thy Induct/SList.thy \ 
519 
Induct/Term.thy Induct/Tree.thy Induct/document/root.tex 

28500  520 
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Induct 
3125  521 

522 

4518  523 
## HOLIMP 
524 

43917  525 
HOLIMP: HOL $(OUT)/HOLIMP 
2448  526 

45112  527 
$(OUT)/HOLIMP: $(OUT)/HOL \ 
45747  528 
IMP/ACom.thy IMP/Abs_Int0_fun.thy IMP/Abs_State.thy IMP/Abs_Int0.thy \ 
45112  529 
IMP/Abs_Int0_const.thy IMP/Abs_Int1.thy IMP/Abs_Int1_ivl.thy \ 
530 
IMP/Abs_Int2.thy IMP/Abs_Int_Den/Abs_Int_den0_fun.thy \ 

45111  531 
IMP/Abs_Int_Den/Abs_State_den.thy IMP/Abs_Int_Den/Abs_Int_den0.thy \ 
532 
IMP/Abs_Int_Den/Abs_Int_den0_const.thy IMP/Abs_Int_Den/Abs_Int_den1.thy \ 

533 
IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy IMP/Abs_Int_Den/Abs_Int_den2.thy \ 

45885  534 
IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy IMP/Big_Step.thy IMP/C_like.thy \ 
46232  535 
IMP/Collecting.thy IMP/Collecting_list.thy IMP/Collecting1.thy IMP/Com.thy \ 
536 
IMP/Compiler.thy IMP/Comp_Rev.thy \ 

537 
IMP/Def_Ass.thy IMP/Def_Ass_Big.thy IMP/Def_Ass_Exp.thy \ 

43158  538 
IMP/Def_Ass_Small.thy IMP/Def_Ass_Sound_Big.thy \ 
539 
IMP/Def_Ass_Sound_Small.thy IMP/Denotation.thy IMP/Hoare.thy \ 

540 
IMP/HoareT.thy IMP/Hoare_Examples.thy IMP/Hoare_Sound_Complete.thy \ 

45812  541 
IMP/Live.thy IMP/Live_True.thy IMP/OO.thy IMP/Poly_Types.thy IMP/Procs.thy \ 
43158  542 
IMP/Procs_Dyn_Vars_Dyn.thy IMP/Procs_Stat_Vars_Dyn.thy \ 
543 
IMP/Procs_Stat_Vars_Stat.thy IMP/Sec_Type_Expr.thy IMP/Sec_Typing.thy \ 

544 
IMP/Sec_TypingT.thy IMP/Small_Step.thy IMP/Star.thy IMP/Types.thy \ 

45716  545 
IMP/VC.thy IMP/Vars.thy \ 
27164  546 
IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib 
45320
9d7b52c8eb01
moved latex generation for HOLIMP out of distribution
kleing
parents:
45319
diff
changeset

547 
@cd IMP && $(ISABELLE_TOOL) usedir g true b $(OUT)/HOL HOLIMP 
2448  548 

8179  549 
## HOLIMPP 
550 

551 
HOLIMPP: HOL $(LOG)/HOLIMPP.gz 

552 

27164  553 
$(LOG)/HOLIMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy \ 
19803  554 
IMPP/Natural.thy IMPP/Hoare.thy IMPP/Misc.thy IMPP/EvenOdd.thy 
28500  555 
@$(ISABELLE_TOOL) usedir $(OUT)/HOL IMPP 
8179  556 

557 

47267
4c7548e7df86
merged, manually resolving conflicts due to session renaming (cf. 6488c5efec49)
krauss
diff
changeset

558 
## HOLImport 
46785  559 

47264
6488c5efec49
renamed import session back to Import, conforming to directory name; NEWS
krauss
parents:
47260
diff
changeset

560 
HOLImport: $(LOG)/HOLImport.gz 
14516  561 

47264
6488c5efec49
renamed import session back to Import, conforming to directory name; NEWS
krauss
parents:
47260
diff
changeset

562 
$(LOG)/HOLImport.gz: $(OUT)/HOL \ 
47258
880e587eee9f
Modernized HOLImport for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
47232
diff
changeset

563 
Import/ROOT.ML \ 
880e587eee9f
Modernized HOLImport for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
47232
diff
changeset

564 
Import/Import_Setup.thy \ 
880e587eee9f
Modernized HOLImport for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
47232
diff
changeset

565 
Import/import_data.ML \ 
880e587eee9f
Modernized HOLImport for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
47232
diff
changeset

566 
Import/import_rule.ML \ 
880e587eee9f
Modernized HOLImport for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
47232
diff
changeset

567 
Import/HOL_Light_Maps.thy \ 
880e587eee9f
Modernized HOLImport 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  570 

47263  571 

32479  572 
## HOLNumber_Theory 
31719  573 

32479  574 
HOLNumber_Theory: HOL $(LOG)/HOLNumber_Theory.gz 
31719  575 

32479  576 
$(LOG)/HOLNumber_Theory.gz: $(OUT)/HOL $(ALGEBRA_DEPENDENCIES) \ 
31771  577 
Library/Multiset.thy \ 
32479  578 
Number_Theory/Binomial.thy \ 
579 
Number_Theory/Cong.thy \ 

580 
Number_Theory/Fib.thy \ 

581 
Number_Theory/MiscAlgebra.thy \ 

582 
Number_Theory/Number_Theory.thy \ 

583 
Number_Theory/Residues.thy \ 

584 
Number_Theory/UniqueFactorization.thy \ 

585 
Number_Theory/ROOT.ML 

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  588 

32479  589 
## HOLOld_Number_Theory 
9510  590 

32479  591 
HOLOld_Number_Theory: HOL $(LOG)/HOLOld_Number_Theory.gz 
9510  592 

37021  593 
$(LOG)/HOLOld_Number_Theory.gz: $(OUT)/HOL Library/Permutation.thy \ 
594 
Old_Number_Theory/Primes.thy Old_Number_Theory/Fib.thy \ 

595 
Old_Number_Theory/Factorization.thy Old_Number_Theory/BijectionRel.thy\ 

596 
Old_Number_Theory/Chinese.thy Old_Number_Theory/EulerFermat.thy \ 

597 
Old_Number_Theory/IntFact.thy Old_Number_Theory/IntPrimes.thy \ 

598 
Old_Number_Theory/WilsonBij.thy Old_Number_Theory/WilsonRuss.thy \ 

599 
Old_Number_Theory/Finite2.thy Old_Number_Theory/Int2.thy \ 

600 
Old_Number_Theory/EvenOdd.thy Old_Number_Theory/Residues.thy \ 

601 
Old_Number_Theory/Euler.thy Old_Number_Theory/Gauss.thy \ 

32479  602 
Old_Number_Theory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy \ 
37021  603 
Old_Number_Theory/Legacy_GCD.thy Old_Number_Theory/Pocklington.thy \ 
604 
Old_Number_Theory/ROOT.ML 

32479  605 
@$(ISABELLE_TOOL) usedir g true $(OUT)/HOL Old_Number_Theory 
9510  606 

607 

4518  608 
## HOLHoare 
609 

610 
HOLHoare: HOL $(LOG)/HOLHoare.gz 

2448  611 

27164  612 
$(LOG)/HOLHoare.gz: $(OUT)/HOL Hoare/Arith2.thy Hoare/Examples.thy \ 
42153  613 
Hoare/Hoare.thy Hoare/hoare_syntax.ML Hoare/hoare_tac.ML \ 
614 
Hoare/Heap.thy Hoare/Hoare_Logic.thy Hoare/Hoare_Logic_Abort.thy \ 

27164  615 
Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy Hoare/ROOT.ML \ 
616 
Hoare/ExamplesAbort.thy Hoare/HeapSyntaxAbort.thy \ 

42153  617 
Hoare/SchorrWaite.thy Hoare/Separation.thy Hoare/SepLogHeap.thy \ 
618 
Hoare/document/root.tex Hoare/document/root.bib 

28500  619 
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Hoare 
2448  620 

621 

32621
a073cb249a06
theory entry point for session Hoare_Parallel (now also with proper underscore)
haftmann
parents:
32618
diff
changeset

622 
## HOLHoare_Parallel 
12996  623 

32621
a073cb249a06
theory entry point for session Hoare_Parallel (now also with proper underscore)
haftmann
parents:
32618
diff
changeset

624 
HOLHoare_Parallel: HOL $(LOG)/HOLHoare_Parallel.gz 
12996  625 

32621
a073cb249a06
theory entry point for session Hoare_Parallel (now also with proper underscore)
haftmann
parents:
32618
diff
changeset

626 
$(LOG)/HOLHoare_Parallel.gz: $(OUT)/HOL Hoare_Parallel/Gar_Coll.thy \ 
33439  627 
Hoare_Parallel/Graph.thy Hoare_Parallel/Hoare_Parallel.thy \ 
628 
Hoare_Parallel/Mul_Gar_Coll.thy Hoare_Parallel/OG_Com.thy \ 

629 
Hoare_Parallel/OG_Examples.thy Hoare_Parallel/OG_Hoare.thy \ 

630 
Hoare_Parallel/OG_Syntax.thy Hoare_Parallel/OG_Tactics.thy \ 

631 
Hoare_Parallel/OG_Tran.thy Hoare_Parallel/Quote_Antiquote.thy \ 

632 
Hoare_Parallel/RG_Com.thy Hoare_Parallel/RG_Examples.thy \ 

633 
Hoare_Parallel/RG_Hoare.thy Hoare_Parallel/RG_Syntax.thy \ 

634 
Hoare_Parallel/RG_Tran.thy Hoare_Parallel/ROOT.ML \ 

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  637 

638 

37747  639 
## HOLLibraryCodegenerator_Test 
37691
4915de09b4d3
build image for session HOLLibrary; introduced distinct session HOLCodegenerator_Test
haftmann
parents:
37672
diff
changeset

640 

37747  641 
HOLLibraryCodegenerator_Test: HOLLibrary $(LOG)/HOLLibraryCodegenerator_Test.gz 
37691
4915de09b4d3
build image for session HOLLibrary; introduced distinct session HOLCodegenerator_Test
haftmann
parents:
37672
diff
changeset

642 

47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
46988
diff
changeset

643 
$(LOG)/HOLLibraryCodegenerator_Test.gz: $(OUT)/HOLLibrary \ 
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 HOLLibrary; introduced distinct session HOLCodegenerator_Test
haftmann
parents:
37672
diff
changeset

648 
Codegenerator_Test/Generate_Pretty.thy 
4915de09b4d3
build image for session HOLLibrary; introduced distinct session HOLCodegenerator_Test
haftmann
parents:
37672
diff
changeset

649 
@$(ISABELLE_TOOL) usedir d false g false i false $(OUT)/HOLLibrary Codegenerator_Test 
4915de09b4d3
build image for session HOLLibrary; introduced distinct session HOLCodegenerator_Test
haftmann
parents:
37672
diff
changeset

650 

4915de09b4d3
build image for session HOLLibrary; introduced distinct session HOLCodegenerator_Test
haftmann
parents:
37672
diff
changeset

651 

33027  652 
## HOLMetis_Examples 
23449  653 

33027  654 
HOLMetis_Examples: HOL $(LOG)/HOLMetis_Examples.gz 
23449  655 

41144  656 
$(LOG)/HOLMetis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML \ 
43197  657 
Metis_Examples/Abstraction.thy Metis_Examples/Big_O.thy \ 
658 
Metis_Examples/Binary_Tree.thy Metis_Examples/Clausification.thy \ 

659 
Metis_Examples/Message.thy Metis_Examples/Proxies.thy \ 

660 
Metis_Examples/Sets.thy Metis_Examples/Tarski.thy \ 

661 
Metis_Examples/Trans_Closure.thy Metis_Examples/Type_Encodings.thy 

33027  662 
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples 
23449  663 

664 

33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

665 
## HOLNitpick_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 
HOLNitpick_Examples: HOL $(LOG)/HOLNitpick_Examples.gz 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

668 

34126  669 
$(LOG)/HOLNitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \ 
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  673 
Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy \ 
674 
Nitpick_Examples/Nitpick_Examples.thy Nitpick_Examples/Pattern_Nits.thy \ 

675 
Nitpick_Examples/Record_Nits.thy Nitpick_Examples/Refute_Nits.thy \ 

676 
Nitpick_Examples/Special_Nits.thy Nitpick_Examples/Tests_Nits.thy \ 

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 
## HOLAlgebra 
7acf6eb8eec1
Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
7985
diff
changeset

682 

33439  683 
HOLAlgebra: HOL $(OUT)/HOLAlgebra 
7999
7acf6eb8eec1
Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
7985
diff
changeset

684 

31771  685 
ALGEBRA_DEPENDENCIES = $(OUT)/HOL \ 
686 
Algebra/ROOT.ML \ 

687 
Library/Binomial.thy \ 

688 
Library/FuncSet.thy \ 

689 
Library/Multiset.thy \ 

690 
Library/Permutation.thy \ 

32479  691 
Number_Theory/Primes.thy \ 
31771  692 
Algebra/AbelCoset.thy \ 
693 
Algebra/Bij.thy \ 

694 
Algebra/Congruence.thy \ 

695 
Algebra/Coset.thy \ 

696 
Algebra/Divisibility.thy \ 

697 
Algebra/Exponent.thy \ 

698 
Algebra/FiniteProduct.thy \ 

699 
Algebra/Group.thy \ 

700 
Algebra/Ideal.thy \ 

701 
Algebra/IntRing.thy \ 

702 
Algebra/Lattice.thy \ 

703 
Algebra/Module.thy \ 

704 
Algebra/QuotRing.thy \ 

705 
Algebra/Ring.thy \ 

706 
Algebra/RingHom.thy \ 

707 
Algebra/Sylow.thy \ 

708 
Algebra/UnivPoly.thy \ 

709 
Algebra/abstract/Abstract.thy \ 

710 
Algebra/abstract/Factor.thy \ 

711 
Algebra/abstract/Field.thy \ 

712 
Algebra/abstract/Ideal2.thy \ 

713 
Algebra/abstract/PID.thy \ 

714 
Algebra/abstract/Ring2.thy \ 

715 
Algebra/abstract/RingHomo.thy \ 

716 
Algebra/document/root.tex \ 

717 
Algebra/document/root.tex \ 

718 
Algebra/poly/LongDiv.thy \ 

719 
Algebra/poly/PolyHomo.thy \ 

720 
Algebra/poly/Polynomial.thy \ 

721 
Algebra/poly/UnivPoly2.thy \ 

722 
Algebra/ringsimp.ML 

723 

33448  724 
$(OUT)/HOLAlgebra: $(ALGEBRA_DEPENDENCIES) 
28500  725 
@cd Algebra; $(ISABELLE_TOOL) usedir b g true V outline=/proof,/ML $(OUT)/HOL HOLAlgebra 
7999
7acf6eb8eec1
Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
7985
diff
changeset

726 

27477
c64736fe2a1f
more precise dependencies for HOLWord and HOLNSA;
wenzelm
parents:
27470
diff
changeset

727 

4518  728 
## HOLAuth 
3819  729 

4518  730 
HOLAuth: HOL $(LOG)/HOLAuth.gz 
3819  731 

28098  732 
$(LOG)/HOLAuth.gz: $(OUT)/HOL \ 
37021  733 
Auth/Auth_Shared.thy Auth/Auth_Public.thy Auth/All_Symmetric.thy \ 
734 
Auth/Guard/Auth_Guard_Shared.thy \ 

735 
Auth/Guard/Auth_Guard_Public.thy \ 

32632  736 
Auth/Smartcard/Auth_Smartcard.thy Auth/All_Symmetric.thy \ 
27164  737 
Auth/CertifiedEmail.thy Auth/Event.thy Auth/Message.thy \ 
738 
Auth/NS_Public.thy Auth/NS_Public_Bad.thy Auth/NS_Shared.thy \ 

739 
Auth/OtwayRees.thy Auth/OtwayReesBella.thy Auth/OtwayRees_AN.thy \ 

740 
Auth/OtwayRees_Bad.thy Auth/Public.thy Auth/ROOT.ML Auth/Recur.thy \ 

741 
Auth/Shared.thy Auth/TLS.thy Auth/WooLam.thy Auth/Kerberos_BAN.thy \ 

742 
Auth/Kerberos_BAN_Gets.thy Auth/KerberosIV.thy \ 

743 
Auth/KerberosIV_Gets.thy Auth/KerberosV.thy Auth/Yahalom.thy \ 

744 
Auth/Yahalom2.thy Auth/Yahalom_Bad.thy Auth/ZhouGollmann.thy \ 

745 
Auth/Guard/Analz.thy Auth/Guard/Extensions.thy Auth/Guard/GuardK.thy \ 

746 
Auth/Guard/Guard_Public.thy Auth/Guard/Guard_Shared.thy \ 

747 
Auth/Guard/Guard.thy Auth/Guard/List_Msg.thy \ 

748 
Auth/Guard/Guard_NS_Public.thy Auth/Guard/Guard_OtwayRees.thy \ 

749 
Auth/Guard/P1.thy Auth/Guard/P2.thy Auth/Guard/Proto.thy \ 

750 
Auth/Guard/Guard_Yahalom.thy Auth/Smartcard/EventSC.thy \ 

751 
Auth/Smartcard/ShoupRubinBella.thy Auth/Smartcard/ShoupRubin.thy \ 

752 
Auth/Smartcard/Smartcard.thy Auth/document/root.tex 

28500  753 
@$(ISABELLE_TOOL) usedir g true $(OUT)/HOL Auth 
2448  754 

755 

4777  756 
## HOLUNITY 
757 

758 
HOLUNITY: HOL $(LOG)/HOLUNITY.gz 

759 

27164  760 
$(LOG)/HOLUNITY.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  763 
UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy UNITY/Guar.thy \ 
764 
UNITY/Lift_prog.thy UNITY/ListOrder.thy UNITY/ProgressSets.thy \ 

765 
UNITY/PPROD.thy UNITY/Project.thy UNITY/Rename.thy \ 

766 
UNITY/Transformers.thy UNITY/SubstAx.thy UNITY/UNITY.thy \ 

767 
UNITY/Union.thy UNITY/WFair.thy UNITY/Simple/Channel.thy \ 

768 
UNITY/Simple/Common.thy UNITY/Simple/Deadlock.thy \ 

769 
UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy \ 

770 
UNITY/Simple/NSP_Bad.thy UNITY/Simple/Network.thy \ 

771 
UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy \ 

772 
UNITY/Simple/Token.thy UNITY/Comp/Alloc.thy UNITY/Comp/AllocBase.thy \ 

773 
UNITY/Comp/AllocImpl.thy UNITY/Comp/Client.thy \ 

774 
UNITY/Comp/Counter.thy UNITY/Comp/Counterc.thy \ 

775 
UNITY/Comp/Handshake.thy UNITY/Comp/PriorityAux.thy \ 

776 
UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \ 

777 
UNITY/Comp/TimerArray.thy UNITY/document/root.tex 

28500  778 
@$(ISABELLE_TOOL) usedir g true $(OUT)/HOL UNITY 
4777  779 

780 

10966  781 
## HOLUnix 
782 

783 
HOLUnix: HOL $(LOG)/HOLUnix.gz 

784 

44236
b73b7832b384
moved theory Nested_Environment to HOLUnix (a bit too specific for HOLLibrary);
wenzelm
parents:
44145
diff
changeset

785 
$(LOG)/HOLUnix.gz: $(OUT)/HOL Library/List_Prefix.thy Unix/ROOT.ML \ 
b73b7832b384
moved theory Nested_Environment to HOLUnix (a bit too specific for HOLLibrary);
wenzelm
parents:
44145
diff
changeset

786 
Unix/Nested_Environment.thy Unix/Unix.thy Unix/document/root.bib \ 
b73b7832b384
moved theory Nested_Environment to HOLUnix (a bit too specific for HOLLibrary);
wenzelm
parents:
44145
diff
changeset

787 
Unix/document/root.tex 
39156  788 
@$(ISABELLE_TOOL) usedir m no_brackets m no_type_brackets $(OUT)/HOL Unix 
10966  789 

27477
c64736fe2a1f
more precise dependencies for HOLWord and HOLNSA;
wenzelm
parents:
27470
diff
changeset

790 

19203  791 
## HOLZF 
792 

793 
HOLZF: HOL $(LOG)/HOLZF.gz 

794 

39306
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset

795 
$(LOG)/HOLZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/LProd.thy \ 
27164  796 
ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex 
28500  797 
@$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF 
10966  798 

27477
c64736fe2a1f
more precise dependencies for HOLWord and HOLNSA;
wenzelm
parents:
27470
diff
changeset

799 

29399
ebcd69a00872
split of Imperative_HOL theories from HOLLibrary
haftmann
parents:
29197
diff
changeset

800 
## HOLImperative_HOL 
ebcd69a00872
split of Imperative_HOL theories from HOLLibrary
haftmann
parents:
29197
diff
changeset

801 

ebcd69a00872
split of Imperative_HOL theories from HOLLibrary
haftmann
parents:
29197
diff
changeset

802 
HOLImperative_HOL: HOL $(LOG)/HOLImperative_HOL.gz 
ebcd69a00872
split of Imperative_HOL theories from HOLLibrary
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)/HOLImperative_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 HOLLibrary
haftmann
parents:
29197
diff
changeset

825 

ebcd69a00872
split of Imperative_HOL theories from HOLLibrary
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 
## HOLDecision_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 
HOLDecision_Procs: HOL $(LOG)/HOLDecision_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)/HOLDecision_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  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  844 
Decision_Procs/Parametric_Ferrante_Rackoff.thy \ 
845 
Decision_Procs/Polynomial_List.thy \ 

37120  846 
Decision_Procs/ROOT.ML \ 
35053  847 
Decision_Procs/Reflected_Multivariate_Polynomial.thy \ 
848 
Decision_Procs/commutative_ring_tac.ML \ 

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  852 
Decision_Procs/ex/Dense_Linear_Order_Ex.thy \ 
853 
Decision_Procs/ferrack_tac.ML \ 

37120  854 
Decision_Procs/ferrante_rackoff.ML \ 
855 
Decision_Procs/ferrante_rackoff_data.ML \ 

856 
Decision_Procs/langford.ML \ 

857 
Decision_Procs/langford_data.ML \ 

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 HOLProofs 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 
## HOLProofs 
b98909faaea8
more explicit HOLProofs 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 HOLProofs 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 
HOLProofs: Pure $(OUT)/HOLProofs 
b98909faaea8
more explicit HOLProofs 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 HOLProofs 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)/HOLProofs: main.ML $(MAIN_DEPENDENCIES) 
b98909faaea8
more explicit HOLProofs 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 HOLProofs 
b98909faaea8
more explicit HOLProofs 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 HOLProofs 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 HOLProofs 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 
## HOLProofsex 
b98909faaea8
more explicit HOLProofs 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 HOLProofs 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 
HOLProofsex: HOLProofs $(LOG)/HOLProofsex.gz 
b98909faaea8
more explicit HOLProofs 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 HOLProofs 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)/HOLProofsex.gz: $(OUT)/HOLProofs \ 
b98909faaea8
more explicit HOLProofs 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 HOLProofs 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)/HOLProofs ex 
b98909faaea8
more explicit HOLProofs 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 HOLProofs 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 HOLProofs 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 
## HOLProofsExtraction 
b98909faaea8
more explicit HOLProofs 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 HOLProofs 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 
HOLProofsExtraction: HOLProofs $(LOG)/HOLProofsExtraction.gz 
b98909faaea8
more explicit HOLProofs 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 HOLProofs 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)/HOLProofsExtraction.gz: $(OUT)/HOLProofs \ 
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 HOLProofs 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 HOLProofs 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 HOLProofs 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 HOLProofs 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 HOLProofs 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 HOLProofs 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)/HOLProofs Extraction 
b98909faaea8
more explicit HOLProofs 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 HOLProofs 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 HOLProofs  avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset

898 
## HOLProofsLambda 
2448  899 

34205
f69cd974bc4e
explicit session HOLProofs  avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset

900 
HOLProofsLambda: HOLProofs $(LOG)/HOLProofsLambda.gz 
2448  901 

39157
b98909faaea8
more explicit HOLProofs 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)/HOLProofsLambda.gz: $(OUT)/HOLProofs \ 
b98909faaea8
more explicit HOLProofs 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 HOLProofs 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 HOLProofs 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 HOLProofs 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 HOLProofs 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 HOLProofs 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 HOLProofs 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 HOLProofs 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 HOLProofs 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)/HOLProofs Lambda 
2448  912 

913 

9015  914 
## HOLProlog 
915 

916 
HOLProlog: HOL $(LOG)/HOLProlog.gz 

917 

27164  918 
$(LOG)/HOLProlog.gz: $(OUT)/HOL Prolog/ROOT.ML Prolog/prolog.ML \ 
919 
Prolog/HOHH.thy Prolog/Test.thy Prolog/Func.thy Prolog/Type.thy 

28500  920 
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Prolog 
9015  921 

922 

8012  923 
## HOLMicroJava 
924 

925 
HOLMicroJava: HOL $(LOG)/HOLMicroJava.gz 

926 

46722  927 
$(LOG)/HOLMicroJava.gz: $(OUT)/HOL MicroJava/ROOT.ML \ 
928 
MicroJava/Comp/AuxLemmas.thy MicroJava/Comp/CorrComp.thy \ 

929 
MicroJava/Comp/CorrCompTp.thy MicroJava/Comp/DefsComp.thy \ 

930 
MicroJava/Comp/Index.thy MicroJava/Comp/LemmasComp.thy \ 

27164  931 
MicroJava/Comp/TranslComp.thy MicroJava/Comp/TranslCompTp.thy \ 
932 
MicroJava/Comp/TypeInf.thy MicroJava/J/Conform.thy \ 

933 
MicroJava/J/Eval.thy MicroJava/J/JBasis.thy \ 

934 
MicroJava/J/JTypeSafe.thy MicroJava/J/Decl.thy MicroJava/J/State.thy \ 

935 
MicroJava/J/Term.thy MicroJava/J/Type.thy MicroJava/J/TypeRel.thy \ 

936 
MicroJava/J/WellForm.thy MicroJava/J/Value.thy \ 

937 
MicroJava/J/WellType.thy MicroJava/J/Example.thy \ 

938 
MicroJava/J/JListExample.thy MicroJava/JVM/JVMExec.thy \ 

939 
MicroJava/JVM/JVMInstructions.thy MicroJava/JVM/JVMState.thy \ 

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  947 
MicroJava/DFA/Semilattices.thy \ 
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  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  952 
MicroJava/BV/Effect.thy MicroJava/BV/EffectMono.thy \ 
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  956 
@$(ISABELLE_TOOL) usedir g true $(OUT)/HOL MicroJava 
11850  957 

8012  958 

11376  959 
## HOLNanoJava 
960 

961 
HOLNanoJava: HOL $(LOG)/HOLNanoJava.gz 

962 

27164  963 
$(LOG)/HOLNanoJava.gz: $(OUT)/HOL NanoJava/ROOT.ML NanoJava/Term.thy \ 
964 
NanoJava/Decl.thy NanoJava/TypeRel.thy NanoJava/State.thy \ 

965 
NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy \ 

11376  966 
NanoJava/document/root.bib NanoJava/document/root.tex 
28500  967 
@$(ISABELLE_TOOL) usedir g true $(OUT)/HOL NanoJava 
11850  968 

8193  969 

12855  970 
## HOLBali 
971 

972 
HOLBali: HOL $(LOG)/HOLBali.gz 

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)/HOLBali.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  982 
@$(ISABELLE_TOOL) usedir g true $(OUT)/HOL Bali 
12855  983 

984 

4518  985 
## HOLIOA 
986 

987 
HOLIOA: HOL $(LOG)/HOLIOA.gz 

2448  988 

27164  989 
$(LOG)/HOLIOA.gz: $(OUT)/HOL IOA/Asig.thy IOA/IOA.thy IOA/ROOT.ML \ 
990 
IOA/Solve.thy 

28500  991 
@$(ISABELLE_TOOL) usedir $(OUT)/HOL IOA 
4518  992 

993 

10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset

994 
## HOLLattice 
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 
HOLLattice: HOL $(LOG)/HOLLattice.gz 
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset

997 

27164  998 
$(LOG)/HOLLattice.gz: $(OUT)/HOL Lattice/Bounds.thy \ 
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  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  1004 
## HOLex 
2448  1005 

4518  1006 
HOLex: HOL $(LOG)/HOLex.gz 
2448  1007 

33439  1008 
$(LOG)/HOLex.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 HOLProofs 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 contentfree theory ex/Arithmetic_Series_Complex.thy
huffman
parents:
47205
diff
changeset

1012 
ex/Arith_Examples.thy ex/BT.thy \ 
44276  1013 
ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradox.thy ex/CTL.thy \ 
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  1027 
ex/Quicksort.thy ex/ROOT.ML \ 
44276  1028 
ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy \ 
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  1034 
ex/document/root.bib ex/document/root.tex ex/svc_funcs.ML \ 
1035 
ex/svc_test.thy ../Tools/interpretation_with_defs.ML 

28500  1036 
@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex 
2448  1037 

1038 

33026  1039 
## HOLIsar_Examples 
6445  1040 

33026  1041 
HOLIsar_Examples: HOL $(LOG)/HOLIsar_Examples.gz 
6445  1042 

33026  1043 
$(LOG)/HOLIsar_Examples.gz: $(OUT)/HOL Isar_Examples/Basic_Logic.thy \ 
1044 
Isar_Examples/Cantor.thy Isar_Examples/Drinker.thy \ 

1045 
Isar_Examples/Expr_Compiler.thy Isar_Examples/Fibonacci.thy \ 

47295  1046 
Isar_Examples/Group.thy Isar_Examples/Group_Context.thy \ 
1047 
Isar_Examples/Group_Notepad.thy Isar_Examples/Hoare.thy \ 

33026  1048 
Isar_Examples/Hoare_Ex.thy Isar_Examples/Knaster_Tarski.thy \ 
1049 
Isar_Examples/Mutilated_Checkerboard.thy \ 

1050 
Isar_Examples/Nested_Datatype.thy Isar_Examples/Peirce.thy \ 

1051 
Isar_Examples/Puzzle.thy Isar_Examples/Summation.thy \ 

1052 
Isar_Examples/ROOT.ML Isar_Examples/document/proof.sty \ 

1053 
Isar_Examples/document/root.bib Isar_Examples/document/root.tex \ 

37672  1054 
Isar_Examples/document/style.tex Hoare/hoare_tac.ML \ 
1055 
Number_Theory/Primes.thy 

33026  1056 
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Isar_Examples 
6445  1057 

1058 

33028  1059 
## HOLSET_Protocol 
14199  1060 

33028  1061 
HOLSET_Protocol: HOL $(LOG)/HOLSET_Protocol.gz 
14199  1062 

33028  1063 
$(LOG)/HOLSET_Protocol.gz: $(OUT)/HOL SET_Protocol/ROOT.ML \ 
1064 
SET_Protocol/Message_SET.thy SET_Protocol/Event_SET.thy \ 

1065 
SET_Protocol/Public_SET.thy SET_Protocol/Cardholder_Registration.thy \ 

1066 
SET_Protocol/Merchant_Registration.thy SET_Protocol/Purchase.thy \ 

39757  1067 
SET_Protocol/SET_Protocol.thy SET_Protocol/document/root.tex 
33028  1068 
@$(ISABELLE_TOOL) usedir g true $(OUT)/HOL SET_Protocol 
14199  1069 

1070 

46988
9f492f5b0cec
renamed HOLMatrix to HOLMatrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset

1071 
## HOLMatrix_LP 
14610  1072 

46988
9f492f5b0cec
renamed HOLMatrix to HOLMatrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset

1073 
HOLMatrix_LP: HOL $(LOG)/HOLMatrix_LP.gz 
17323  1074 

46988
9f492f5b0cec
renamed HOLMatrix to HOLMatrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset

1075 
$(LOG)/HOLMatrix_LP.gz: $(OUT)/HOL Matrix_LP/ComputeFloat.thy \ 
9f492f5b0cec
renamed HOLMatrix to HOLMatrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset

1076 
Matrix_LP/ComputeHOL.thy Matrix_LP/ComputeNumeral.thy \ 
9f492f5b0cec
renamed HOLMatrix to HOLMatrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset

1077 
Matrix_LP/Compute_Oracle/Compute_Oracle.thy \ 
9f492f5b0cec
renamed HOLMatrix to HOLMatrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset

1078 
Matrix_LP/Compute_Oracle/am.ML \ 
9f492f5b0cec
renamed HOLMatrix to HOLMatrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset

1079 
Matrix_LP/Compute_Oracle/am_compiler.ML \ 
9f492f5b0cec
renamed HOLMatrix to HOLMatrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset

1080 
Matrix_LP/Compute_Oracle/am_ghc.ML \ 
9f492f5b0cec
renamed HOLMatrix to HOLMatrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset

1081 
Matrix_LP/Compute_Oracle/am_interpreter.ML \ 
9f492f5b0cec
renamed HOLMatrix to HOLMatrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset

1082 
Matrix_LP/Compute_Oracle/am_sml.ML \ 
9f492f5b0cec
renamed HOLMatrix to HOLMatrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset

1083 
Matrix_LP/Compute_Oracle/compute.ML \ 
9f492f5b0cec
renamed HOLMatrix to HOLMatrix_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 HOLMatrix to HOLMatrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset

1085 
Matrix_LP/CplexMatrixConverter.ML Matrix_LP/Cplex_tools.ML \ 
9f492f5b0cec
renamed HOLMatrix to HOLMatrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset

1086 
Matrix_LP/FloatSparseMatrixBuilder.ML Matrix_LP/LP.thy \ 
9f492f5b0cec
renamed HOLMatrix to HOLMatrix_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 HOLMatrix to HOLMatrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset

1088 
Matrix_LP/document/root.tex Matrix_LP/fspmlp.ML \ 
9f492f5b0cec
renamed HOLMatrix to HOLMatrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset

1089 
Matrix_LP/matrixlp.ML Tools/float_arith.ML 
9f492f5b0cec
renamed HOLMatrix to HOLMatrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset

1090 
@$(ISABELLE_TOOL) usedir g true $(OUT)/HOL Matrix_LP 
16873  1091 

14199  1092 

4518  1093 
## TLA 
1094 

1095 
TLA: HOL $(OUT)/TLA 

1096 

27164  1097 
$(OUT)/TLA: $(OUT)/HOL TLA/Action.thy TLA/Init.thy TLA/Intensional.thy \ 
21624  1098 
TLA/ROOT.ML TLA/Stfun.thy TLA/TLA.thy 
28500  1099 
@cd TLA; $(ISABELLE_TOOL) usedir b $(OUT)/HOL TLA 
4518  1100 

1101 

1102 
## TLAInc 

1103 

1104 
TLAInc: TLA $(LOG)/TLAInc.gz 

1105 

21624  1106 
$(LOG)/TLAInc.gz: $(OUT)/TLA TLA/Inc/Inc.thy 
28500  1107 
@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Inc 
4518  1108 

1109 

1110 
## TLABuffer 

1111 

1112 
TLABuffer: TLA $(LOG)/TLABuffer.gz 

2448  1113 

33024
60a098883d81
more accurate dependencies for HOLSMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset

1114 
$(LOG)/TLABuffer.gz: $(OUT)/TLA TLA/Buffer/Buffer.thy \ 
60a098883d81
more accurate dependencies for HOLSMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset

1115 
TLA/Buffer/DBuffer.thy 
28500  1116 
@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Buffer 
4518  1117 

1118 

1119 
## TLAMemory 

1120 

1121 
TLAMemory: TLA $(LOG)/TLAMemory.gz 

4447  1122 

27164  1123 
$(LOG)/TLAMemory.gz: $(OUT)/TLA TLA/Memory/MemClerk.thy \ 
1124 
TLA/Memory/MemClerkParameters.thy TLA/Memory/Memory.thy \ 

1125 
TLA/Memory/MemoryImplementation.thy TLA/Memory/MemoryParameters.thy \ 

1126 
TLA/Memory/ProcedureInterface.thy TLA/Memory/RPC.thy \ 

21624  1127 
TLA/Memory/RPCMemoryParams.thy TLA/Memory/RPCParameters.thy 
28500  1128 
@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Memory 
4518  1129 

1130 

43804
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
43800
diff
changeset

1131 
## HOLTPTP 
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 
HOLTPTP: HOL $(LOG)/HOLTPTP.gz 
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
43800
diff
changeset

1134 

46951  1135 
$(LOG)/HOLTPTP.gz: $(OUT)/HOL \ 
1136 
TPTP/ATP_Problem_Import.thy \ 

1137 
TPTP/ATP_Theory_Export.thy \ 

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  1140 
TPTP/TPTP_Parser.thy \ 
1141 
TPTP/TPTP_Parser/ml_yacc_lib.ML \ 

1142 
TPTP/TPTP_Parser/tptp_interpret.ML \ 

1143 
TPTP/TPTP_Parser/tptp_lexyacc.ML \ 

1144 
TPTP/TPTP_Parser/tptp_parser.ML \ 

1145 
TPTP/TPTP_Parser/tptp_problem_name.ML \ 

1146 
TPTP/TPTP_Parser/tptp_syntax.ML \ 

1147 
TPTP/TPTP_Parser_Test.thy \ 

46324  1148 
TPTP/atp_problem_import.ML \ 
46951  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  1153 
## HOLMultivariate_Analysis 
1154 

36898  1155 
HOLMultivariate_Analysis: HOL $(OUT)/HOLMultivariate_Analysis 
33175  1156 

36937  1157 
$(OUT)/HOLMultivariate_Analysis: $(OUT)/HOL \ 
1158 
Multivariate_Analysis/Brouwer_Fixpoint.thy \ 

47232  1159 
Multivariate_Analysis/Cartesian_Euclidean_Space.thy \ 
36937  1160 
Multivariate_Analysis/Convex_Euclidean_Space.thy \ 
1161 
Multivariate_Analysis/Derivative.thy \ 

1162 
Multivariate_Analysis/Determinants.thy \ 

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  1165 
Multivariate_Analysis/Fashoda.thy \ 
1166 
Multivariate_Analysis/Finite_Cartesian_Product.thy \ 

1167 
Multivariate_Analysis/Integration.certs \ 

1168 
Multivariate_Analysis/Integration.thy \ 

1169 
Multivariate_Analysis/L2_Norm.thy \ 

44288  1170 
Multivariate_Analysis/Linear_Algebra.thy \ 
36937  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  1173 
Multivariate_Analysis/Operator_Norm.thy \ 
1174 
Multivariate_Analysis/Path_Connected.thy \ 

1175 
Multivariate_Analysis/ROOT.ML \ 

1176 
Multivariate_Analysis/Real_Integration.thy \ 

1177 
Multivariate_Analysis/Topology_Euclidean_Space.thy \ 

1178 
Multivariate_Analysis/document/root.tex \ 

37742  1179 
Multivariate_Analysis/normarith.ML Library/Glbs.thy \ 
43920  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  1183 
Library/Product_plus.thy Library/Sum_of_Squares.thy 
36898  1184 
@cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir b g true $(OUT)/HOL HOLMultivariate_Analysis 
33175  1185 

33285  1186 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33270
diff
changeset

1187 
## HOLProbability 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33270
diff
changeset

1188 

38656  1189 
HOLProbability: HOLMultivariate_Analysis $(OUT)/HOLProbability 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33270
diff
changeset

1190 

40863  1191 
$(OUT)/HOLProbability: $(OUT)/HOLMultivariate_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 HOLMultivariate_Analysis and HOLProbability.
hoelzl
parents:
40839
diff
changeset

1195 
Probability/ex/Dining_Cryptographers.thy \ 
a6df324752da
More correct make dependencies for HOLMultivariate_Analysis and HOLProbability.
hoelzl
parents:
40839
diff
changeset

1196 
Probability/ex/Koepf_Duermuth_Countermeasure.thy \ 
42147  1197 
Probability/Finite_Product_Measure.thy \ 
47232  1198 
Probability/Independent_Family.thy \ 
42147  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  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 HOLMultivariate_Analysis and HOLProbability.
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  1205 
@cd Probability; $(ISABELLE_TOOL) usedir b g true $(OUT)/HOLMultivariate_Analysis HOLProbability 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33270
diff
changeset

1206 

39157
b98909faaea8
more explicit HOLProofs 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  1208 
## HOLNominal 
1209 

1210 
HOLNominal: HOL $(OUT)/HOLNominal 

1211 

22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
22167
diff
changeset

1212 
$(OUT)/HOLNominal: $(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  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  1217 
Nominal/nominal_induct.ML \ 
22314  1218 
Nominal/nominal_inductive.ML \ 
28652  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  1223 
Library/Infinite_Set.thy 
28500  1224 
@cd Nominal; $(ISABELLE_TOOL) usedir b g true $(OUT)/HOL HOLNominal 
19497  1225 

1226 

1227 
## HOLNominalExamples 

1228 

1229 
HOLNominalExamples: HOLNominal $(LOG)/HOLNominalExamples.gz 

1230 

39157
b98909faaea8
more explicit HOLProofs 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)/HOLNominalExamples.gz: $(OUT)/HOLNominal \ 
32636
55a0be42327c
added session theory for Bali and Nominal_Examples
haftmann
parents:
32632
diff
changeset

1232 
Nominal/Examples/Nominal_Examples.thy \ 
27163  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 ChurchRosser of BetaReduction
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  1240 
Nominal/Examples/Contexts.thy \ 
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  1243 
Nominal/Examples/Height.thy \ 
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  1246 
Nominal/Examples/LocalWeakening.thy \ 
33189  1247 
Nominal/Examples/Pattern.thy \ 
25725  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  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  1253 
Nominal/Examples/Type_Preservation.thy \ 
25725  1254 
Nominal/Examples/VC_Condition.thy \ 
26195  1255 
Nominal/Examples/W.thy \ 
25725  1256 
Nominal/Examples/Weakening.thy 
28500  1257 
@cd Nominal; $(ISABELLE_TOOL) usedir $(OUT)/HOLNominal Examples 
19497  1258 

1259 

24333  1260 
## HOLWord 
1261 

1262 
HOLWord: HOL $(OUT)/HOLWord 

1263 

33024
60a098883d81
more accurate dependencies for HOLSMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset

1264 
$(OUT)/HOLWord: $(OUT)/HOL Word/ROOT.ML Library/Boolean_Algebra.thy \ 
37655  1265 
Library/Numeral_Type.thy Word/Misc_Numeric.thy Word/Misc_Typedef.thy \ 
37659  1266 
Word/Type_Length.thy Word/Bit_Representation.thy Word/Bit_Int.thy \ 
1267 
Word/Bool_List_Representation.thy Word/Bit_Operations.thy \ 

37660  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  1270 
@cd Word; $(ISABELLE_TOOL) usedir b g true $(OUT)/HOL HOLWord 
24333  1271 

1272 

24442  1273 
## HOLWordExamples 
1274 

1275 
HOLWordExamples: HOLWord $(LOG)/HOLWordExamples.gz 

1276 

27164  1277 
$(LOG)/HOLWordExamples.gz: $(OUT)/HOLWord Word/Examples/ROOT.ML \ 
24442  1278 
Word/Examples/WordExamples.thy 
28500  1279 
@cd Word; $(ISABELLE_TOOL) usedir $(OUT)/HOLWord Examples 