author  bulwahn 
Fri, 11 Mar 2011 10:37:41 +0100  
changeset 41911  c6e66b32ce16 
parent 41906  e163d435ccf7 
child 41919  e180c2a9873b 
permissions  rwrr 
2448  1 
# 
2 
# IsaMakefile for HOL 

3 
# 

4 

4518  5 
## targets 
2448  6 

4518  7 
default: HOL 
27421  8 
generate: HOLGenerateHOL HOLGenerateHOLLight 
33210
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset

9 

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

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

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

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

13 
HOLAlgebra \ 
33419  14 
HOLBoogie \ 
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 \ 
35931  18 
HOLProbability \ 
34205
f69cd974bc4e
explicit session HOLProofs  avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset

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

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

22 
HOL4 \ 
40774  23 
HOLCF \ 
24 
IOA \ 

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

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

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

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

28 
HOLPlain 
10135  29 

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

30 
#Note: keep targets sorted (except for HOLex) 
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset

31 
test: \ 
24325  32 
HOLex \ 
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset

33 
HOLAuth \ 
14031  34 
HOLBali \ 
33439  35 
HOLBoogieExamples \ 
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset

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

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

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

39 
HOLHoare_Parallel \ 
40774  40 
HOLCFFOCUS \ 
41 
HOLCFIMP \ 

42 
HOLCFLibrary \ 

43 
HOLCFTutorial \ 

44 
HOLCFex \ 

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

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

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

47 
HOLIOA \ 
40774  48 
IOAABP \ 
49 
IOANTP \ 

50 
IOAStorage \ 

51 
IOAex \ 

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

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

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

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

56 
HOLLattice \ 
37747  57 
HOLLibraryCodegenerator_Test \ 
28637  58 
HOLMatrix \ 
33027  59 
HOLMetis_Examples \ 
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset

60 
HOLMicroJava \ 
32496  61 
HOLMirabelle \ 
35536  62 
HOLMutabelle \ 
11376  63 
HOLNanoJava \ 
33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

64 
HOLNitpick_Examples \ 
19497  65 
HOLNominalExamples \ 
32479  66 
HOLNumber_Theory \ 
67 
HOLOld_Number_Theory \ 

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

68 
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

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

70 
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

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

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

73 
HOLProofsLambda \ 
33028  74 
HOLSET_Protocol \ 
41569  75 
HOLSPARKExamples \ 
36933
705b58fde476
more precise dependencies for HOLWordSMT_Examples;
wenzelm
parents:
36916
diff
changeset

76 
HOLWordSMT_Examples \ 
25171  77 
HOLStatespace \ 
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset

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

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

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

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

82 
HOLUNITY \ 
10966  83 
HOLUnix \ 
24442  84 
HOLWordExamples \ 
24325  85 
HOLZF 
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset

86 
# ^ this is the sort position 
10614  87 

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

88 
all: test images 
4518  89 

90 

91 
## global settings 

92 

93 
SRC = $(ISABELLE_HOME)/src 

3118  94 
OUT = $(ISABELLE_OUTPUT) 
4447  95 
LOG = $(OUT)/log 
2448  96 

4518  97 

98 
## HOL 

2448  99 

28393  100 
HOL: Pure $(OUT)/HOL 
27368  101 

29505  102 
HOLBase: Pure $(OUT)/HOLBase 
103 

27368  104 
HOLPlain: Pure $(OUT)/HOLPlain 
4518  105 

28401  106 
HOLMain: Pure $(OUT)/HOLMain 
107 

4518  108 
Pure: 
28500  109 
@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure 
3232
19a2b853ba7b
Removal of ex/LexProd; TFL files; new treatment of Prover files
paulson
parents:
3222
diff
changeset

110 

27694  111 
$(OUT)/Pure: Pure 
112 

36073  113 
BASE_DEPENDENCIES = $(OUT)/Pure \ 
30160
5f7b17941730
moved some generic tools to src/Tools/  src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset

114 
$(SRC)/Provers/blast.ML \ 
5f7b17941730
moved some generic tools to src/Tools/  src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset

115 
$(SRC)/Provers/clasimp.ML \ 
5f7b17941730
moved some generic tools to src/Tools/  src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset

116 
$(SRC)/Provers/classical.ML \ 
5f7b17941730
moved some generic tools to src/Tools/  src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset

117 
$(SRC)/Provers/hypsubst.ML \ 
5f7b17941730
moved some generic tools to src/Tools/  src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset

118 
$(SRC)/Provers/quantifier1.ML \ 
5f7b17941730
moved some generic tools to src/Tools/  src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset

119 
$(SRC)/Provers/splitter.ML \ 
37818
dd65033fed78
load cache_io before code generator; moved adhocoverloading to generic tools
haftmann
parents:
37790
diff
changeset

120 
$(SRC)/Tools/cache_io.ML \ 
31771  121 
$(SRC)/Tools/Code/code_haskell.ML \ 
122 
$(SRC)/Tools/Code/code_ml.ML \ 

38970
53d1ee3d98b8
factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
38965
diff
changeset

123 
$(SRC)/Tools/Code/code_namespace.ML \ 
31771  124 
$(SRC)/Tools/Code/code_preproc.ML \ 
125 
$(SRC)/Tools/Code/code_printer.ML \ 

39402  126 
$(SRC)/Tools/Code/code_runtime.ML \ 
34945  127 
$(SRC)/Tools/Code/code_scala.ML \ 
37442  128 
$(SRC)/Tools/Code/code_simp.ML \ 
31771  129 
$(SRC)/Tools/Code/code_target.ML \ 
130 
$(SRC)/Tools/Code/code_thingol.ML \ 

32733
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32674
diff
changeset

131 
$(SRC)/Tools/Code_Generator.thy \ 
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32674
diff
changeset

132 
$(SRC)/Tools/IsaPlanner/isand.ML \ 
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32674
diff
changeset

133 
$(SRC)/Tools/IsaPlanner/rw_inst.ML \ 
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32674
diff
changeset

134 
$(SRC)/Tools/IsaPlanner/rw_tools.ML \ 
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32674
diff
changeset

135 
$(SRC)/Tools/IsaPlanner/zipper.ML \ 
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32674
diff
changeset

136 
$(SRC)/Tools/atomize_elim.ML \ 
39323
ce5c6a8b0359
start renaming "Auto_Counterexample" to "Auto_Tools";
blanchet
parents:
39271
diff
changeset

137 
$(SRC)/Tools/auto_tools.ML \ 
41827  138 
$(SRC)/Tools/case_product.ML \ 
30160
5f7b17941730
moved some generic tools to src/Tools/  src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset

139 
$(SRC)/Tools/coherent.ML \ 
32733
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32674
diff
changeset

140 
$(SRC)/Tools/cong_tac.ML \ 
30160
5f7b17941730
moved some generic tools to src/Tools/  src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset

141 
$(SRC)/Tools/eqsubst.ML \ 
5f7b17941730
moved some generic tools to src/Tools/  src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset

142 
$(SRC)/Tools/induct.ML \ 
32733
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32674
diff
changeset

143 
$(SRC)/Tools/induct_tacs.ML \ 
30165
6ee87f67d9cd
moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
30160
diff
changeset

144 
$(SRC)/Tools/intuitionistic.ML \ 
37781
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
37779
diff
changeset

145 
$(SRC)/Tools/misc_legacy.ML \ 
30160
5f7b17941730
moved some generic tools to src/Tools/  src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset

146 
$(SRC)/Tools/nbe.ML \ 
32733
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32674
diff
changeset

147 
$(SRC)/Tools/project_rule.ML \ 
30973
304ab57afa6e
observe distinction between Pure/Tools and Tools more closely
haftmann
parents:
30954
diff
changeset

148 
$(SRC)/Tools/quickcheck.ML \ 
40116
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
40067
diff
changeset

149 
$(SRC)/Tools/solve_direct.ML \ 
30160
5f7b17941730
moved some generic tools to src/Tools/  src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset

150 
$(SRC)/Tools/value.ML \ 
29505  151 
HOL.thy \ 
152 
Tools/hologic.ML \ 

153 
Tools/recfun_codegen.ML \ 

36073  154 
Tools/simpdata.ML 
29505  155 

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

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

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

159 
PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES) \ 
40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset

160 
$(SRC)/Provers/Arith/cancel_div_mod.ML \ 
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset

161 
$(SRC)/Provers/Arith/cancel_sums.ML \ 
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset

162 
$(SRC)/Provers/Arith/fast_lin_arith.ML \ 
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset

163 
$(SRC)/Provers/order.ML \ 
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset

164 
$(SRC)/Provers/trancl.ML \ 
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset

165 
$(SRC)/Tools/Metis/metis.ML \ 
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset

166 
$(SRC)/Tools/rat.ML \ 
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset

167 
$(SRC)/Tools/subtyping.ML \ 
32139  168 
Complete_Lattice.thy \ 
40108  169 
Complete_Partial_Order.thy \ 
27368  170 
Datatype.thy \ 
171 
Extraction.thy \ 

35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35039
diff
changeset

172 
Fields.thy \ 
27368  173 
Finite_Set.thy \ 
174 
Fun.thy \ 

175 
FunDef.thy \ 

35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35039
diff
changeset

176 
Groups.thy \ 
27368  177 
Inductive.thy \ 
178 
Lattices.thy \ 

39945  179 
Meson.thy \ 
39946  180 
Metis.thy \ 
27368  181 
Nat.thy \ 
32733
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32674
diff
changeset

182 
Option.thy \ 
27368  183 
Orderings.thy \ 
40108  184 
Partial_Function.thy \ 
27368  185 
Plain.thy \ 
186 
Power.thy \ 

187 
Predicate.thy \ 

188 
Product_Type.thy \ 

189 
Relation.thy \ 

35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35039
diff
changeset

190 
Rings.thy \ 
27368  191 
SAT.thy \ 
192 
Set.thy \ 

193 
Sum_Type.thy \ 

40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset

194 
Tools/Datatype/datatype.ML \ 
31771  195 
Tools/Datatype/datatype_abs_proofs.ML \ 
196 
Tools/Datatype/datatype_aux.ML \ 

197 
Tools/Datatype/datatype_case.ML \ 

198 
Tools/Datatype/datatype_codegen.ML \ 

33963
977b94b64905
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33954
diff
changeset

199 
Tools/Datatype/datatype_data.ML \ 
31771  200 
Tools/Datatype/datatype_prop.ML \ 
201 
Tools/Datatype/datatype_realizer.ML \ 

202 
Tools/Function/context_tree.ML \ 

40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset

203 
Tools/Function/fun.ML \ 
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset

204 
Tools/Function/function.ML \ 
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
33098
diff
changeset

205 
Tools/Function/function_common.ML \ 
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
33098
diff
changeset

206 
Tools/Function/function_core.ML \ 
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
33098
diff
changeset

207 
Tools/Function/function_lib.ML \ 
33471  208 
Tools/Function/induction_schema.ML \ 
31771  209 
Tools/Function/lexicographic_order.ML \ 
210 
Tools/Function/measure_functions.ML \ 

211 
Tools/Function/mutual.ML \ 

40108  212 
Tools/Function/partial_function.ML \ 
33083  213 
Tools/Function/pat_completeness.ML \ 
31771  214 
Tools/Function/pattern_split.ML \ 
33100  215 
Tools/Function/relation.ML \ 
31771  216 
Tools/Function/scnp_reconstruct.ML \ 
217 
Tools/Function/scnp_solve.ML \ 

218 
Tools/Function/size.ML \ 

219 
Tools/Function/sum_tree.ML \ 

220 
Tools/Function/termination.ML \ 

39940  221 
Tools/Meson/meson.ML \ 
222 
Tools/Meson/meson_clausify.ML \ 

39948  223 
Tools/Meson/meson_tactic.ML \ 
39946  224 
Tools/Metis/metis_reconstruct.ML \ 
40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset

225 
Tools/Metis/metis_tactics.ML \ 
39946  226 
Tools/Metis/metis_translate.ML \ 
40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset

227 
Tools/abel_cancel.ML \ 
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset

228 
Tools/arith_data.ML \ 
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset

229 
Tools/cnf_funcs.ML \ 
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset

230 
Tools/dseq.ML \ 
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset

231 
Tools/inductive.ML \ 
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset

232 
Tools/inductive_codegen.ML \ 
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset

233 
Tools/inductive_realizer.ML \ 
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset

234 
Tools/inductive_set.ML \ 
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset

235 
Tools/lin_arith.ML \ 
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
30457
diff
changeset

236 
Tools/nat_arith.ML \ 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31706
diff
changeset

237 
Tools/primrec.ML \ 
27368  238 
Tools/prop_logic.ML \ 
239 
Tools/refute.ML \ 

240 
Tools/rewrite_hol_proof.ML \ 

241 
Tools/sat_funcs.ML \ 

242 
Tools/sat_solver.ML \ 

243 
Tools/split_rule.ML \ 

38942
e10c11971fa7
"try"  a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
38730
diff
changeset

244 
Tools/try.ML \ 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31706
diff
changeset

245 
Tools/typedef.ML \ 
41505
6d19301074cf
"enriched_type" replaces less specific "type_lifting"
haftmann
parents:
41496
diff
changeset

246 
Tools/enriched_type.ML \ 
27368  247 
Transitive_Closure.thy \ 
248 
Typedef.thy \ 

40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset

249 
Wellfounded.thy 
28312
f0838044f034
different session branches for HOLPlain vs. Plain
haftmann
parents:
28243
diff
changeset

250 

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

251 
$(OUT)/HOLPlain: plain.ML $(PLAIN_DEPENDENCIES) 
28500  252 
@$(ISABELLE_TOOL) usedir b f plain.ML g true $(OUT)/Pure HOLPlain 
27368  253 

28401  254 
MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \ 
40178
00152d17855b
reverted e7a80c6752c9  there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
blanchet
parents:
40162
diff
changeset

255 
ATP.thy \ 
35725
4d7e3cc9c52c
Big_Operators now in Main rather than Plain src/HOL/Wellfounded.thy
haftmann
parents:
35719
diff
changeset

256 
Big_Operators.thy \ 
32657  257 
Code_Evaluation.thy \ 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

258 
Code_Numeral.thy \ 
33296
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
33272
diff
changeset

259 
Divides.thy \ 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34228
diff
changeset

260 
DSequence.thy \ 
27368  261 
Equiv_Relations.thy \ 
40650
d40b347d5b0b
adding Enum to HOLMain image and removing it from HOLLibrary
bulwahn
parents:
40634
diff
changeset

262 
Enum.thy \ 
27368  263 
Groebner_Basis.thy \ 
264 
Hilbert_Choice.thy \ 

32733
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32674
diff
changeset

265 
Int.thy \ 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34228
diff
changeset

266 
Lazy_Sequence.thy \ 
27421  267 
List.thy \ 
268 
Main.thy \ 

269 
Map.thy \ 

30925  270 
Nat_Numeral.thy \ 
33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33298
diff
changeset

271 
Nat_Transfer.thy \ 
39183
512c10416590
adding dependencies to IsaMakefile; increasing negative search limit for predicate_compile_quickcheck; adding tracing of introduction rules in code_prolog
bulwahn
parents:
39048
diff
changeset

272 
New_DSequence.thy \ 
512c10416590
adding dependencies to IsaMakefile; increasing negative search limit for predicate_compile_quickcheck; adding tracing of introduction rules in code_prolog
bulwahn
parents:
39048
diff
changeset

273 
New_Random_Sequence.thy \ 
36915
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset

274 
Nitpick.thy \ 
33356
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
33348
diff
changeset

275 
Numeral_Simprocs.thy \ 
27421  276 
Presburger.thy \ 
33250
5c2af18a3237
including the predicate compiler in HOLMain; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33210
diff
changeset

277 
Predicate_Compile.thy \ 
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31186
diff
changeset

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

279 
Quotient.thy \ 
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31186
diff
changeset

280 
Random.thy \ 
34948
2d5f2a9f7601
refactoring the predicate compiler; adding theories for Sequences; adding retrieval to Spec_Rules; adding timing to Quickcheck
bulwahn
parents:
34228
diff
changeset

281 
Random_Sequence.thy \ 
27421  282 
Recdef.thy \ 
39271  283 
Record.thy \ 
36916  284 
Refute.thy \ 
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36700
diff
changeset

285 
Semiring_Normalization.thy \ 
27421  286 
SetInterval.thy \ 
40178
00152d17855b
reverted e7a80c6752c9  there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
blanchet
parents:
40162
diff
changeset

287 
Sledgehammer.thy \ 
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
40355
diff
changeset

288 
Smallcheck.thy \ 
36898  289 
SMT.thy \ 
31048
ac146fc38b51
refined HOL string theories and corresponding ML fragments
haftmann
parents:
31036
diff
changeset

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

291 
Typerep.thy \ 
27421  292 
$(SRC)/Provers/Arith/assoc_fold.ML \ 
293 
$(SRC)/Provers/Arith/cancel_numeral_factor.ML \ 

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

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

296 
$(SRC)/Provers/Arith/extract_common_term.ML \ 

38047  297 
Tools/ATP/atp_problem.ML \ 
39452  298 
Tools/ATP/atp_proof.ML \ 
38047  299 
Tools/ATP/atp_systems.ML \ 
33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33298
diff
changeset

300 
Tools/choice_specification.ML \ 
39564  301 
Tools/code_evaluation.ML \ 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31060
diff
changeset

302 
Tools/int_arith.ML \ 
36753
5cf4e9128f22
renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents:
36751
diff
changeset

303 
Tools/groebner.ML \ 
31055
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
31048
diff
changeset

304 
Tools/list_code.ML \ 
41463
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
41426
diff
changeset

305 
Tools/list_to_set_comprehension.ML \ 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31060
diff
changeset

306 
Tools/nat_numeral_simprocs.ML \ 
36915
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset

307 
Tools/Nitpick/kodkod.ML \ 
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset

308 
Tools/Nitpick/kodkod_sat.ML \ 
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset

309 
Tools/Nitpick/nitpick.ML \ 
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset

310 
Tools/Nitpick/nitpick_hol.ML \ 
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset

311 
Tools/Nitpick/nitpick_isar.ML \ 
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset

312 
Tools/Nitpick/nitpick_kodkod.ML \ 
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset

313 
Tools/Nitpick/nitpick_model.ML \ 
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset

314 
Tools/Nitpick/nitpick_mono.ML \ 
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset

315 
Tools/Nitpick/nitpick_nut.ML \ 
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset

316 
Tools/Nitpick/nitpick_peephole.ML \ 
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset

317 
Tools/Nitpick/nitpick_preproc.ML \ 
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset

318 
Tools/Nitpick/nitpick_rep.ML \ 
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset

319 
Tools/Nitpick/nitpick_scope.ML \ 
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset

320 
Tools/Nitpick/nitpick_tests.ML \ 
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset

321 
Tools/Nitpick/nitpick_util.ML \ 
27421  322 
Tools/numeral.ML \ 
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31060
diff
changeset

323 
Tools/numeral_simprocs.ML \ 
27421  324 
Tools/numeral_syntax.ML \ 
40141
0e8a4e27a685
adding new predicate compiler files to the IsaMakefile
bulwahn
parents:
40123
diff
changeset

325 
Tools/Predicate_Compile/core_data.ML \ 
0e8a4e27a685
adding new predicate compiler files to the IsaMakefile
bulwahn
parents:
40123
diff
changeset

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

327 
Tools/Predicate_Compile/predicate_compile_aux.ML \ 
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
36032
diff
changeset

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

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

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

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

332 
Tools/Predicate_Compile/predicate_compile.ML \ 
40141
0e8a4e27a685
adding new predicate compiler files to the IsaMakefile
bulwahn
parents:
40123
diff
changeset

333 
Tools/Predicate_Compile/predicate_compile_proof.ML \ 
36032
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
35972
diff
changeset

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

335 
Tools/Predicate_Compile/predicate_compile_pred.ML \ 
31260  336 
Tools/quickcheck_generators.ML \ 
27421  337 
Tools/Qelim/cooper.ML \ 
36803  338 
Tools/Qelim/cooper_procedure.ML \ 
27421  339 
Tools/Qelim/qelim.ML \ 
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset

340 
Tools/Quotient/quotient_def.ML \ 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset

341 
Tools/Quotient/quotient_info.ML \ 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset

342 
Tools/Quotient/quotient_tacs.ML \ 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset

343 
Tools/Quotient/quotient_term.ML \ 
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset

344 
Tools/Quotient/quotient_typ.ML \ 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31706
diff
changeset

345 
Tools/recdef.ML \ 
38394
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
38282
diff
changeset

346 
Tools/record.ML \ 
36753
5cf4e9128f22
renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents:
36751
diff
changeset

347 
Tools/semiring_normalizer.ML \ 
41042
8275f52ac991
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents:
41023
diff
changeset

348 
Tools/Sledgehammer/async_manager.ML \ 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41065
diff
changeset

349 
Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML \ 
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41065
diff
changeset

350 
Tools/Sledgehammer/sledgehammer_atp_translate.ML \ 
38986  351 
Tools/Sledgehammer/sledgehammer_filter.ML \ 
352 
Tools/Sledgehammer/sledgehammer_minimize.ML \ 

35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset

353 
Tools/Sledgehammer/sledgehammer_isar.ML \ 
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41065
diff
changeset

354 
Tools/Sledgehammer/sledgehammer_provers.ML \ 
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41065
diff
changeset

355 
Tools/Sledgehammer/sledgehammer_run.ML \ 
35967  356 
Tools/Sledgehammer/sledgehammer_util.ML \ 
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
40355
diff
changeset

357 
Tools/smallvalue_generators.ML \ 
36898  358 
Tools/SMT/smtlib_interface.ML \ 
40277  359 
Tools/SMT/smt_builtin.ML \ 
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40420
diff
changeset

360 
Tools/SMT/smt_config.ML \ 
41426
09615ed31f04
reimplemented support for datatypes (including records and typedefs);
boehmes
parents:
41413
diff
changeset

361 
Tools/SMT/smt_datatypes.ML \ 
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40420
diff
changeset

362 
Tools/SMT/smt_failure.ML \ 
36898  363 
Tools/SMT/smt_monomorph.ML \ 
364 
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

365 
Tools/SMT/smt_setup_solvers.ML \ 
36898  366 
Tools/SMT/smt_solver.ML \ 
367 
Tools/SMT/smt_translate.ML \ 

40662
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40650
diff
changeset

368 
Tools/SMT/smt_utils.ML \ 
36898  369 
Tools/SMT/z3_interface.ML \ 
370 
Tools/SMT/z3_model.ML \ 

371 
Tools/SMT/z3_proof_literals.ML \ 

40662
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40650
diff
changeset

372 
Tools/SMT/z3_proof_methods.ML \ 
36898  373 
Tools/SMT/z3_proof_parser.ML \ 
374 
Tools/SMT/z3_proof_reconstruction.ML \ 

375 
Tools/SMT/z3_proof_tools.ML \ 

31055
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
31048
diff
changeset

376 
Tools/string_code.ML \ 
27421  377 
Tools/string_syntax.ML \ 
33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33298
diff
changeset

378 
Tools/transfer.ML \ 
27421  379 
Tools/TFL/casesplit.ML \ 
380 
Tools/TFL/dcterm.ML \ 

381 
Tools/TFL/post.ML \ 

382 
Tools/TFL/rules.ML \ 

383 
Tools/TFL/tfl.ML \ 

384 
Tools/TFL/thms.ML \ 

385 
Tools/TFL/thry.ML \ 

386 
Tools/TFL/usyntax.ML \ 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28476
diff
changeset

387 
Tools/TFL/utils.ML 
28401  388 

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

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

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

392 
HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \ 
30096  393 
Archimedean_Field.thy \ 
32733
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32674
diff
changeset

394 
Complex.thy \ 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset

395 
Complex_Main.thy \ 
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset

396 
Deriv.thy \ 
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset

397 
Fact.thy \ 
32479  398 
GCD.thy \ 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset

399 
Lim.thy \ 
31352  400 
Limits.thy \ 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset

401 
Ln.thy \ 
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset

402 
Log.thy \ 
32479  403 
Lubs.thy \ 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset

404 
MacLaurin.thy \ 
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset

405 
NthRoot.thy \ 
32733
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32674
diff
changeset

406 
Parity.thy \ 
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32674
diff
changeset

407 
RComplete.thy \ 
35372  408 
Rat.thy \ 
32733
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32674
diff
changeset

409 
Real.thy \ 
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32674
diff
changeset

410 
RealDef.thy \ 
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32674
diff
changeset

411 
RealVector.thy \ 
29197
6d4cb27ed19c
adapted HOL source structure to distribution layout
haftmann
parents:
29181
diff
changeset

412 
SEQ.thy \ 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset

413 
Series.thy \ 
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
33083
diff
changeset

414 
SupInf.thy \ 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset

415 
Taylor.thy \ 
40839
48e01d16dd17
activate subtyping/coercions in theory Complex_Main;
wenzelm
parents:
40837
diff
changeset

416 
Tools/SMT/smt_real.ML \ 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset

417 
Tools/float_syntax.ML \ 
40839
48e01d16dd17
activate subtyping/coercions in theory Complex_Main;
wenzelm
parents:
40837
diff
changeset

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

419 

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

420 
$(OUT)/HOL: ROOT.ML $(HOL_DEPENDENCIES) 
f69cd974bc4e
explicit session HOLProofs  avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset

421 
@$(ISABELLE_TOOL) usedir b g true $(OUT)/Pure HOL 
f69cd974bc4e
explicit session HOLProofs  avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset

422 

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

423 

10255  424 
## HOLLibrary 
425 

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

426 
HOLLibrary: HOL $(OUT)/HOLLibrary 
10255  427 

38137
6fda94059baa
renamed funny Library ROOT files back to default ROOT.ML  ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents:
38119
diff
changeset

428 
$(OUT)/HOLLibrary: $(OUT)/HOL Library/ROOT.ML \ 
37691
4915de09b4d3
build image for session HOLLibrary; introduced distinct session HOLCodegenerator_Test
haftmann
parents:
37672
diff
changeset

429 
$(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML \ 
37818
dd65033fed78
load cache_io before code generator; moved adhocoverloading to generic tools
haftmann
parents:
37790
diff
changeset

430 
Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy \ 
38137
6fda94059baa
renamed funny Library ROOT files back to default ROOT.ML  ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents:
38119
diff
changeset

431 
Library/AssocList.thy Library/BigO.thy Library/Binomial.thy \ 
37968  432 
Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy \ 
37662  433 
Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy \ 
38137
6fda94059baa
renamed funny Library ROOT files back to default ROOT.ML  ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents:
38119
diff
changeset

434 
Library/Code_Integer.thy Library/Code_Natural.thy \ 
38119
e00f970425e9
adding Code_Prolog theory to IsaMakefile and HOLLibrary root file
bulwahn
parents:
38074
diff
changeset

435 
Library/Code_Prolog.thy Tools/Predicate_Compile/code_prolog.ML \ 
37968  436 
Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy \ 
38137
6fda94059baa
renamed funny Library ROOT files back to default ROOT.ML  ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents:
38119
diff
changeset

437 
Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy \ 
40650
d40b347d5b0b
adding Enum to HOLMain image and removing it from HOLLibrary
bulwahn
parents:
40634
diff
changeset

438 
Library/Efficient_Nat.thy Library/Eval_Witness.thy \ 
37968  439 
Library/Executable_Set.thy Library/Float.thy \ 
440 
Library/Formal_Power_Series.thy Library/Fraction_Field.thy \ 

40672
abd4e7358847
replaced misleading Fset/fset name  these do not stand for finite sets
haftmann
parents:
40582
diff
changeset

441 
Library/FrechetDeriv.thy Library/Cset.thy Library/FuncSet.thy \ 
38622  442 
Library/Function_Algebras.thy \ 
37968  443 
Library/Fundamental_Theorem_Algebra.thy Library/Glbs.thy \ 
444 
Library/Indicator_Function.thy Library/Infinite_Set.thy \ 

445 
Library/Inner_Product.thy Library/Kleene_Algebra.thy \ 

37118
ccae4ecd67f4
eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir f HOL_Library_ROOT.ML;
wenzelm
parents:
37024
diff
changeset

446 
Library/LaTeXsugar.thy Library/Lattice_Algebras.thy \ 
ccae4ecd67f4
eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir f HOL_Library_ROOT.ML;
wenzelm
parents:
37024
diff
changeset

447 
Library/Lattice_Syntax.thy Library/Library.thy \ 
ccae4ecd67f4
eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir f HOL_Library_ROOT.ML;
wenzelm
parents:
37024
diff
changeset

448 
Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy \ 
37790  449 
Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy \ 
37818
dd65033fed78
load cache_io before code generator; moved adhocoverloading to generic tools
haftmann
parents:
37790
diff
changeset

450 
Library/Multiset.thy Library/Nat_Bijection.thy \ 
38137
6fda94059baa
renamed funny Library ROOT files back to default ROOT.ML  ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents:
38119
diff
changeset

451 
Library/Nat_Infinity.thy Library/Nested_Environment.thy \ 
6fda94059baa
renamed funny Library ROOT files back to default ROOT.ML  ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents:
38119
diff
changeset

452 
Library/Numeral_Type.thy Library/OptionalSugar.thy \ 
6fda94059baa
renamed funny Library ROOT files back to default ROOT.ML  ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents:
38119
diff
changeset

453 
Library/Order_Relation.thy Library/Permutation.thy \ 
6fda94059baa
renamed funny Library ROOT files back to default ROOT.ML  ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents:
38119
diff
changeset

454 
Library/Permutations.thy Library/Poly_Deriv.thy \ 
6fda94059baa
renamed funny Library ROOT files back to default ROOT.ML  ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents:
38119
diff
changeset

455 
Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy \ 
6fda94059baa
renamed funny Library ROOT files back to default ROOT.ML  ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents:
38119
diff
changeset

456 
Library/Preorder.thy Library/Product_Vector.thy \ 
6fda94059baa
renamed funny Library ROOT files back to default ROOT.ML  ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents:
38119
diff
changeset

457 
Library/Product_ord.thy Library/Product_plus.thy \ 
40349  458 
Library/Quickcheck_Types.thy \ 
37118
ccae4ecd67f4
eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir f HOL_Library_ROOT.ML;
wenzelm
parents:
37024
diff
changeset

459 
Library/Quotient_List.thy Library/Quotient_Option.thy \ 
ccae4ecd67f4
eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir f HOL_Library_ROOT.ML;
wenzelm
parents:
37024
diff
changeset

460 
Library/Quotient_Product.thy Library/Quotient_Sum.thy \ 
ccae4ecd67f4
eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir f HOL_Library_ROOT.ML;
wenzelm
parents:
37024
diff
changeset

461 
Library/Quotient_Syntax.thy Library/Quotient_Type.thy \ 
ccae4ecd67f4
eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir f HOL_Library_ROOT.ML;
wenzelm
parents:
37024
diff
changeset

462 
Library/RBT.thy Library/RBT_Impl.thy Library/README.html \ 
38622  463 
Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy \ 
464 
Library/Reflection.thy Library/SML_Quickcheck.thy \ 

41474  465 
Library/Sublist_Order.thy Library/Sum_of_Squares.thy \ 
466 
Library/Sum_of_Squares/sos_wrapper.ML \ 

467 
Library/Sum_of_Squares/sum_of_squares.ML \ 

37118
ccae4ecd67f4
eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir f HOL_Library_ROOT.ML;
wenzelm
parents:
37024
diff
changeset

468 
Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy \ 
ccae4ecd67f4
eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir f HOL_Library_ROOT.ML;
wenzelm
parents:
37024
diff
changeset

469 
Library/While_Combinator.thy Library/Zorn.thy \ 
37818
dd65033fed78
load cache_io before code generator; moved adhocoverloading to generic tools
haftmann
parents:
37790
diff
changeset

470 
$(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML \ 
37789  471 
Library/reflection.ML Library/reify_data.ML \ 
41906  472 
Library/LSC.thy $(SRC)/HOL/Tools/LSC/lazysmallcheck.ML \ 
473 
$(SRC)/HOL/Tools/LSC/LazySmallCheck.hs \ 

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

474 
Library/document/root.bib Library/document/root.tex 
38137
6fda94059baa
renamed funny Library ROOT files back to default ROOT.ML  ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents:
38119
diff
changeset

475 
@cd Library; $(ISABELLE_TOOL) usedir b $(OUT)/HOL HOLLibrary 
10255  476 

477 

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

478 
## HOLHahn_Banach 
27421  479 

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

480 
HOLHahn_Banach: HOL $(LOG)/HOLHahn_Banach.gz 
27421  481 

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

482 
$(LOG)/HOLHahn_Banach.gz: $(OUT)/HOL Hahn_Banach/Bounds.thy \ 
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset

483 
Hahn_Banach/Function_Norm.thy Hahn_Banach/Function_Order.thy \ 
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset

484 
Hahn_Banach/Hahn_Banach.thy Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy \ 
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset

485 
Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Hahn_Banach/Linearform.thy \ 
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset

486 
Hahn_Banach/Normed_Space.thy Hahn_Banach/README.html \ 
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset

487 
Hahn_Banach/ROOT.ML Hahn_Banach/Subspace.thy \ 
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset

488 
Hahn_Banach/Vector_Space.thy Hahn_Banach/Zorn_Lemma.thy \ 
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset

489 
Hahn_Banach/document/root.bib Hahn_Banach/document/root.tex 
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset

490 
@$(ISABELLE_TOOL) usedir g true $(OUT)/HOL Hahn_Banach 
27421  491 

492 

4518  493 
## HOLSubst 
494 

495 
HOLSubst: HOL $(LOG)/HOLSubst.gz 

496 

27164  497 
$(LOG)/HOLSubst.gz: $(OUT)/HOL Subst/AList.thy Subst/ROOT.ML \ 
498 
Subst/Subst.thy Subst/UTerm.thy Subst/Unifier.thy Subst/Unify.thy 

28500  499 
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Subst 
2448  500 

501 

4518  502 
## HOLInduct 
2473  503 

4518  504 
HOLInduct: HOL $(LOG)/HOLInduct.gz 
3125  505 

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

506 
$(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

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

508 
Induct/QuoDataType.thy Induct/ROOT.ML Induct/Sexp.thy \ 
35249  509 
Induct/Sigma_Algebra.thy Induct/ABexp.thy Induct/SList.thy \ 
510 
Induct/Term.thy Induct/Tree.thy Induct/document/root.tex 

28500  511 
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Induct 
3125  512 

513 

4518  514 
## HOLIMP 
515 

516 
HOLIMP: HOL $(LOG)/HOLIMP.gz 

2448  517 

27164  518 
$(LOG)/HOLIMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Compiler0.thy \ 
519 
IMP/Compiler.thy IMP/Denotation.thy IMP/Expr.thy IMP/Hoare.thy \ 

520 
IMP/Natural.thy IMP/Examples.thy IMP/Transition.thy IMP/VC.thy \ 

521 
IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib 

28500  522 
@$(ISABELLE_TOOL) usedir g true $(OUT)/HOL IMP 
2448  523 

524 

8179  525 
## HOLIMPP 
526 

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

528 

27164  529 
$(LOG)/HOLIMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy \ 
19803  530 
IMPP/Natural.thy IMPP/Hoare.thy IMPP/Misc.thy IMPP/EvenOdd.thy 
28500  531 
@$(ISABELLE_TOOL) usedir $(OUT)/HOL IMPP 
8179  532 

533 

27421  534 
## HOLImport 
14516  535 

19097  536 
IMPORTER_FILES = Import/lazy_seq.ML Import/proof_kernel.ML Import/replay.ML \ 
20610  537 
Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \ 
14516  538 
Import/HOL4Syntax.thy Import/HOL4Compat.thy Import/import_syntax.ML \ 
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31706
diff
changeset

539 
Import/hol4rews.ML Import/import.ML Import/ROOT.ML 
14516  540 

17323  541 
IMPORTER_HOLLIGHT_FILES = Import/proof_kernel.ML Import/replay.ML \ 
542 
Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \ 

543 
Import/HOL4Syntax.thy Import/HOLLightCompat.thy Import/import_syntax.ML \ 

31771  544 
Import/hol4rews.ML Import/import.ML Import/ROOT.ML 
17323  545 

27421  546 
HOLImport: HOL $(LOG)/HOLImport.gz 
14516  547 

27421  548 
$(LOG)/HOLImport.gz: $(OUT)/HOL $(IMPORTER_FILES) 
37296  549 
@$(ISABELLE_TOOL) usedir p 0 $(OUT)/HOL Import 
14516  550 

551 

27421  552 
## HOLGenerateHOL 
14516  553 

27421  554 
HOLGenerateHOL: HOL $(LOG)/HOLGenerateHOL.gz 
14516  555 

27421  556 
$(LOG)/HOLGenerateHOL.gz: $(OUT)/HOL \ 
27164  557 
$(IMPORTER_FILES) Import/GenerateHOL/GenHOL4Base.thy \ 
558 
Import/GenerateHOL/GenHOL4Prob.thy \ 

559 
Import/GenerateHOL/GenHOL4Real.thy \ 

560 
Import/GenerateHOL/GenHOL4Vec.thy \ 

14516  561 
Import/GenerateHOL/GenHOL4Word32.thy Import/GenerateHOL/ROOT.ML 
28500  562 
@cd Import; $(ISABELLE_TOOL) usedir $(OUT)/HOL GenerateHOL 
14516  563 

17460  564 

27421  565 
## HOLGenerateHOLLight 
17460  566 

27421  567 
HOLGenerateHOLLight: HOL $(LOG)/HOLGenerateHOLLight.gz 
17323  568 

37742  569 
$(LOG)/HOLGenerateHOLLight.gz: $(OUT)/HOL \ 
27164  570 
$(IMPORTER_HOLLIGHT_FILES) Import/GenerateHOLLight/GenHOLLight.thy \ 
571 
Import/GenerateHOLLight/ROOT.ML 

28500  572 
@cd Import; $(ISABELLE_TOOL) usedir $(OUT)/HOL GenerateHOLLight 
14516  573 

17460  574 

14516  575 
## HOLImportHOL 
576 

27421  577 
HOL4: HOL $(LOG)/HOL4.gz 
14516  578 

579 
HOL_IMPORT_FILES = arithmetic.imp bits.imp boolean_sequence.imp bool.imp \ 

580 
bword_arith.imp bword_bitop.imp bword_num.imp combin.imp divides.imp \ 

581 
hrat.imp hreal.imp ind_type.imp lim.imp list.imp marker.imp nets.imp \ 

582 
numeral.imp num.imp one.imp operator.imp option.imp pair.imp poly.imp \ 

583 
powser.imp pred_set.imp prime.imp prim_rec.imp prob_algebra.imp \ 

584 
prob_canon.imp prob_extra.imp prob.imp prob_indep.imp prob_pseudo.imp \ 

23194  585 
prob_uniform.imp realax.imp real.imp relation.imp res_quan.imp \ 
586 
rich_list.imp \ 

14516  587 
seq.imp state_transformer.imp sum.imp topology.imp transc.imp word32.imp \ 
588 
word_base.imp word_bitop.imp word_num.imp 

589 

37742  590 
$(LOG)/HOL4.gz: $(OUT)/HOL $(IMPORTER_FILES) \ 
27164  591 
$(HOL_IMPORT_FILES:%=Import/HOL/%) Import/HOL/HOL4Base.thy \ 
592 
Import/HOL/HOL4Prob.thy Import/HOL/HOL4Real.thy \ 

593 
Import/HOL/HOL4Vec.thy Import/HOL/HOL4Word32.thy Import/HOL/HOL4.thy \ 

594 
Import/HOL/ROOT.ML 

28500  595 
@cd Import/HOL; $(ISABELLE_TOOL) usedir b $(OUT)/HOL HOL4 
14516  596 

27421  597 
HOLLight: HOL $(LOG)/HOLLight.gz 
17645  598 

37742  599 
$(LOG)/HOLLight.gz: $(OUT)/HOL $(IMPORTER_HOLLIGHT_FILES) \ 
27164  600 
Import/HOLLight/hollight.imp Import/HOLLight/HOLLight.thy \ 
17645  601 
Import/HOLLight/ROOT.ML 
28500  602 
@cd Import/HOLLight; $(ISABELLE_TOOL) usedir b $(OUT)/HOL HOLLight 
17645  603 

14516  604 

32479  605 
## HOLNumber_Theory 
31719  606 

32479  607 
HOLNumber_Theory: HOL $(LOG)/HOLNumber_Theory.gz 
31719  608 

32479  609 
$(LOG)/HOLNumber_Theory.gz: $(OUT)/HOL $(ALGEBRA_DEPENDENCIES) \ 
31771  610 
Library/Multiset.thy \ 
32479  611 
Number_Theory/Binomial.thy \ 
612 
Number_Theory/Cong.thy \ 

613 
Number_Theory/Fib.thy \ 

614 
Number_Theory/MiscAlgebra.thy \ 

615 
Number_Theory/Number_Theory.thy \ 

616 
Number_Theory/Residues.thy \ 

617 
Number_Theory/UniqueFactorization.thy \ 

618 
Number_Theory/ROOT.ML 

619 
@$(ISABELLE_TOOL) usedir g true $(OUT)/HOL Number_Theory 

31719  620 

621 

32479  622 
## HOLOld_Number_Theory 
9510  623 

32479  624 
HOLOld_Number_Theory: HOL $(LOG)/HOLOld_Number_Theory.gz 
9510  625 

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

628 
Old_Number_Theory/Factorization.thy Old_Number_Theory/BijectionRel.thy\ 

629 
Old_Number_Theory/Chinese.thy Old_Number_Theory/EulerFermat.thy \ 

630 
Old_Number_Theory/IntFact.thy Old_Number_Theory/IntPrimes.thy \ 

631 
Old_Number_Theory/WilsonBij.thy Old_Number_Theory/WilsonRuss.thy \ 

632 
Old_Number_Theory/Finite2.thy Old_Number_Theory/Int2.thy \ 

633 
Old_Number_Theory/EvenOdd.thy Old_Number_Theory/Residues.thy \ 

634 
Old_Number_Theory/Euler.thy Old_Number_Theory/Gauss.thy \ 

32479  635 
Old_Number_Theory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy \ 
37021  636 
Old_Number_Theory/Legacy_GCD.thy Old_Number_Theory/Pocklington.thy \ 
637 
Old_Number_Theory/ROOT.ML 

32479  638 
@$(ISABELLE_TOOL) usedir g true $(OUT)/HOL Old_Number_Theory 
9510  639 

640 

4518  641 
## HOLHoare 
642 

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

2448  644 

27164  645 
$(LOG)/HOLHoare.gz: $(OUT)/HOL Hoare/Arith2.thy Hoare/Examples.thy \ 
646 
Hoare/Hoare.thy Hoare/hoare_tac.ML Hoare/Heap.thy \ 

35319  647 
Hoare/Hoare_Logic.thy Hoare/Hoare_Logic_Abort.thy \ 
27164  648 
Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy Hoare/ROOT.ML \ 
649 
Hoare/ExamplesAbort.thy Hoare/HeapSyntaxAbort.thy \ 

35319  650 
Hoare/SchorrWaite.thy Hoare/Separation.thy \ 
27164  651 
Hoare/SepLogHeap.thy Hoare/document/root.tex Hoare/document/root.bib 
28500  652 
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Hoare 
2448  653 

654 

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

655 
## HOLHoare_Parallel 
12996  656 

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

657 
HOLHoare_Parallel: HOL $(LOG)/HOLHoare_Parallel.gz 
12996  658 

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

659 
$(LOG)/HOLHoare_Parallel.gz: $(OUT)/HOL Hoare_Parallel/Gar_Coll.thy \ 
33439  660 
Hoare_Parallel/Graph.thy Hoare_Parallel/Hoare_Parallel.thy \ 
661 
Hoare_Parallel/Mul_Gar_Coll.thy Hoare_Parallel/OG_Com.thy \ 

662 
Hoare_Parallel/OG_Examples.thy Hoare_Parallel/OG_Hoare.thy \ 

663 
Hoare_Parallel/OG_Syntax.thy Hoare_Parallel/OG_Tactics.thy \ 

664 
Hoare_Parallel/OG_Tran.thy Hoare_Parallel/Quote_Antiquote.thy \ 

665 
Hoare_Parallel/RG_Com.thy Hoare_Parallel/RG_Examples.thy \ 

666 
Hoare_Parallel/RG_Hoare.thy Hoare_Parallel/RG_Syntax.thy \ 

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

668 
Hoare_Parallel/document/root.tex Hoare_Parallel/document/root.bib 

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

669 
@$(ISABELLE_TOOL) usedir g true $(OUT)/HOL Hoare_Parallel 
12996  670 

671 

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

673 

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

675 

37747  676 
$(LOG)/HOLLibraryCodegenerator_Test.gz: $(OUT)/HOLLibrary \ 
37742  677 
Codegenerator_Test/ROOT.ML \ 
678 
Codegenerator_Test/Candidates.thy \ 

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

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

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

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

682 
@$(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

683 

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

684 

33027  685 
## HOLMetis_Examples 
23449  686 

33027  687 
HOLMetis_Examples: HOL $(LOG)/HOLMetis_Examples.gz 
23449  688 

41144  689 
$(LOG)/HOLMetis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML \ 
690 
Metis_Examples/Abstraction.thy Metis_Examples/BigO.thy \ 

691 
Metis_Examples/BT.thy Metis_Examples/HO_Reas.thy \ 

692 
Metis_Examples/Message.thy Metis_Examples/Tarski.thy \ 

693 
Metis_Examples/TransClosure.thy Metis_Examples/set.thy 

33027  694 
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples 
23449  695 

696 

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

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

698 

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

699 
HOLNitpick_Examples: HOL $(LOG)/HOLNitpick_Examples.gz 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

700 

34126  701 
$(LOG)/HOLNitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \ 
702 
Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \ 

35076
cc19e2aef17e
added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents:
35070
diff
changeset

703 
Nitpick_Examples/Hotel_Nits.thy Nitpick_Examples/Induct_Nits.thy \ 
cc19e2aef17e
added hotel key card example for Nitpick, and renumber atoms in Nitpick's output for increased readability
blanchet
parents:
35070
diff
changeset

704 
Nitpick_Examples/Integer_Nits.thy Nitpick_Examples/Manual_Nits.thy \ 
39221
70fd4a3c41ed
remove "minipick" (the toy version of Nitpick) and some tests;
blanchet
parents:
39048
diff
changeset

705 
Nitpick_Examples/Mono_Nits.thy Nitpick_Examples/Nitpick_Examples.thy \ 
70fd4a3c41ed
remove "minipick" (the toy version of Nitpick) and some tests;
blanchet
parents:
39048
diff
changeset

706 
Nitpick_Examples/Pattern_Nits.thy Nitpick_Examples/Record_Nits.thy \ 
70fd4a3c41ed
remove "minipick" (the toy version of Nitpick) and some tests;
blanchet
parents:
39048
diff
changeset

707 
Nitpick_Examples/Refute_Nits.thy Nitpick_Examples/Special_Nits.thy \ 
70fd4a3c41ed
remove "minipick" (the toy version of Nitpick) and some tests;
blanchet
parents:
39048
diff
changeset

708 
Nitpick_Examples/Tests_Nits.thy Nitpick_Examples/Typedef_Nits.thy 
33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

709 
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples 
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset

710 

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

711 

7999
7acf6eb8eec1
Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
7985
diff
changeset

712 
## HOLAlgebra 
7acf6eb8eec1
Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
7985
diff
changeset

713 

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

715 

31771  716 
ALGEBRA_DEPENDENCIES = $(OUT)/HOL \ 
717 
Algebra/ROOT.ML \ 

718 
Library/Binomial.thy \ 

719 
Library/FuncSet.thy \ 

720 
Library/Multiset.thy \ 

721 
Library/Permutation.thy \ 

32479  722 
Number_Theory/Primes.thy \ 
31771  723 
Algebra/AbelCoset.thy \ 
724 
Algebra/Bij.thy \ 

725 
Algebra/Congruence.thy \ 

726 
Algebra/Coset.thy \ 

727 
Algebra/Divisibility.thy \ 

728 
Algebra/Exponent.thy \ 

729 
Algebra/FiniteProduct.thy \ 

730 
Algebra/Group.thy \ 

731 
Algebra/Ideal.thy \ 

732 
Algebra/IntRing.thy \ 

733 
Algebra/Lattice.thy \ 

734 
Algebra/Module.thy \ 

735 
Algebra/QuotRing.thy \ 

736 
Algebra/Ring.thy \ 

737 
Algebra/RingHom.thy \ 

738 
Algebra/Sylow.thy \ 

739 
Algebra/UnivPoly.thy \ 

740 
Algebra/abstract/Abstract.thy \ 

741 
Algebra/abstract/Factor.thy \ 

742 
Algebra/abstract/Field.thy \ 

743 
Algebra/abstract/Ideal2.thy \ 

744 
Algebra/abstract/PID.thy \ 

745 
Algebra/abstract/Ring2.thy \ 

746 
Algebra/abstract/RingHomo.thy \ 

747 
Algebra/document/root.tex \ 

748 
Algebra/document/root.tex \ 

749 
Algebra/poly/LongDiv.thy \ 

750 
Algebra/poly/PolyHomo.thy \ 

751 
Algebra/poly/Polynomial.thy \ 

752 
Algebra/poly/UnivPoly2.thy \ 

753 
Algebra/ringsimp.ML 

754 

33448  755 
$(OUT)/HOLAlgebra: $(ALGEBRA_DEPENDENCIES) 
28500  756 
@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

757 

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

758 

4518  759 
## HOLAuth 
3819  760 

4518  761 
HOLAuth: HOL $(LOG)/HOLAuth.gz 
3819  762 

28098  763 
$(LOG)/HOLAuth.gz: $(OUT)/HOL \ 
37021  764 
Auth/Auth_Shared.thy Auth/Auth_Public.thy Auth/All_Symmetric.thy \ 
765 
Auth/Guard/Auth_Guard_Shared.thy \ 

766 
Auth/Guard/Auth_Guard_Public.thy \ 

32632  767 
Auth/Smartcard/Auth_Smartcard.thy Auth/All_Symmetric.thy \ 
27164  768 
Auth/CertifiedEmail.thy Auth/Event.thy Auth/Message.thy \ 
769 
Auth/NS_Public.thy Auth/NS_Public_Bad.thy Auth/NS_Shared.thy \ 

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

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

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

773 
Auth/Kerberos_BAN_Gets.thy Auth/KerberosIV.thy \ 

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

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

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

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

778 
Auth/Guard/Guard.thy Auth/Guard/List_Msg.thy \ 

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

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

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

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

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

28500  784 
@$(ISABELLE_TOOL) usedir g true $(OUT)/HOL Auth 
2448  785 

786 

4777  787 
## HOLUNITY 
788 

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

790 

27164  791 
$(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

792 
UNITY/UNITY_Main.thy UNITY/UNITY_tactics.ML UNITY/Comp.thy \ 
2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well  essentially reverting 3dec57ec3473;
wenzelm
parents:
41854
diff
changeset

793 
UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy \ 
27164  794 
UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy UNITY/Guar.thy \ 
795 
UNITY/Lift_prog.thy UNITY/ListOrder.thy UNITY/ProgressSets.thy \ 

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

797 
UNITY/Transformers.thy UNITY/SubstAx.thy UNITY/UNITY.thy \ 

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

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

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

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

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

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

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

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

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

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

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

28500  809 
@$(ISABELLE_TOOL) usedir g true $(OUT)/HOL UNITY 
4777  810 

811 

10966  812 
## HOLUnix 
813 

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

815 

37742  816 
$(LOG)/HOLUnix.gz: $(OUT)/HOL Library/Nested_Environment.thy \ 
817 
Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy \ 

10966  818 
Unix/document/root.bib Unix/document/root.tex 
39156  819 
@$(ISABELLE_TOOL) usedir m no_brackets m no_type_brackets $(OUT)/HOL Unix 
10966  820 

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

821 

19203  822 
## HOLZF 
823 

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

825 

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

826 
$(LOG)/HOLZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/LProd.thy \ 
27164  827 
ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex 
28500  828 
@$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF 
10966  829 

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

830 

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

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

832 

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

833 
HOLImperative_HOL: HOL $(LOG)/HOLImperative_HOL.gz 
ebcd69a00872
split of Imperative_HOL theories from HOLLibrary
haftmann
parents:
29197
diff
changeset

834 

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

835 
$(LOG)/HOLImperative_HOL.gz: $(OUT)/HOL \ 
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset

836 
Imperative_HOL/Array.thy \ 
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset

837 
Imperative_HOL/Heap.thy \ 
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset

838 
Imperative_HOL/Heap_Monad.thy \ 
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset

839 
Imperative_HOL/Imperative_HOL.thy \ 
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset

840 
Imperative_HOL/Imperative_HOL_ex.thy \ 
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset

841 
Imperative_HOL/Mrec.thy \ 
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset

842 
Imperative_HOL/Ref.thy \ 
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset

843 
Imperative_HOL/ROOT.ML \ 
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset

844 
Imperative_HOL/ex/Imperative_Quicksort.thy \ 
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset

845 
Imperative_HOL/ex/Imperative_Reverse.thy \ 
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset

846 
Imperative_HOL/ex/Linked_Lists.thy \ 
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset

847 
Imperative_HOL/ex/SatChecker.thy \ 
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset

848 
Imperative_HOL/ex/Sorted_List.thy \ 
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset

849 
Imperative_HOL/ex/Subarray.thy \ 
30689
b14b2cc4e25e
moved Imperative_HOL examples to Imperative_HOL/ex
haftmann
parents:
30654
diff
changeset

850 
Imperative_HOL/ex/Sublist.thy 
39306
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset

851 
@$(ISABELLE_TOOL) usedir g true m iff m no_brackets $(OUT)/HOL Imperative_HOL 
29399
ebcd69a00872
split of Imperative_HOL theories from HOLLibrary
haftmann
parents:
29197
diff
changeset

852 

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

853 

29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset

854 
## HOLDecision_Procs 
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset

855 

0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset

856 
HOLDecision_Procs: HOL $(LOG)/HOLDecision_Procs.gz 
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset

857 

0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset

858 
$(LOG)/HOLDecision_Procs.gz: $(OUT)/HOL \ 
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset

859 
Decision_Procs/Approximation.thy \ 
33356
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
33348
diff
changeset

860 
Decision_Procs/Commutative_Ring.thy \ 
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
33348
diff
changeset

861 
Decision_Procs/Commutative_Ring_Complete.thy \ 
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset

862 
Decision_Procs/Cooper.thy \ 
35053  863 
Decision_Procs/Decision_Procs.thy \ 
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset

864 
Decision_Procs/Dense_Linear_Order.thy \ 
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset

865 
Decision_Procs/Ferrack.thy \ 
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset

866 
Decision_Procs/MIR.thy \ 
35053  867 
Decision_Procs/Parametric_Ferrante_Rackoff.thy \ 
868 
Decision_Procs/Polynomial_List.thy \ 

37120  869 
Decision_Procs/ROOT.ML \ 
35053  870 
Decision_Procs/Reflected_Multivariate_Polynomial.thy \ 
871 
Decision_Procs/commutative_ring_tac.ML \ 

872 
Decision_Procs/cooper_tac.ML \ 

30429
39acdf031548
moved Decision_Procs examples to Decision_Procs/ex
haftmann
parents:
30400
diff
changeset

873 
Decision_Procs/ex/Approximation_Ex.thy \ 
33356
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
33348
diff
changeset

874 
Decision_Procs/ex/Commutative_Ring_Ex.thy \ 
35053  875 
Decision_Procs/ex/Dense_Linear_Order_Ex.thy \ 
876 
Decision_Procs/ferrack_tac.ML \ 

37120  877 
Decision_Procs/ferrante_rackoff.ML \ 
878 
Decision_Procs/ferrante_rackoff_data.ML \ 

879 
Decision_Procs/langford.ML \ 

880 
Decision_Procs/langford_data.ML \ 

881 
Decision_Procs/mir_tac.ML 

29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset

882 
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Decision_Procs 
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset

883 

0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset

884 

39157
b98909faaea8
more explicit 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

885 
## 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

886 

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 
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

888 

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

889 
$(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

890 
@$(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

891 

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 

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 
## 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

894 

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 
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

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 
$(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

898 
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

899 
@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

900 

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

901 

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 
## 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

903 

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 
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

905 

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 
$(LOG)/HOLProofsExtraction.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

907 
Library/Efficient_Nat.thy Proofs/Extraction/Euclid.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/Extraction/Greatest_Common_Divisor.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/Extraction/Higman.thy Proofs/Extraction/Pigeonhole.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

910 
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

911 
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

912 
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

913 
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

914 
@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

915 

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

916 

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

917 
## HOLProofsLambda 
2448  918 

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

919 
HOLProofsLambda: HOLProofs $(LOG)/HOLProofsLambda.gz 
2448  920 

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

921 
$(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

922 
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

923 
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

924 
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

925 
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

926 
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

927 
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

928 
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

929 
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

930 
@cd Proofs; $(ISABELLE_TOOL) usedir g true m no_brackets p 2 q 0 $(OUT)/HOLProofs Lambda 
2448  931 

932 

9015  933 
## HOLProlog 
934 

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

936 

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

28500  939 
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Prolog 
9015  940 

941 

8012  942 
## HOLMicroJava 
943 

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

945 

27164  946 
$(LOG)/HOLMicroJava.gz: $(OUT)/HOL Library/Executable_Set.thy \ 
947 
MicroJava/ROOT.ML MicroJava/Comp/AuxLemmas.thy \ 

948 
MicroJava/Comp/CorrComp.thy MicroJava/Comp/CorrCompTp.thy \ 

949 
MicroJava/Comp/DefsComp.thy MicroJava/Comp/Index.thy \ 

950 
MicroJava/Comp/LemmasComp.thy MicroJava/Comp/NatCanonify.thy \ 

951 
MicroJava/Comp/TranslComp.thy MicroJava/Comp/TranslCompTp.thy \ 

952 
MicroJava/Comp/TypeInf.thy MicroJava/J/Conform.thy \ 

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

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

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

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

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

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

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

960 
MicroJava/JVM/JVMExecInstr.thy MicroJava/JVM/JVMListExample.thy \ 

33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33820
diff
changeset

961 
MicroJava/JVM/JVMExceptions.thy MicroJava/DFA/Abstract_BV.thy \ 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33820
diff
changeset

962 
MicroJava/DFA/Err.thy MicroJava/DFA/Kildall.thy \ 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33820
diff
changeset

963 
MicroJava/DFA/LBVComplete.thy MicroJava/DFA/LBVCorrect.thy \ 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33820
diff
changeset

964 
MicroJava/DFA/LBVSpec.thy MicroJava/DFA/Listn.thy \ 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33820
diff
changeset

965 
MicroJava/DFA/Opt.thy MicroJava/DFA/Product.thy \ 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33820
diff
changeset

966 
MicroJava/DFA/SemilatAlg.thy MicroJava/DFA/Semilat.thy \ 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33820
diff
changeset

967 
MicroJava/DFA/Semilattices.thy MicroJava/DFA/Typing_Framework_err.thy \ 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33820
diff
changeset

968 
MicroJava/DFA/Typing_Framework.thy MicroJava/BV/BVSpec.thy \ 
27164  969 
MicroJava/BV/BVSpecTypeSafe.thy MicroJava/BV/Correct.thy \ 
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33820
diff
changeset

970 
MicroJava/BV/JType.thy MicroJava/BV/JVM.thy MicroJava/BV/JVMType.thy \ 
27164  971 
MicroJava/BV/Effect.thy MicroJava/BV/EffectMono.thy \ 
972 
MicroJava/BV/Typing_Framework_JVM.thy MicroJava/BV/BVExample.thy \ 

33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33820
diff
changeset

973 
MicroJava/BV/LBVJVM.thy MicroJava/document/root.bib \ 
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33820
diff
changeset

974 
MicroJava/document/root.tex MicroJava/document/introduction.tex 
28500  975 
@$(ISABELLE_TOOL) usedir g true $(OUT)/HOL MicroJava 
11850  976 

8012  977 

11376  978 
## HOLNanoJava 
979 

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

981 

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

984 
NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy \ 

11376  985 
NanoJava/document/root.bib NanoJava/document/root.tex 
28500  986 
@$(ISABELLE_TOOL) usedir g true $(OUT)/HOL NanoJava 
11850  987 

8193  988 

12855  989 
## HOLBali 
990 

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

992 

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

993 
$(LOG)/HOLBali.gz: $(OUT)/HOL Bali/Bali.thy Bali/AxCompl.thy \ 
60a098883d81
more accurate dependencies for HOLSMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset

994 
Bali/AxExample.thy Bali/AxSem.thy Bali/AxSound.thy Bali/Basis.thy \ 
60a098883d81
more accurate dependencies for HOLSMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset

995 
Bali/Conform.thy Bali/Decl.thy Bali/DeclConcepts.thy Bali/Eval.thy \ 
60a098883d81
more accurate dependencies for HOLSMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset

996 
Bali/Evaln.thy Bali/Example.thy Bali/Name.thy Bali/ROOT.ML \ 
60a098883d81
more accurate dependencies for HOLSMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset

997 
Bali/State.thy Bali/Table.thy Bali/Term.thy Bali/Trans.thy \ 
60a098883d81
more accurate dependencies for HOLSMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset

998 
Bali/Type.thy Bali/TypeRel.thy Bali/TypeSafe.thy Bali/Value.thy \ 
60a098883d81
more accurate dependencies for HOLSMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset

999 
Bali/WellForm.thy Bali/DefiniteAssignment.thy \ 
60a098883d81
more accurate dependencies for HOLSMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset

1000 
Bali/DefiniteAssignmentCorrect.thy Bali/WellType.thy \ 
60a098883d81
more accurate dependencies for HOLSMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset

1001 
Bali/document/root.tex 
28500  1002 
@$(ISABELLE_TOOL) usedir g true $(OUT)/HOL Bali 
12855  1003 

1004 

4518  1005 
## HOLIOA 
1006 

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

2448  1008 

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

28500  1011 
@$(ISABELLE_TOOL) usedir $(OUT)/HOL IOA 
4518  1012 

1013 

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

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

1015 

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

1016 
HOLLattice: HOL $(LOG)/HOLLattice.gz 
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset

1017 

27164  1018 
$(LOG)/HOLLattice.gz: $(OUT)/HOL Lattice/Bounds.thy \ 
1019 
Lattice/CompleteLattice.thy Lattice/Lattice.thy Lattice/Orders.thy \ 

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

1020 
Lattice/ROOT.ML Lattice/document/root.tex 
28500  1021 
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Lattice 
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset

1022 

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

1023 

4518  1024 
## HOLex 
2448  1025 

4518  1026 
HOLex: HOL $(LOG)/HOLex.gz 
2448  1027 

33439  1028 
$(LOG)/HOLex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.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

1029 
Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.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

1030 
ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy ex/BT.thy \ 
40837  1031 
ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradoxon.thy ex/CTL.thy \ 
41827  1032 
ex/Case_Product.thy \ 
40837  1033 
ex/Chinese.thy ex/Classical.thy ex/CodegenSML_Test.thy \ 
1034 
ex/Coercion_Examples.thy ex/Coherent.thy ex/Dedekind_Real.thy \ 

1035 
ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy \ 

1036 
ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy \ 

1037 
ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy \ 

1038 
ex/Higher_Order_Logic.thy ex/Iff_Oracle.thy ex/Induction_Schema.thy \ 

1039 
ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \ 

41582
c34415351b6d
experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
41569
diff
changeset

1040 
ex/Interpretation_with_Defs.thy ex/Intuitionistic.thy ex/Lagrange.thy \ 
c34415351b6d
experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
41569
diff
changeset

1041 
ex/List_to_Set_Comprehension_Examples.thy ex/LocaleTest2.thy \ 
41911
c6e66b32ce16
adding lazysmallcheck example theory to HOLex session
bulwahn
parents:
41906
diff
changeset

1042 
ex/LSC_Examples.thy \ 
41582
c34415351b6d
experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
41569
diff
changeset

1043 
ex/MT.thy ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \ 
40837  1044 
ex/Multiquote.thy ex/NatSum.thy ex/Normalization_by_Evaluation.thy \ 
1045 
ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \ 

1046 
ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \ 

1047 
ex/Quicksort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \ 

1048 
ex/ReflectionEx.thy ex/Refute_Examples.thy ex/SAT_Examples.thy \ 

41582
c34415351b6d
experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
41569
diff
changeset

1049 
ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy ex/Sqrt.thy \ 
c34415351b6d
experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
41569
diff
changeset

1050 
ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy \ 
c34415351b6d
experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
41569
diff
changeset

1051 
ex/Transfer_Ex.thy ex/Tree23.thy ex/Unification.thy \ 
c34415351b6d
experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
41569
diff
changeset

1052 
ex/While_Combinator_Example.thy ex/document/root.bib \ 
c34415351b6d
experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
41569
diff
changeset

1053 
ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy \ 
c34415351b6d
experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
41569
diff
changeset

1054 
../Tools/interpretation_with_defs.ML 
28500  1055 
@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex 
2448  1056 

1057 

33026  1058 
## HOLIsar_Examples 
6445  1059 

33026  1060 
HOLIsar_Examples: HOL $(LOG)/HOLIsar_Examples.gz 
6445  1061 

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

1064 
Isar_Examples/Expr_Compiler.thy Isar_Examples/Fibonacci.thy \ 

1065 
Isar_Examples/Group.thy Isar_Examples/Hoare.thy \ 

1066 
Isar_Examples/Hoare_Ex.thy Isar_Examples/Knaster_Tarski.thy \ 

1067 
Isar_Examples/Mutilated_Checkerboard.thy \ 

1068 
Isar_Examples/Nested_Datatype.thy Isar_Examples/Peirce.thy \ 

1069 
Isar_Examples/Puzzle.thy Isar_Examples/Summation.thy \ 

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

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

37672  1072 
Isar_Examples/document/style.tex Hoare/hoare_tac.ML \ 
1073 
Number_Theory/Primes.thy 

33026  1074 
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Isar_Examples 
6445  1075 

1076 

33028  1077 
## HOLSET_Protocol 
14199  1078 

33028  1079 
HOLSET_Protocol: HOL $(LOG)/HOLSET_Protocol.gz 
14199  1080 

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

1083 
SET_Protocol/Public_SET.thy SET_Protocol/Cardholder_Registration.thy \ 

1084 
SET_Protocol/Merchant_Registration.thy SET_Protocol/Purchase.thy \ 

39757  1085 
SET_Protocol/SET_Protocol.thy SET_Protocol/document/root.tex 
33028  1086 
@$(ISABELLE_TOOL) usedir g true $(OUT)/HOL SET_Protocol 
14199  1087 

1088 

27421  1089 
## HOLMatrix 
14610  1090 

28637  1091 
HOLMatrix: HOL $(LOG)/HOLMatrix.gz 
17323  1092 

37872
d83659570337
moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle  it actually depends on HOL anyway;
wenzelm
parents:
37818
diff
changeset

1093 
$(LOG)/HOLMatrix.gz: $(OUT)/HOL Matrix/ComputeFloat.thy \ 
d83659570337
moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle  it actually depends on HOL anyway;
wenzelm
parents:
37818
diff
changeset

1094 
Matrix/ComputeHOL.thy Matrix/ComputeNumeral.thy \ 
d83659570337
moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle  it actually depends on HOL anyway;
wenzelm
parents:
37818
diff
changeset

1095 
Matrix/Compute_Oracle/Compute_Oracle.thy Matrix/Compute_Oracle/am.ML \ 
d83659570337
moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle  it actually depends on HOL anyway;
wenzelm
parents:
37818
diff
changeset

1096 
Matrix/Compute_Oracle/am_compiler.ML Matrix/Compute_Oracle/am_ghc.ML \ 
d83659570337
moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle  it actually depends on HOL anyway;
wenzelm
parents:
37818
diff
changeset

1097 
Matrix/Compute_Oracle/am_interpreter.ML \ 
d83659570337
moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle  it actually depends on HOL anyway;
wenzelm
parents:
37818
diff
changeset

1098 
Matrix/Compute_Oracle/am_sml.ML Matrix/Compute_Oracle/compute.ML \ 
d83659570337
moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle  it actually depends on HOL anyway;
wenzelm
parents:
37818
diff
changeset

1099 
Matrix/Compute_Oracle/linker.ML Matrix/Cplex.thy \ 
37764  1100 
Matrix/CplexMatrixConverter.ML Matrix/Cplex_tools.ML \ 
37872
d83659570337
moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle  it actually depends on HOL anyway;
wenzelm
parents:
37818
diff
changeset

1101 
Matrix/FloatSparseMatrixBuilder.ML Matrix/LP.thy Matrix/Matrix.thy \ 
d83659570337
moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle  it actually depends on HOL anyway;
wenzelm
parents:
37818
diff
changeset

1102 
Matrix/ROOT.ML Matrix/SparseMatrix.thy Matrix/document/root.tex \ 
d83659570337
moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle  it actually depends on HOL anyway;
wenzelm
parents:
37818
diff
changeset

1103 
Matrix/fspmlp.ML Matrix/matrixlp.ML Tools/float_arith.ML 
28500  1104 
@$(ISABELLE_TOOL) usedir g true $(OUT)/HOL Matrix 
16873  1105 

14199  1106 

4518  1107 
## TLA 
1108 

1109 
TLA: HOL $(OUT)/TLA 

1110 

27164  1111 
$(OUT)/TLA: $(OUT)/HOL TLA/Action.thy TLA/Init.thy TLA/Intensional.thy \ 
21624  1112 
TLA/ROOT.ML TLA/Stfun.thy TLA/TLA.thy 
28500  1113 
@cd TLA; $(ISABELLE_TOOL) usedir b $(OUT)/HOL TLA 
4518  1114 

1115 

1116 
## TLAInc 

1117 

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

1119 

21624  1120 
$(LOG)/TLAInc.gz: $(OUT)/TLA TLA/Inc/Inc.thy 
28500  1121 
@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Inc 
4518  1122 

1123 

1124 
## TLABuffer 

1125 

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

2448  1127 

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

1128 
$(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

1129 
TLA/Buffer/DBuffer.thy 
28500  1130 
@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Buffer 
4518  1131 

1132 

1133 
## TLAMemory 

1134 

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

4447  1136 

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

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

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

21624  1141 
TLA/Memory/RPCMemoryParams.thy TLA/Memory/RPCParameters.thy 
28500  1142 
@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Memory 
4518  1143 

1144 

33175  1145 
## HOLMultivariate_Analysis 
1146 

36898  1147 
HOLMultivariate_Analysis: HOL $(OUT)/HOLMultivariate_Analysis 
33175  1148 

36937  1149 
$(OUT)/HOLMultivariate_Analysis: $(OUT)/HOL \ 
1150 
Multivariate_Analysis/Brouwer_Fixpoint.thy \ 

37522  1151 
Multivariate_Analysis/Cartesian_Euclidean_Space.thy \ 
36937  1152 
Multivariate_Analysis/Convex_Euclidean_Space.thy \ 
1153 
Multivariate_Analysis/Derivative.thy \ 

1154 
Multivariate_Analysis/Determinants.thy \ 

1155 
Multivariate_Analysis/Euclidean_Space.thy \ 

1156 
Multivariate_Analysis/Fashoda.thy \ 

1157 
Multivariate_Analysis/Finite_Cartesian_Product.thy \ 

1158 
Multivariate_Analysis/Integration.certs \ 

1159 
Multivariate_Analysis/Integration.thy \ 

1160 
Multivariate_Analysis/L2_Norm.thy \ 

1161 
Multivariate_Analysis/Multivariate_Analysis.thy \ 

1162 
Multivariate_Analysis/Operator_Norm.thy \ 

1163 
Multivariate_Analysis/Path_Connected.thy \ 

1164 
Multivariate_Analysis/ROOT.ML \ 

1165 
Multivariate_Analysis/Real_Integration.thy \ 

1166 
Multivariate_Analysis/Topology_Euclidean_Space.thy \ 

1167 
Multivariate_Analysis/document/root.tex \ 

37742  1168 
Multivariate_Analysis/normarith.ML Library/Glbs.thy \ 
40860
a6df324752da
More correct make dependencies for HOLMultivariate_Analysis and HOLProbability.
hoelzl
parents:
40839
diff
changeset

1169 
Library/Indicator_Function.thy Library/Inner_Product.thy \ 
a6df324752da
More correct make dependencies for HOLMultivariate_Analysis and HOLProbability.
hoelzl
parents:
40839
diff
changeset

1170 
Library/Numeral_Type.thy Library/Convex.thy Library/FrechetDeriv.thy \ 
36649
bfd8c550faa6
Corrected imports; better approximation of dependencies.
hoelzl
parents:
36648
diff
changeset

1171 
Library/Product_Vector.thy Library/Product_plus.thy 
36898  1172 
@cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir b g true $(OUT)/HOL HOLMultivariate_Analysis 
33175  1173 

33285  1174 

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

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

1176 

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

1178 

40863  1179 
$(OUT)/HOLProbability: $(OUT)/HOLMultivariate_Analysis \ 
40860
a6df324752da
More correct make dependencies for HOLMultivariate_Analysis and HOLProbability.
hoelzl
parents:
40839
diff
changeset

1180 
Probability/Borel_Space.thy Probability/Caratheodory.thy \ 
a6df324752da
More correct make dependencies for HOLMultivariate_Analysis and HOLProbability.
hoelzl
parents:
40839
diff
changeset

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

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

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

1184 
Probability/Information.thy Probability/Lebesgue_Integration.thy \ 
a6df324752da
More correct make dependencies for HOLMultivariate_Analysis and HOLProbability.
hoelzl
parents:
40839
diff
changeset

1185 
Probability/Lebesgue_Measure.thy Probability/Measure.thy \ 
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40969
diff
changeset

1186 
Probability/Positive_Extended_Real.thy \ 
40860
a6df324752da
More correct make dependencies for HOLMultivariate_Analysis and HOLProbability.
hoelzl
parents:
40839
diff
changeset

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

1188 
Probability/Product_Measure.thy Probability/Radon_Nikodym.thy \ 
a6df324752da
More correct make dependencies for HOLMultivariate_Analysis and HOLProbability.
hoelzl
parents:
40839
diff
changeset

1189 
Probability/ROOT.ML Probability/Sigma_Algebra.thy \ 
a6df324752da
More correct make dependencies for HOLMultivariate_Analysis and HOLProbability.
hoelzl
parents:
40839
diff
changeset

1190 
Library/Countable.thy Library/FuncSet.thy \ 
a6df324752da
More correct make dependencies for HOLMultivariate_Analysis and HOLProbability.
hoelzl
parents:
40839
diff
changeset

1191 
Library/Nat_Bijection.thy 
38656  1192 
@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

1193 

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

1194 

19497  1195 
## HOLNominal 
1196 

1197 
HOLNominal: HOL $(OUT)/HOLNominal 

1198 

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

1199 
$(OUT)/HOLNominal: $(OUT)/HOL Nominal/ROOT.ML \ 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
22167
diff
changeset

1200 
Nominal/Nominal.thy \ 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
22167
diff
changeset

1201 
Nominal/nominal_atoms.ML \ 
31936  1202 
Nominal/nominal_datatype.ML \ 
22784
4637b69de71b
Added datatype_case.ML and nominal_fresh_fun.ML.
berghofe
parents:
22657
diff
changeset

1203 
Nominal/nominal_fresh_fun.ML \ 
22247  1204 
Nominal/nominal_induct.ML \ 
22314  1205 
Nominal/nominal_inductive.ML \ 
28652  1206 
Nominal/nominal_inductive2.ML \ 
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
22167
diff
changeset

1207 
Nominal/nominal_permeq.ML \ 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
22167
diff
changeset

1208 
Nominal/nominal_primrec.ML \ 
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
22167
diff
changeset

1209 
Nominal/nominal_thmdecls.ML \ 
21542  1210 
Library/Infinite_Set.thy 
28500  1211 
@cd Nominal; $(ISABELLE_TOOL) usedir b g true $(OUT)/HOL HOLNominal 
19497  1212 

1213 

1214 
## HOLNominalExamples 

1215 

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

1217 

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

1218 
$(LOG)/HOLNominalExamples.gz: $(OUT)/HOLNominal \ 
32636
55a0be42327c
added session theory for Bali and Nominal_Examples
haftmann
parents:
32632
diff
changeset

1219 
Nominal/Examples/Nominal_Examples.thy \ 
27163  1220 
Nominal/Examples/CK_Machine.thy \ 
22073
c170dcbe6c9d
formalisation of Crary's chapter on logical relations
urbanc
parents:
22067
diff
changeset

1221 
Nominal/Examples/CR.thy \ 
22821
15b2e7ec1f3b
alternative and much simpler proof for ChurchRosser of BetaReduction
urbanc
parents:
22819
diff
changeset

1222 
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

1223 
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

1224 
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

1225 
Nominal/Examples/Class3.thy \ 
22073
c170dcbe6c9d
formalisation of Crary's chapter on logical relations
urbanc
parents:
22067
diff
changeset

1226 
Nominal/Examples/Compile.thy \ 
25725  1227 
Nominal/Examples/Contexts.thy \ 
1228 
Nominal/Examples/Crary.thy \ 

22073
c170dcbe6c9d
formalisation of Crary's chapter on logical relations
urbanc
parents:
22067
diff
changeset

1229 
Nominal/Examples/Fsub.thy \ 
25725  1230 
Nominal/Examples/Height.thy \ 
1231 
Nominal/Examples/Lam_Funs.thy \ 

22073
c170dcbe6c9d
formalisation of Crary's chapter on logical relations
urbanc
parents:
22067
diff
changeset

1232 
Nominal/Examples/Lambda_mu.thy \ 
25725  1233 
Nominal/Examples/LocalWeakening.thy \ 
33189  1234 
Nominal/Examples/Pattern.thy \ 
25725  1235 
Nominal/Examples/ROOT.ML \ 
22073
c170dcbe6c9d
formalisation of Crary's chapter on logical relations
urbanc
parents:
22067
diff
changeset

1236 
Nominal/Examples/SN.thy \ 
23144  1237 
Nominal/Examples/SOS.thy \ 
27624
a925aa66e17a
Added Standardization theory to nominal examples.
berghofe
parents:
27484
diff
changeset

1238 
Nominal/Examples/Standardization.thy \ 
24896
70f238757695
added the two new examples from Nominal to the build process
urbanc
parents:
24830
diff
changeset

1239 
Nominal/Examples/Support.thy \ 
27032  1240 
Nominal/Examples/Type_Preservation.thy \ 
25725  1241 
Nominal/Examples/VC_Condition.thy \ 
26195  1242 
Nominal/Examples/W.thy \ 
25725  1243 
Nominal/Examples/Weakening.thy 
28500  1244 
@cd Nominal; $(ISABELLE_TOOL) usedir $(OUT)/HOLNominal Examples 
19497  1245 

1246 

24333  1247 
## HOLWord 
1248 

1249 
HOLWord: HOL $(OUT)/HOLWord 

1250 

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

1251 
$(OUT)/HOLWord: $(OUT)/HOL Word/ROOT.ML Library/Boolean_Algebra.thy \ 
37655  1252 
Library/Numeral_Type.thy Word/Misc_Numeric.thy Word/Misc_Typedef.thy \ 
37659  1253 
Word/Type_Length.thy Word/Bit_Representation.thy Word/Bit_Int.thy \ 
1254 
Word/Bool_List_Representation.thy Word/Bit_Operations.thy \ 

37660  1255 
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

1256 
Word/document/root.bib Word/Tools/smt_word.ML 
28500  1257 
@cd Word; $(ISABELLE_TOOL) usedir b g true $(OUT)/HOL HOLWord 
24333  1258 

1259 

24442  1260 
## HOLWordExamples 
1261 

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

1263 

27164  1264 
$(LOG)/HOLWordExamples.gz: $(OUT)/HOLWord Word/Examples/ROOT.ML \ 
24442  1265 
Word/Examples/WordExamples.thy 
28500  1266 
@cd Word; $(ISABELLE_TOOL) usedir $(OUT)/HOLWord Examples 
24442  1267 

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

1268 

25171  1269 
## HOLStatespace 
1270 

1271 
HOLStatespace: HOL $(LOG)/HOLStatespace.gz 

1272 

27164  1273 
$(LOG)/HOLStatespace.gz: $(OUT)/HOL Statespace/DistinctTreeProver.thy \ 
1274 
Statespace/StateFun.thy Statespace/StateSpaceLocale.thy \ 

1275 
Statespace/StateSpaceSyntax.thy Statespace/StateSpaceEx.thy \ 

1276 
Statespace/distinct_tree_prover.ML Statespace/state_space.ML \ 

1277 
Statespace/state_fun.ML Statespace/document/root.tex 

28500  1278 
@$(ISABELLE_TOOL) usedir g true $(OUT)/HOL Statespace 
24442  1279 

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

1280 

27470  1281 
## HOLNSA 
1282 

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

1283 
HOLNSA: HOL $(OUT)/HOLNSA 
27470  1284 
