| author | boehmes |
| Mon, 22 Nov 2010 15:45:42 +0100 | |
| changeset 40662 | 798aad2229c0 |
| parent 40650 | d40b347d5b0b |
| child 40676 | 23904fa13e03 |
| permissions | -rw-r--r-- |
|
36147
b43b22f63665
theory RBT with abstract type of red-black trees backed by implementation RBT_Impl
haftmann
parents:
36115
diff
changeset
|
1 |
|
| 2448 | 2 |
# |
3 |
# IsaMakefile for HOL |
|
4 |
# |
|
5 |
||
| 4518 | 6 |
## targets |
| 2448 | 7 |
|
| 4518 | 8 |
default: HOL |
| 27421 | 9 |
generate: HOL-Generate-HOL HOL-Generate-HOLLight |
|
33210
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset
|
10 |
|
|
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset
|
11 |
images: \ |
|
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset
|
12 |
HOL \ |
|
37691
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
13 |
HOL-Library \ |
|
33210
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset
|
14 |
HOL-Algebra \ |
| 33419 | 15 |
HOL-Boogie \ |
|
33210
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset
|
16 |
HOL-Multivariate_Analysis \ |
|
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset
|
17 |
HOL-NSA \ |
|
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset
|
18 |
HOL-Nominal \ |
| 35931 | 19 |
HOL-Probability \ |
|
34205
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
20 |
HOL-Proofs \ |
|
33210
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset
|
21 |
HOL-Word \ |
|
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset
|
22 |
HOL4 \ |
|
37691
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
23 |
TLA \ |
|
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
24 |
HOL-Base \ |
|
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
25 |
HOL-Main \ |
|
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
26 |
HOL-Plain |
| 10135 | 27 |
|
|
37691
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
28 |
#Note: keep targets sorted (except for HOL-ex) |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
29 |
test: \ |
| 24325 | 30 |
HOL-ex \ |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
31 |
HOL-Auth \ |
| 14031 | 32 |
HOL-Bali \ |
| 33439 | 33 |
HOL-Boogie-Examples \ |
|
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
34 |
HOL-Decision_Procs \ |
|
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset
|
35 |
HOL-Hahn_Banach \ |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
36 |
HOL-Hoare \ |
|
32621
a073cb249a06
theory entry point for session Hoare_Parallel (now also with proper underscore)
haftmann
parents:
32618
diff
changeset
|
37 |
HOL-Hoare_Parallel \ |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
38 |
HOL-IMP \ |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
39 |
HOL-IMPP \ |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
40 |
HOL-IOA \ |
|
29399
ebcd69a00872
split of Imperative_HOL theories from HOL-Library
haftmann
parents:
29197
diff
changeset
|
41 |
HOL-Imperative_HOL \ |
|
33210
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset
|
42 |
HOL-Import \ |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
43 |
HOL-Induct \ |
| 33026 | 44 |
HOL-Isar_Examples \ |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
45 |
HOL-Lattice \ |
| 37747 | 46 |
HOL-Library-Codegenerator_Test \ |
| 28637 | 47 |
HOL-Matrix \ |
| 33027 | 48 |
HOL-Metis_Examples \ |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
49 |
HOL-MicroJava \ |
| 32496 | 50 |
HOL-Mirabelle \ |
| 35536 | 51 |
HOL-Mutabelle \ |
| 11376 | 52 |
HOL-NanoJava \ |
|
33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset
|
53 |
HOL-Nitpick_Examples \ |
| 19497 | 54 |
HOL-Nominal-Examples \ |
| 32479 | 55 |
HOL-Number_Theory \ |
56 |
HOL-Old_Number_Theory \ |
|
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
57 |
HOL-Quotient_Examples \ |
|
35950
791ce568d40a
moved examples for the predicate compiler into its own session Predicate_Compile_Examples to slenderise the HOL-ex session
bulwahn
parents:
35931
diff
changeset
|
58 |
HOL-Predicate_Compile_Examples \ |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
59 |
HOL-Prolog \ |
|
39157
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
60 |
HOL-Proofs-ex \ |
|
34205
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
61 |
HOL-Proofs-Extraction \ |
|
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
62 |
HOL-Proofs-Lambda \ |
| 33028 | 63 |
HOL-SET_Protocol \ |
|
36933
705b58fde476
more precise dependencies for HOL-Word-SMT_Examples;
wenzelm
parents:
36916
diff
changeset
|
64 |
HOL-Word-SMT_Examples \ |
| 25171 | 65 |
HOL-Statespace \ |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
66 |
HOL-Subst \ |
|
33210
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset
|
67 |
TLA-Buffer \ |
|
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset
|
68 |
TLA-Inc \ |
|
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset
|
69 |
TLA-Memory \ |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
70 |
HOL-UNITY \ |
| 10966 | 71 |
HOL-Unix \ |
| 24442 | 72 |
HOL-Word-Examples \ |
| 24325 | 73 |
HOL-ZF |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
74 |
# ^ this is the sort position |
| 10614 | 75 |
|
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
76 |
all: test images |
| 4518 | 77 |
|
78 |
||
79 |
## global settings |
|
80 |
||
81 |
SRC = $(ISABELLE_HOME)/src |
|
| 3118 | 82 |
OUT = $(ISABELLE_OUTPUT) |
| 4447 | 83 |
LOG = $(OUT)/log |
| 2448 | 84 |
|
| 4518 | 85 |
|
86 |
## HOL |
|
| 2448 | 87 |
|
| 28393 | 88 |
HOL: Pure $(OUT)/HOL |
| 27368 | 89 |
|
| 29505 | 90 |
HOL-Base: Pure $(OUT)/HOL-Base |
91 |
||
| 27368 | 92 |
HOL-Plain: Pure $(OUT)/HOL-Plain |
| 4518 | 93 |
|
| 28401 | 94 |
HOL-Main: Pure $(OUT)/HOL-Main |
95 |
||
| 4518 | 96 |
Pure: |
| 28500 | 97 |
@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
|
98 |
|
| 27694 | 99 |
$(OUT)/Pure: Pure |
100 |
||
| 36073 | 101 |
BASE_DEPENDENCIES = $(OUT)/Pure \ |
|
30160
5f7b17941730
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset
|
102 |
$(SRC)/Provers/blast.ML \ |
|
5f7b17941730
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset
|
103 |
$(SRC)/Provers/clasimp.ML \ |
|
5f7b17941730
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset
|
104 |
$(SRC)/Provers/classical.ML \ |
|
5f7b17941730
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset
|
105 |
$(SRC)/Provers/hypsubst.ML \ |
|
5f7b17941730
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset
|
106 |
$(SRC)/Provers/quantifier1.ML \ |
|
5f7b17941730
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset
|
107 |
$(SRC)/Provers/splitter.ML \ |
|
37818
dd65033fed78
load cache_io before code generator; moved adhoc-overloading to generic tools
haftmann
parents:
37790
diff
changeset
|
108 |
$(SRC)/Tools/cache_io.ML \ |
| 31771 | 109 |
$(SRC)/Tools/Code/code_haskell.ML \ |
110 |
$(SRC)/Tools/Code/code_ml.ML \ |
|
|
38970
53d1ee3d98b8
factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
38965
diff
changeset
|
111 |
$(SRC)/Tools/Code/code_namespace.ML \ |
| 31771 | 112 |
$(SRC)/Tools/Code/code_preproc.ML \ |
113 |
$(SRC)/Tools/Code/code_printer.ML \ |
|
| 39402 | 114 |
$(SRC)/Tools/Code/code_runtime.ML \ |
| 34945 | 115 |
$(SRC)/Tools/Code/code_scala.ML \ |
| 37442 | 116 |
$(SRC)/Tools/Code/code_simp.ML \ |
| 31771 | 117 |
$(SRC)/Tools/Code/code_target.ML \ |
118 |
$(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
|
119 |
$(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
|
120 |
$(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
|
121 |
$(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
|
122 |
$(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
|
123 |
$(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
|
124 |
$(SRC)/Tools/atomize_elim.ML \ |
|
39323
ce5c6a8b0359
start renaming "Auto_Counterexample" to "Auto_Tools";
blanchet
parents:
39271
diff
changeset
|
125 |
$(SRC)/Tools/auto_tools.ML \ |
|
30160
5f7b17941730
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset
|
126 |
$(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
|
127 |
$(SRC)/Tools/cong_tac.ML \ |
|
30160
5f7b17941730
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset
|
128 |
$(SRC)/Tools/eqsubst.ML \ |
|
5f7b17941730
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset
|
129 |
$(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
|
130 |
$(SRC)/Tools/induct_tacs.ML \ |
|
30165
6ee87f67d9cd
moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
30160
diff
changeset
|
131 |
$(SRC)/Tools/intuitionistic.ML \ |
|
37781
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
37779
diff
changeset
|
132 |
$(SRC)/Tools/misc_legacy.ML \ |
|
30160
5f7b17941730
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset
|
133 |
$(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
|
134 |
$(SRC)/Tools/project_rule.ML \ |
|
30973
304ab57afa6e
observe distinction between Pure/Tools and Tools more closely
haftmann
parents:
30954
diff
changeset
|
135 |
$(SRC)/Tools/quickcheck.ML \ |
|
40116
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
40067
diff
changeset
|
136 |
$(SRC)/Tools/solve_direct.ML \ |
|
30160
5f7b17941730
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset
|
137 |
$(SRC)/Tools/value.ML \ |
| 29505 | 138 |
HOL.thy \ |
| 40582 | 139 |
Tools/functorial_mappers.ML \ |
| 29505 | 140 |
Tools/hologic.ML \ |
141 |
Tools/recfun_codegen.ML \ |
|
| 36073 | 142 |
Tools/simpdata.ML |
| 29505 | 143 |
|
144 |
$(OUT)/HOL-Base: base.ML $(BASE_DEPENDENCIES) |
|
| 29523 | 145 |
@$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base |
| 29505 | 146 |
|
|
39157
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
147 |
PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES) \ |
| 32139 | 148 |
Complete_Lattice.thy \ |
| 40108 | 149 |
Complete_Partial_Order.thy \ |
| 27368 | 150 |
Datatype.thy \ |
151 |
Extraction.thy \ |
|
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35039
diff
changeset
|
152 |
Fields.thy \ |
| 27368 | 153 |
Finite_Set.thy \ |
154 |
Fun.thy \ |
|
155 |
FunDef.thy \ |
|
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35039
diff
changeset
|
156 |
Groups.thy \ |
| 27368 | 157 |
Inductive.thy \ |
158 |
Lattices.thy \ |
|
| 39945 | 159 |
Meson.thy \ |
| 39946 | 160 |
Metis.thy \ |
| 27368 | 161 |
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
|
162 |
Option.thy \ |
| 27368 | 163 |
Orderings.thy \ |
| 40108 | 164 |
Partial_Function.thy \ |
| 27368 | 165 |
Plain.thy \ |
166 |
Power.thy \ |
|
167 |
Predicate.thy \ |
|
168 |
Product_Type.thy \ |
|
169 |
Relation.thy \ |
|
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35039
diff
changeset
|
170 |
Rings.thy \ |
| 27368 | 171 |
SAT.thy \ |
172 |
Set.thy \ |
|
173 |
Sum_Type.thy \ |
|
|
37884
314a88278715
discontinued pretending that abel_cancel is logic-independent; cleaned up junk
haftmann
parents:
37818
diff
changeset
|
174 |
Tools/abel_cancel.ML \ |
|
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset
|
175 |
Tools/arith_data.ML \ |
|
40345
129d31b162f3
moved file in makefile to reflect actual dependencies
blanchet
parents:
40281
diff
changeset
|
176 |
Tools/async_manager.ML \ |
| 27368 | 177 |
Tools/cnf_funcs.ML \ |
| 31771 | 178 |
Tools/Datatype/datatype_abs_proofs.ML \ |
179 |
Tools/Datatype/datatype_aux.ML \ |
|
180 |
Tools/Datatype/datatype_case.ML \ |
|
181 |
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
|
182 |
Tools/Datatype/datatype_data.ML \ |
| 31771 | 183 |
Tools/Datatype/datatype_prop.ML \ |
184 |
Tools/Datatype/datatype_realizer.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
|
185 |
Tools/Datatype/datatype.ML \ |
| 27368 | 186 |
Tools/dseq.ML \ |
| 31771 | 187 |
Tools/Function/context_tree.ML \ |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
33098
diff
changeset
|
188 |
Tools/Function/function_common.ML \ |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
33098
diff
changeset
|
189 |
Tools/Function/function_core.ML \ |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
33098
diff
changeset
|
190 |
Tools/Function/function_lib.ML \ |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
33098
diff
changeset
|
191 |
Tools/Function/function.ML \ |
| 33098 | 192 |
Tools/Function/fun.ML \ |
| 33471 | 193 |
Tools/Function/induction_schema.ML \ |
| 31771 | 194 |
Tools/Function/lexicographic_order.ML \ |
195 |
Tools/Function/measure_functions.ML \ |
|
196 |
Tools/Function/mutual.ML \ |
|
| 40108 | 197 |
Tools/Function/partial_function.ML \ |
| 33083 | 198 |
Tools/Function/pat_completeness.ML \ |
| 31771 | 199 |
Tools/Function/pattern_split.ML \ |
| 33100 | 200 |
Tools/Function/relation.ML \ |
| 31771 | 201 |
Tools/Function/scnp_reconstruct.ML \ |
202 |
Tools/Function/scnp_solve.ML \ |
|
203 |
Tools/Function/size.ML \ |
|
204 |
Tools/Function/sum_tree.ML \ |
|
205 |
Tools/Function/termination.ML \ |
|
| 27368 | 206 |
Tools/inductive_codegen.ML \ |
|
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31706
diff
changeset
|
207 |
Tools/inductive.ML \ |
| 27368 | 208 |
Tools/inductive_realizer.ML \ |
|
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31706
diff
changeset
|
209 |
Tools/inductive_set.ML \ |
| 27368 | 210 |
Tools/lin_arith.ML \ |
| 39940 | 211 |
Tools/Meson/meson.ML \ |
212 |
Tools/Meson/meson_clausify.ML \ |
|
| 39948 | 213 |
Tools/Meson/meson_tactic.ML \ |
| 39946 | 214 |
Tools/Metis/metis_reconstruct.ML \ |
215 |
Tools/Metis/metis_translate.ML \ |
|
216 |
Tools/Metis/metis_tactics.ML \ |
|
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
30457
diff
changeset
|
217 |
Tools/nat_arith.ML \ |
|
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31706
diff
changeset
|
218 |
Tools/primrec.ML \ |
| 27368 | 219 |
Tools/prop_logic.ML \ |
220 |
Tools/refute.ML \ |
|
221 |
Tools/rewrite_hol_proof.ML \ |
|
222 |
Tools/sat_funcs.ML \ |
|
223 |
Tools/sat_solver.ML \ |
|
224 |
Tools/split_rule.ML \ |
|
|
38942
e10c11971fa7
"try" -- a new diagnosis tool that tries to apply several methods in parallel
blanchet
parents:
38730
diff
changeset
|
225 |
Tools/try.ML \ |
|
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31706
diff
changeset
|
226 |
Tools/typedef.ML \ |
| 27368 | 227 |
Transitive_Closure.thy \ |
228 |
Typedef.thy \ |
|
229 |
Wellfounded.thy \ |
|
230 |
$(SRC)/Provers/Arith/cancel_div_mod.ML \ |
|
231 |
$(SRC)/Provers/Arith/cancel_sums.ML \ |
|
232 |
$(SRC)/Provers/Arith/fast_lin_arith.ML \ |
|
233 |
$(SRC)/Provers/order.ML \ |
|
234 |
$(SRC)/Provers/trancl.ML \ |
|
| 39946 | 235 |
$(SRC)/Tools/Metis/metis.ML \ |
| 27368 | 236 |
$(SRC)/Tools/rat.ML |
|
28312
f0838044f034
different session branches for HOL-Plain vs. Plain
haftmann
parents:
28243
diff
changeset
|
237 |
|
|
f0838044f034
different session branches for HOL-Plain vs. Plain
haftmann
parents:
28243
diff
changeset
|
238 |
$(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES) |
| 28500 | 239 |
@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain |
| 27368 | 240 |
|
| 28401 | 241 |
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
|
242 |
ATP.thy \ |
|
35725
4d7e3cc9c52c
Big_Operators now in Main rather than Plain src/HOL/Wellfounded.thy
haftmann
parents:
35719
diff
changeset
|
243 |
Big_Operators.thy \ |
| 32657 | 244 |
Code_Evaluation.thy \ |
|
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
245 |
Code_Numeral.thy \ |
|
33296
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
33272
diff
changeset
|
246 |
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
|
247 |
DSequence.thy \ |
| 27368 | 248 |
Equiv_Relations.thy \ |
|
40650
d40b347d5b0b
adding Enum to HOL-Main image and removing it from HOL-Library
bulwahn
parents:
40634
diff
changeset
|
249 |
Enum.thy \ |
| 27368 | 250 |
Groebner_Basis.thy \ |
251 |
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
|
252 |
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
|
253 |
Lazy_Sequence.thy \ |
| 27421 | 254 |
List.thy \ |
255 |
Main.thy \ |
|
256 |
Map.thy \ |
|
| 30925 | 257 |
Nat_Numeral.thy \ |
|
33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33298
diff
changeset
|
258 |
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
|
259 |
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
|
260 |
New_Random_Sequence.thy \ |
|
36915
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
261 |
Nitpick.thy \ |
|
33356
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
33348
diff
changeset
|
262 |
Numeral_Simprocs.thy \ |
| 27421 | 263 |
Presburger.thy \ |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33210
diff
changeset
|
264 |
Predicate_Compile.thy \ |
|
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31186
diff
changeset
|
265 |
Quickcheck.thy \ |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
266 |
Quotient.thy \ |
|
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31186
diff
changeset
|
267 |
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
|
268 |
Random_Sequence.thy \ |
| 27421 | 269 |
Recdef.thy \ |
| 39271 | 270 |
Record.thy \ |
| 36916 | 271 |
Refute.thy \ |
|
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36700
diff
changeset
|
272 |
Semiring_Normalization.thy \ |
| 27421 | 273 |
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
|
274 |
Sledgehammer.thy \ |
|
40420
552563ea3304
adding code and theory for smallvalue generators, but do not setup the interpretation yet
bulwahn
parents:
40355
diff
changeset
|
275 |
Smallcheck.thy \ |
| 36898 | 276 |
SMT.thy \ |
|
31048
ac146fc38b51
refined HOL string theories and corresponding ML fragments
haftmann
parents:
31036
diff
changeset
|
277 |
String.thy \ |
|
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31186
diff
changeset
|
278 |
Typerep.thy \ |
| 27421 | 279 |
$(SRC)/Provers/Arith/assoc_fold.ML \ |
280 |
$(SRC)/Provers/Arith/cancel_numeral_factor.ML \ |
|
281 |
$(SRC)/Provers/Arith/cancel_numerals.ML \ |
|
282 |
$(SRC)/Provers/Arith/combine_numerals.ML \ |
|
283 |
$(SRC)/Provers/Arith/extract_common_term.ML \ |
|
| 38047 | 284 |
Tools/ATP/atp_problem.ML \ |
| 39452 | 285 |
Tools/ATP/atp_proof.ML \ |
| 38047 | 286 |
Tools/ATP/atp_systems.ML \ |
|
33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33298
diff
changeset
|
287 |
Tools/choice_specification.ML \ |
| 39564 | 288 |
Tools/code_evaluation.ML \ |
|
39483
9f0e5684f04b
add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents:
39452
diff
changeset
|
289 |
Tools/Datatype/datatype_selectors.ML \ |
|
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31060
diff
changeset
|
290 |
Tools/int_arith.ML \ |
|
36753
5cf4e9128f22
renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents:
36751
diff
changeset
|
291 |
Tools/groebner.ML \ |
|
31055
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
31048
diff
changeset
|
292 |
Tools/list_code.ML \ |
|
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31060
diff
changeset
|
293 |
Tools/nat_numeral_simprocs.ML \ |
|
36915
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
294 |
Tools/Nitpick/kodkod.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
295 |
Tools/Nitpick/kodkod_sat.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
296 |
Tools/Nitpick/nitpick.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
297 |
Tools/Nitpick/nitpick_hol.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
298 |
Tools/Nitpick/nitpick_isar.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
299 |
Tools/Nitpick/nitpick_kodkod.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
300 |
Tools/Nitpick/nitpick_model.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
301 |
Tools/Nitpick/nitpick_mono.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
302 |
Tools/Nitpick/nitpick_nut.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
303 |
Tools/Nitpick/nitpick_peephole.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
304 |
Tools/Nitpick/nitpick_preproc.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
305 |
Tools/Nitpick/nitpick_rep.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
306 |
Tools/Nitpick/nitpick_scope.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
307 |
Tools/Nitpick/nitpick_tests.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
308 |
Tools/Nitpick/nitpick_util.ML \ |
| 27421 | 309 |
Tools/numeral.ML \ |
|
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31060
diff
changeset
|
310 |
Tools/numeral_simprocs.ML \ |
| 27421 | 311 |
Tools/numeral_syntax.ML \ |
|
40141
0e8a4e27a685
adding new predicate compiler files to the IsaMakefile
bulwahn
parents:
40123
diff
changeset
|
312 |
Tools/Predicate_Compile/core_data.ML \ |
|
0e8a4e27a685
adding new predicate compiler files to the IsaMakefile
bulwahn
parents:
40123
diff
changeset
|
313 |
Tools/Predicate_Compile/mode_inference.ML \ |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33210
diff
changeset
|
314 |
Tools/Predicate_Compile/predicate_compile_aux.ML \ |
|
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
36032
diff
changeset
|
315 |
Tools/Predicate_Compile/predicate_compile_compilations.ML \ |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33210
diff
changeset
|
316 |
Tools/Predicate_Compile/predicate_compile_core.ML \ |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33210
diff
changeset
|
317 |
Tools/Predicate_Compile/predicate_compile_data.ML \ |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33210
diff
changeset
|
318 |
Tools/Predicate_Compile/predicate_compile_fun.ML \ |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33210
diff
changeset
|
319 |
Tools/Predicate_Compile/predicate_compile.ML \ |
|
40141
0e8a4e27a685
adding new predicate compiler files to the IsaMakefile
bulwahn
parents:
40123
diff
changeset
|
320 |
Tools/Predicate_Compile/predicate_compile_proof.ML \ |
|
36032
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
35972
diff
changeset
|
321 |
Tools/Predicate_Compile/predicate_compile_specialisation.ML \ |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33210
diff
changeset
|
322 |
Tools/Predicate_Compile/predicate_compile_pred.ML \ |
| 31260 | 323 |
Tools/quickcheck_generators.ML \ |
| 27421 | 324 |
Tools/Qelim/cooper.ML \ |
| 36803 | 325 |
Tools/Qelim/cooper_procedure.ML \ |
| 27421 | 326 |
Tools/Qelim/qelim.ML \ |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
327 |
Tools/Quotient/quotient_def.ML \ |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
328 |
Tools/Quotient/quotient_info.ML \ |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
329 |
Tools/Quotient/quotient_tacs.ML \ |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
330 |
Tools/Quotient/quotient_term.ML \ |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
331 |
Tools/Quotient/quotient_typ.ML \ |
|
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31706
diff
changeset
|
332 |
Tools/recdef.ML \ |
|
38394
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
38282
diff
changeset
|
333 |
Tools/record.ML \ |
|
36753
5cf4e9128f22
renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents:
36751
diff
changeset
|
334 |
Tools/semiring_normalizer.ML \ |
|
38021
e024504943d1
rename "ATP_Manager" ML module to "Sledgehammer";
blanchet
parents:
38019
diff
changeset
|
335 |
Tools/Sledgehammer/sledgehammer.ML \ |
| 38986 | 336 |
Tools/Sledgehammer/sledgehammer_filter.ML \ |
337 |
Tools/Sledgehammer/sledgehammer_minimize.ML \ |
|
|
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
338 |
Tools/Sledgehammer/sledgehammer_isar.ML \ |
| 40067 | 339 |
Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML \ |
340 |
Tools/Sledgehammer/sledgehammer_atp_translate.ML \ |
|
| 35967 | 341 |
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
|
342 |
Tools/smallvalue_generators.ML \ |
| 36898 | 343 |
Tools/SMT/smtlib_interface.ML \ |
| 40277 | 344 |
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
|
345 |
Tools/SMT/smt_config.ML \ |
|
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
|
346 |
Tools/SMT/smt_failure.ML \ |
| 36898 | 347 |
Tools/SMT/smt_monomorph.ML \ |
348 |
Tools/SMT/smt_normalize.ML \ |
|
|
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40141
diff
changeset
|
349 |
Tools/SMT/smt_setup_solvers.ML \ |
| 36898 | 350 |
Tools/SMT/smt_solver.ML \ |
351 |
Tools/SMT/smt_translate.ML \ |
|
|
40662
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40650
diff
changeset
|
352 |
Tools/SMT/smt_utils.ML \ |
| 36898 | 353 |
Tools/SMT/z3_interface.ML \ |
354 |
Tools/SMT/z3_model.ML \ |
|
355 |
Tools/SMT/z3_proof_literals.ML \ |
|
|
40662
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40650
diff
changeset
|
356 |
Tools/SMT/z3_proof_methods.ML \ |
| 36898 | 357 |
Tools/SMT/z3_proof_parser.ML \ |
358 |
Tools/SMT/z3_proof_reconstruction.ML \ |
|
359 |
Tools/SMT/z3_proof_tools.ML \ |
|
|
31055
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
31048
diff
changeset
|
360 |
Tools/string_code.ML \ |
| 27421 | 361 |
Tools/string_syntax.ML \ |
|
33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33298
diff
changeset
|
362 |
Tools/transfer.ML \ |
| 27421 | 363 |
Tools/TFL/casesplit.ML \ |
364 |
Tools/TFL/dcterm.ML \ |
|
365 |
Tools/TFL/post.ML \ |
|
366 |
Tools/TFL/rules.ML \ |
|
367 |
Tools/TFL/tfl.ML \ |
|
368 |
Tools/TFL/thms.ML \ |
|
369 |
Tools/TFL/thry.ML \ |
|
370 |
Tools/TFL/usyntax.ML \ |
|
|
28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
28476
diff
changeset
|
371 |
Tools/TFL/utils.ML |
| 28401 | 372 |
|
373 |
$(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES) |
|
| 28500 | 374 |
@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main |
| 28401 | 375 |
|
|
34205
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
376 |
HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \ |
| 30096 | 377 |
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
|
378 |
Complex.thy \ |
|
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset
|
379 |
Complex_Main.thy \ |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset
|
380 |
Deriv.thy \ |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset
|
381 |
Fact.thy \ |
| 32479 | 382 |
GCD.thy \ |
|
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset
|
383 |
Lim.thy \ |
| 31352 | 384 |
Limits.thy \ |
|
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset
|
385 |
Ln.thy \ |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset
|
386 |
Log.thy \ |
| 32479 | 387 |
Lubs.thy \ |
|
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset
|
388 |
MacLaurin.thy \ |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset
|
389 |
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
|
390 |
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
|
391 |
RComplete.thy \ |
| 35372 | 392 |
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
|
393 |
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
|
394 |
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
|
395 |
RealVector.thy \ |
|
29197
6d4cb27ed19c
adapted HOL source structure to distribution layout
haftmann
parents:
29181
diff
changeset
|
396 |
SEQ.thy \ |
|
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset
|
397 |
Series.thy \ |
|
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
33083
diff
changeset
|
398 |
SupInf.thy \ |
|
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset
|
399 |
Taylor.thy \ |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset
|
400 |
Transcendental.thy \ |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset
|
401 |
Tools/float_syntax.ML \ |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
402 |
Tools/SMT/smt_real.ML |
|
34205
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
403 |
|
|
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
404 |
$(OUT)/HOL: ROOT.ML $(HOL_DEPENDENCIES) |
|
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
405 |
@$(ISABELLE_TOOL) usedir -b -g true $(OUT)/Pure HOL |
|
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
406 |
|
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
7513
diff
changeset
|
407 |
|
| 10255 | 408 |
## HOL-Library |
409 |
||
|
37691
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
410 |
HOL-Library: HOL $(OUT)/HOL-Library |
| 10255 | 411 |
|
|
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
|
412 |
$(OUT)/HOL-Library: $(OUT)/HOL Library/ROOT.ML \ |
|
37691
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
413 |
$(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML \ |
|
37818
dd65033fed78
load cache_io before code generator; moved adhoc-overloading to generic tools
haftmann
parents:
37790
diff
changeset
|
414 |
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
|
415 |
Library/AssocList.thy Library/BigO.thy Library/Binomial.thy \ |
| 37968 | 416 |
Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy \ |
| 37662 | 417 |
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
|
418 |
Library/Code_Integer.thy Library/Code_Natural.thy \ |
|
38119
e00f970425e9
adding Code_Prolog theory to IsaMakefile and HOL-Library root file
bulwahn
parents:
38074
diff
changeset
|
419 |
Library/Code_Prolog.thy Tools/Predicate_Compile/code_prolog.ML \ |
| 37968 | 420 |
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
|
421 |
Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy \ |
|
40650
d40b347d5b0b
adding Enum to HOL-Main image and removing it from HOL-Library
bulwahn
parents:
40634
diff
changeset
|
422 |
Library/Efficient_Nat.thy Library/Eval_Witness.thy \ |
| 37968 | 423 |
Library/Executable_Set.thy Library/Float.thy \ |
424 |
Library/Formal_Power_Series.thy Library/Fraction_Field.thy \ |
|
425 |
Library/FrechetDeriv.thy Library/Fset.thy Library/FuncSet.thy \ |
|
| 38622 | 426 |
Library/Function_Algebras.thy \ |
| 37968 | 427 |
Library/Fundamental_Theorem_Algebra.thy Library/Glbs.thy \ |
428 |
Library/Indicator_Function.thy Library/Infinite_Set.thy \ |
|
429 |
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
|
430 |
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
|
431 |
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
|
432 |
Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy \ |
| 37790 | 433 |
Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy \ |
|
37818
dd65033fed78
load cache_io before code generator; moved adhoc-overloading to generic tools
haftmann
parents:
37790
diff
changeset
|
434 |
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
|
435 |
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
|
436 |
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
|
437 |
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
|
438 |
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
|
439 |
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
|
440 |
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
|
441 |
Library/Product_ord.thy Library/Product_plus.thy \ |
| 40349 | 442 |
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
|
443 |
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
|
444 |
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
|
445 |
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
|
446 |
Library/RBT.thy Library/RBT_Impl.thy Library/README.html \ |
| 38622 | 447 |
Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy \ |
448 |
Library/Reflection.thy Library/SML_Quickcheck.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
|
449 |
Library/Sublist_Order.thy Library/Sum_Of_Squares.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
|
450 |
Library/Sum_Of_Squares/sos_wrapper.ML \ |
|
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
|
451 |
Library/Sum_Of_Squares/sum_of_squares.ML \ |
|
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
|
452 |
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
|
453 |
Library/While_Combinator.thy Library/Zorn.thy \ |
|
37818
dd65033fed78
load cache_io before code generator; moved adhoc-overloading to generic tools
haftmann
parents:
37790
diff
changeset
|
454 |
$(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML \ |
| 37789 | 455 |
Library/reflection.ML Library/reify_data.ML \ |
|
37691
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
456 |
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
|
457 |
@cd Library; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL-Library |
| 10255 | 458 |
|
459 |
||
|
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset
|
460 |
## HOL-Hahn_Banach |
| 27421 | 461 |
|
|
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset
|
462 |
HOL-Hahn_Banach: HOL $(LOG)/HOL-Hahn_Banach.gz |
| 27421 | 463 |
|
|
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset
|
464 |
$(LOG)/HOL-Hahn_Banach.gz: $(OUT)/HOL Hahn_Banach/Bounds.thy \ |
|
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset
|
465 |
Hahn_Banach/Function_Norm.thy Hahn_Banach/Function_Order.thy \ |
|
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset
|
466 |
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
|
467 |
Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Hahn_Banach/Linearform.thy \ |
|
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset
|
468 |
Hahn_Banach/Normed_Space.thy Hahn_Banach/README.html \ |
|
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset
|
469 |
Hahn_Banach/ROOT.ML Hahn_Banach/Subspace.thy \ |
|
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset
|
470 |
Hahn_Banach/Vector_Space.thy Hahn_Banach/Zorn_Lemma.thy \ |
|
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset
|
471 |
Hahn_Banach/document/root.bib Hahn_Banach/document/root.tex |
|
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset
|
472 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hahn_Banach |
| 27421 | 473 |
|
474 |
||
| 4518 | 475 |
## HOL-Subst |
476 |
||
477 |
HOL-Subst: HOL $(LOG)/HOL-Subst.gz |
|
478 |
||
| 27164 | 479 |
$(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.thy Subst/ROOT.ML \ |
480 |
Subst/Subst.thy Subst/UTerm.thy Subst/Unifier.thy Subst/Unify.thy |
|
| 28500 | 481 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Subst |
| 2448 | 482 |
|
483 |
||
| 4518 | 484 |
## HOL-Induct |
| 2473 | 485 |
|
| 4518 | 486 |
HOL-Induct: HOL $(LOG)/HOL-Induct.gz |
| 3125 | 487 |
|
|
33688
1a97dcd8dc6a
moved old SList, LList, LFilter to AFP/Lazy-Lists-II;
wenzelm
parents:
33649
diff
changeset
|
488 |
$(LOG)/HOL-Induct.gz: $(OUT)/HOL Induct/Com.thy Induct/Comb.thy \ |
|
1a97dcd8dc6a
moved old SList, LList, LFilter to AFP/Lazy-Lists-II;
wenzelm
parents:
33649
diff
changeset
|
489 |
Induct/Ordinals.thy Induct/PropLog.thy Induct/QuoNestedDataType.thy \ |
|
1a97dcd8dc6a
moved old SList, LList, LFilter to AFP/Lazy-Lists-II;
wenzelm
parents:
33649
diff
changeset
|
490 |
Induct/QuoDataType.thy Induct/ROOT.ML Induct/Sexp.thy \ |
| 35249 | 491 |
Induct/Sigma_Algebra.thy Induct/ABexp.thy Induct/SList.thy \ |
492 |
Induct/Term.thy Induct/Tree.thy Induct/document/root.tex |
|
| 28500 | 493 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Induct |
| 3125 | 494 |
|
495 |
||
| 4518 | 496 |
## HOL-IMP |
497 |
||
498 |
HOL-IMP: HOL $(LOG)/HOL-IMP.gz |
|
| 2448 | 499 |
|
| 27164 | 500 |
$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Compiler0.thy \ |
501 |
IMP/Compiler.thy IMP/Denotation.thy IMP/Expr.thy IMP/Hoare.thy \ |
|
502 |
IMP/Natural.thy IMP/Examples.thy IMP/Transition.thy IMP/VC.thy \ |
|
503 |
IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib |
|
| 28500 | 504 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL IMP |
| 2448 | 505 |
|
506 |
||
| 8179 | 507 |
## HOL-IMPP |
508 |
||
509 |
HOL-IMPP: HOL $(LOG)/HOL-IMPP.gz |
|
510 |
||
| 27164 | 511 |
$(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy \ |
| 19803 | 512 |
IMPP/Natural.thy IMPP/Hoare.thy IMPP/Misc.thy IMPP/EvenOdd.thy |
| 28500 | 513 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL IMPP |
| 8179 | 514 |
|
515 |
||
| 27421 | 516 |
## HOL-Import |
| 14516 | 517 |
|
| 19097 | 518 |
IMPORTER_FILES = Import/lazy_seq.ML Import/proof_kernel.ML Import/replay.ML \ |
| 20610 | 519 |
Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \ |
| 14516 | 520 |
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
|
521 |
Import/hol4rews.ML Import/import.ML Import/ROOT.ML |
| 14516 | 522 |
|
| 17323 | 523 |
IMPORTER_HOLLIGHT_FILES = Import/proof_kernel.ML Import/replay.ML \ |
524 |
Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \ |
|
525 |
Import/HOL4Syntax.thy Import/HOLLightCompat.thy Import/import_syntax.ML \ |
|
| 31771 | 526 |
Import/hol4rews.ML Import/import.ML Import/ROOT.ML |
| 17323 | 527 |
|
| 27421 | 528 |
HOL-Import: HOL $(LOG)/HOL-Import.gz |
| 14516 | 529 |
|
| 27421 | 530 |
$(LOG)/HOL-Import.gz: $(OUT)/HOL $(IMPORTER_FILES) |
| 37296 | 531 |
@$(ISABELLE_TOOL) usedir -p 0 $(OUT)/HOL Import |
| 14516 | 532 |
|
533 |
||
| 27421 | 534 |
## HOL-Generate-HOL |
| 14516 | 535 |
|
| 27421 | 536 |
HOL-Generate-HOL: HOL $(LOG)/HOL-Generate-HOL.gz |
| 14516 | 537 |
|
| 27421 | 538 |
$(LOG)/HOL-Generate-HOL.gz: $(OUT)/HOL \ |
| 27164 | 539 |
$(IMPORTER_FILES) Import/Generate-HOL/GenHOL4Base.thy \ |
540 |
Import/Generate-HOL/GenHOL4Prob.thy \ |
|
541 |
Import/Generate-HOL/GenHOL4Real.thy \ |
|
542 |
Import/Generate-HOL/GenHOL4Vec.thy \ |
|
| 14516 | 543 |
Import/Generate-HOL/GenHOL4Word32.thy Import/Generate-HOL/ROOT.ML |
| 28500 | 544 |
@cd Import; $(ISABELLE_TOOL) usedir $(OUT)/HOL Generate-HOL |
| 14516 | 545 |
|
| 17460 | 546 |
|
| 27421 | 547 |
## HOL-Generate-HOLLight |
| 17460 | 548 |
|
| 27421 | 549 |
HOL-Generate-HOLLight: HOL $(LOG)/HOL-Generate-HOLLight.gz |
| 17323 | 550 |
|
| 37742 | 551 |
$(LOG)/HOL-Generate-HOLLight.gz: $(OUT)/HOL \ |
| 27164 | 552 |
$(IMPORTER_HOLLIGHT_FILES) Import/Generate-HOLLight/GenHOLLight.thy \ |
553 |
Import/Generate-HOLLight/ROOT.ML |
|
| 28500 | 554 |
@cd Import; $(ISABELLE_TOOL) usedir $(OUT)/HOL Generate-HOLLight |
| 14516 | 555 |
|
| 17460 | 556 |
|
| 14516 | 557 |
## HOL-Import-HOL |
558 |
||
| 27421 | 559 |
HOL4: HOL $(LOG)/HOL4.gz |
| 14516 | 560 |
|
561 |
HOL_IMPORT_FILES = arithmetic.imp bits.imp boolean_sequence.imp bool.imp \ |
|
562 |
bword_arith.imp bword_bitop.imp bword_num.imp combin.imp divides.imp \ |
|
563 |
hrat.imp hreal.imp ind_type.imp lim.imp list.imp marker.imp nets.imp \ |
|
564 |
numeral.imp num.imp one.imp operator.imp option.imp pair.imp poly.imp \ |
|
565 |
powser.imp pred_set.imp prime.imp prim_rec.imp prob_algebra.imp \ |
|
566 |
prob_canon.imp prob_extra.imp prob.imp prob_indep.imp prob_pseudo.imp \ |
|
| 23194 | 567 |
prob_uniform.imp realax.imp real.imp relation.imp res_quan.imp \ |
568 |
rich_list.imp \ |
|
| 14516 | 569 |
seq.imp state_transformer.imp sum.imp topology.imp transc.imp word32.imp \ |
570 |
word_base.imp word_bitop.imp word_num.imp |
|
571 |
||
| 37742 | 572 |
$(LOG)/HOL4.gz: $(OUT)/HOL $(IMPORTER_FILES) \ |
| 27164 | 573 |
$(HOL_IMPORT_FILES:%=Import/HOL/%) Import/HOL/HOL4Base.thy \ |
574 |
Import/HOL/HOL4Prob.thy Import/HOL/HOL4Real.thy \ |
|
575 |
Import/HOL/HOL4Vec.thy Import/HOL/HOL4Word32.thy Import/HOL/HOL4.thy \ |
|
576 |
Import/HOL/ROOT.ML |
|
| 28500 | 577 |
@cd Import/HOL; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL4 |
| 14516 | 578 |
|
| 27421 | 579 |
HOLLight: HOL $(LOG)/HOLLight.gz |
| 17645 | 580 |
|
| 37742 | 581 |
$(LOG)/HOLLight.gz: $(OUT)/HOL $(IMPORTER_HOLLIGHT_FILES) \ |
| 27164 | 582 |
Import/HOLLight/hollight.imp Import/HOLLight/HOLLight.thy \ |
| 17645 | 583 |
Import/HOLLight/ROOT.ML |
| 28500 | 584 |
@cd Import/HOLLight; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOLLight |
| 17645 | 585 |
|
| 14516 | 586 |
|
| 32479 | 587 |
## HOL-Number_Theory |
| 31719 | 588 |
|
| 32479 | 589 |
HOL-Number_Theory: HOL $(LOG)/HOL-Number_Theory.gz |
| 31719 | 590 |
|
| 32479 | 591 |
$(LOG)/HOL-Number_Theory.gz: $(OUT)/HOL $(ALGEBRA_DEPENDENCIES) \ |
| 31771 | 592 |
Library/Multiset.thy \ |
| 32479 | 593 |
Number_Theory/Binomial.thy \ |
594 |
Number_Theory/Cong.thy \ |
|
595 |
Number_Theory/Fib.thy \ |
|
596 |
Number_Theory/MiscAlgebra.thy \ |
|
597 |
Number_Theory/Number_Theory.thy \ |
|
598 |
Number_Theory/Residues.thy \ |
|
599 |
Number_Theory/UniqueFactorization.thy \ |
|
600 |
Number_Theory/ROOT.ML |
|
601 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Number_Theory |
|
| 31719 | 602 |
|
603 |
||
| 32479 | 604 |
## HOL-Old_Number_Theory |
| 9510 | 605 |
|
| 32479 | 606 |
HOL-Old_Number_Theory: HOL $(LOG)/HOL-Old_Number_Theory.gz |
| 9510 | 607 |
|
| 37021 | 608 |
$(LOG)/HOL-Old_Number_Theory.gz: $(OUT)/HOL Library/Permutation.thy \ |
609 |
Old_Number_Theory/Primes.thy Old_Number_Theory/Fib.thy \ |
|
610 |
Old_Number_Theory/Factorization.thy Old_Number_Theory/BijectionRel.thy\ |
|
611 |
Old_Number_Theory/Chinese.thy Old_Number_Theory/EulerFermat.thy \ |
|
612 |
Old_Number_Theory/IntFact.thy Old_Number_Theory/IntPrimes.thy \ |
|
613 |
Old_Number_Theory/WilsonBij.thy Old_Number_Theory/WilsonRuss.thy \ |
|
614 |
Old_Number_Theory/Finite2.thy Old_Number_Theory/Int2.thy \ |
|
615 |
Old_Number_Theory/EvenOdd.thy Old_Number_Theory/Residues.thy \ |
|
616 |
Old_Number_Theory/Euler.thy Old_Number_Theory/Gauss.thy \ |
|
| 32479 | 617 |
Old_Number_Theory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy \ |
| 37021 | 618 |
Old_Number_Theory/Legacy_GCD.thy Old_Number_Theory/Pocklington.thy \ |
619 |
Old_Number_Theory/ROOT.ML |
|
| 32479 | 620 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Old_Number_Theory |
| 9510 | 621 |
|
622 |
||
| 4518 | 623 |
## HOL-Hoare |
624 |
||
625 |
HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz |
|
| 2448 | 626 |
|
| 27164 | 627 |
$(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.thy Hoare/Examples.thy \ |
628 |
Hoare/Hoare.thy Hoare/hoare_tac.ML Hoare/Heap.thy \ |
|
| 35319 | 629 |
Hoare/Hoare_Logic.thy Hoare/Hoare_Logic_Abort.thy \ |
| 27164 | 630 |
Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy Hoare/ROOT.ML \ |
631 |
Hoare/ExamplesAbort.thy Hoare/HeapSyntaxAbort.thy \ |
|
| 35319 | 632 |
Hoare/SchorrWaite.thy Hoare/Separation.thy \ |
| 27164 | 633 |
Hoare/SepLogHeap.thy Hoare/document/root.tex Hoare/document/root.bib |
| 28500 | 634 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Hoare |
| 2448 | 635 |
|
636 |
||
|
32621
a073cb249a06
theory entry point for session Hoare_Parallel (now also with proper underscore)
haftmann
parents:
32618
diff
changeset
|
637 |
## HOL-Hoare_Parallel |
| 12996 | 638 |
|
|
32621
a073cb249a06
theory entry point for session Hoare_Parallel (now also with proper underscore)
haftmann
parents:
32618
diff
changeset
|
639 |
HOL-Hoare_Parallel: HOL $(LOG)/HOL-Hoare_Parallel.gz |
| 12996 | 640 |
|
|
32621
a073cb249a06
theory entry point for session Hoare_Parallel (now also with proper underscore)
haftmann
parents:
32618
diff
changeset
|
641 |
$(LOG)/HOL-Hoare_Parallel.gz: $(OUT)/HOL Hoare_Parallel/Gar_Coll.thy \ |
| 33439 | 642 |
Hoare_Parallel/Graph.thy Hoare_Parallel/Hoare_Parallel.thy \ |
643 |
Hoare_Parallel/Mul_Gar_Coll.thy Hoare_Parallel/OG_Com.thy \ |
|
644 |
Hoare_Parallel/OG_Examples.thy Hoare_Parallel/OG_Hoare.thy \ |
|
645 |
Hoare_Parallel/OG_Syntax.thy Hoare_Parallel/OG_Tactics.thy \ |
|
646 |
Hoare_Parallel/OG_Tran.thy Hoare_Parallel/Quote_Antiquote.thy \ |
|
647 |
Hoare_Parallel/RG_Com.thy Hoare_Parallel/RG_Examples.thy \ |
|
648 |
Hoare_Parallel/RG_Hoare.thy Hoare_Parallel/RG_Syntax.thy \ |
|
649 |
Hoare_Parallel/RG_Tran.thy Hoare_Parallel/ROOT.ML \ |
|
650 |
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
|
651 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hoare_Parallel |
| 12996 | 652 |
|
653 |
||
| 37747 | 654 |
## HOL-Library-Codegenerator_Test |
|
37691
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
655 |
|
| 37747 | 656 |
HOL-Library-Codegenerator_Test: HOL-Library $(LOG)/HOL-Library-Codegenerator_Test.gz |
|
37691
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
657 |
|
| 37747 | 658 |
$(LOG)/HOL-Library-Codegenerator_Test.gz: $(OUT)/HOL-Library \ |
| 37742 | 659 |
Codegenerator_Test/ROOT.ML \ |
660 |
Codegenerator_Test/Candidates.thy \ |
|
|
37691
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
661 |
Codegenerator_Test/Candidates_Pretty.thy \ |
|
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
662 |
Codegenerator_Test/Generate.thy \ |
|
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
663 |
Codegenerator_Test/Generate_Pretty.thy |
|
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
664 |
@$(ISABELLE_TOOL) usedir -d false -g false -i false $(OUT)/HOL-Library Codegenerator_Test |
|
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
665 |
|
|
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
666 |
|
| 33027 | 667 |
## HOL-Metis_Examples |
| 23449 | 668 |
|
| 33027 | 669 |
HOL-Metis_Examples: HOL $(LOG)/HOL-Metis_Examples.gz |
| 23449 | 670 |
|
| 37742 | 671 |
$(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML \ |
672 |
Metis_Examples/Abstraction.thy Metis_Examples/BigO.thy \ |
|
673 |
Metis_Examples/BT.thy Metis_Examples/Message.thy \ |
|
674 |
Metis_Examples/Tarski.thy Metis_Examples/TransClosure.thy \ |
|
| 33027 | 675 |
Metis_Examples/set.thy |
676 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples |
|
| 23449 | 677 |
|
678 |
||
|
33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset
|
679 |
## HOL-Nitpick_Examples |
|
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset
|
680 |
|
|
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset
|
681 |
HOL-Nitpick_Examples: HOL $(LOG)/HOL-Nitpick_Examples.gz |
|
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset
|
682 |
|
| 34126 | 683 |
$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \ |
684 |
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
|
685 |
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
|
686 |
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
|
687 |
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
|
688 |
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
|
689 |
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
|
690 |
Nitpick_Examples/Tests_Nits.thy Nitpick_Examples/Typedef_Nits.thy |
|
33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset
|
691 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples |
|
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset
|
692 |
|
|
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset
|
693 |
|
|
7999
7acf6eb8eec1
Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
7985
diff
changeset
|
694 |
## HOL-Algebra |
|
7acf6eb8eec1
Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
7985
diff
changeset
|
695 |
|
| 33439 | 696 |
HOL-Algebra: HOL $(OUT)/HOL-Algebra |
|
7999
7acf6eb8eec1
Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
7985
diff
changeset
|
697 |
|
| 31771 | 698 |
ALGEBRA_DEPENDENCIES = $(OUT)/HOL \ |
699 |
Algebra/ROOT.ML \ |
|
700 |
Library/Binomial.thy \ |
|
701 |
Library/FuncSet.thy \ |
|
702 |
Library/Multiset.thy \ |
|
703 |
Library/Permutation.thy \ |
|
| 32479 | 704 |
Number_Theory/Primes.thy \ |
| 31771 | 705 |
Algebra/AbelCoset.thy \ |
706 |
Algebra/Bij.thy \ |
|
707 |
Algebra/Congruence.thy \ |
|
708 |
Algebra/Coset.thy \ |
|
709 |
Algebra/Divisibility.thy \ |
|
710 |
Algebra/Exponent.thy \ |
|
711 |
Algebra/FiniteProduct.thy \ |
|
712 |
Algebra/Group.thy \ |
|
713 |
Algebra/Ideal.thy \ |
|
714 |
Algebra/IntRing.thy \ |
|
715 |
Algebra/Lattice.thy \ |
|
716 |
Algebra/Module.thy \ |
|
717 |
Algebra/QuotRing.thy \ |
|
718 |
Algebra/Ring.thy \ |
|
719 |
Algebra/RingHom.thy \ |
|
720 |
Algebra/Sylow.thy \ |
|
721 |
Algebra/UnivPoly.thy \ |
|
722 |
Algebra/abstract/Abstract.thy \ |
|
723 |
Algebra/abstract/Factor.thy \ |
|
724 |
Algebra/abstract/Field.thy \ |
|
725 |
Algebra/abstract/Ideal2.thy \ |
|
726 |
Algebra/abstract/PID.thy \ |
|
727 |
Algebra/abstract/Ring2.thy \ |
|
728 |
Algebra/abstract/RingHomo.thy \ |
|
729 |
Algebra/document/root.tex \ |
|
730 |
Algebra/document/root.tex \ |
|
731 |
Algebra/poly/LongDiv.thy \ |
|
732 |
Algebra/poly/PolyHomo.thy \ |
|
733 |
Algebra/poly/Polynomial.thy \ |
|
734 |
Algebra/poly/UnivPoly2.thy \ |
|
735 |
Algebra/ringsimp.ML |
|
736 |
||
| 33448 | 737 |
$(OUT)/HOL-Algebra: $(ALGEBRA_DEPENDENCIES) |
| 28500 | 738 |
@cd Algebra; $(ISABELLE_TOOL) usedir -b -g true -V outline=/proof,/ML $(OUT)/HOL HOL-Algebra |
|
7999
7acf6eb8eec1
Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
7985
diff
changeset
|
739 |
|
|
27477
c64736fe2a1f
more precise dependencies for HOL-Word and HOL-NSA;
wenzelm
parents:
27470
diff
changeset
|
740 |
|
| 4518 | 741 |
## HOL-Auth |
| 3819 | 742 |
|
| 4518 | 743 |
HOL-Auth: HOL $(LOG)/HOL-Auth.gz |
| 3819 | 744 |
|
| 28098 | 745 |
$(LOG)/HOL-Auth.gz: $(OUT)/HOL \ |
| 37021 | 746 |
Auth/Auth_Shared.thy Auth/Auth_Public.thy Auth/All_Symmetric.thy \ |
747 |
Auth/Guard/Auth_Guard_Shared.thy \ |
|
748 |
Auth/Guard/Auth_Guard_Public.thy \ |
|
| 32632 | 749 |
Auth/Smartcard/Auth_Smartcard.thy Auth/All_Symmetric.thy \ |
| 27164 | 750 |
Auth/CertifiedEmail.thy Auth/Event.thy Auth/Message.thy \ |
751 |
Auth/NS_Public.thy Auth/NS_Public_Bad.thy Auth/NS_Shared.thy \ |
|
752 |
Auth/OtwayRees.thy Auth/OtwayReesBella.thy Auth/OtwayRees_AN.thy \ |
|
753 |
Auth/OtwayRees_Bad.thy Auth/Public.thy Auth/ROOT.ML Auth/Recur.thy \ |
|
754 |
Auth/Shared.thy Auth/TLS.thy Auth/WooLam.thy Auth/Kerberos_BAN.thy \ |
|
755 |
Auth/Kerberos_BAN_Gets.thy Auth/KerberosIV.thy \ |
|
756 |
Auth/KerberosIV_Gets.thy Auth/KerberosV.thy Auth/Yahalom.thy \ |
|
757 |
Auth/Yahalom2.thy Auth/Yahalom_Bad.thy Auth/ZhouGollmann.thy \ |
|
758 |
Auth/Guard/Analz.thy Auth/Guard/Extensions.thy Auth/Guard/GuardK.thy \ |
|
759 |
Auth/Guard/Guard_Public.thy Auth/Guard/Guard_Shared.thy \ |
|
760 |
Auth/Guard/Guard.thy Auth/Guard/List_Msg.thy \ |
|
761 |
Auth/Guard/Guard_NS_Public.thy Auth/Guard/Guard_OtwayRees.thy \ |
|
762 |
Auth/Guard/P1.thy Auth/Guard/P2.thy Auth/Guard/Proto.thy \ |
|
763 |
Auth/Guard/Guard_Yahalom.thy Auth/Smartcard/EventSC.thy \ |
|
764 |
Auth/Smartcard/ShoupRubinBella.thy Auth/Smartcard/ShoupRubin.thy \ |
|
765 |
Auth/Smartcard/Smartcard.thy Auth/document/root.tex |
|
| 28500 | 766 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Auth |
| 2448 | 767 |
|
768 |
||
| 4777 | 769 |
## HOL-UNITY |
770 |
||
771 |
HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz |
|
772 |
||
| 27164 | 773 |
$(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \ |
| 33439 | 774 |
UNITY/UNITY_Main.thy UNITY/UNITY_Examples.thy UNITY/UNITY_tactics.ML \ |
775 |
UNITY/Comp.thy UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy \ |
|
| 27164 | 776 |
UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy UNITY/Guar.thy \ |
777 |
UNITY/Lift_prog.thy UNITY/ListOrder.thy UNITY/ProgressSets.thy \ |
|
778 |
UNITY/PPROD.thy UNITY/Project.thy UNITY/Rename.thy \ |
|
779 |
UNITY/Transformers.thy UNITY/SubstAx.thy UNITY/UNITY.thy \ |
|
780 |
UNITY/Union.thy UNITY/WFair.thy UNITY/Simple/Channel.thy \ |
|
781 |
UNITY/Simple/Common.thy UNITY/Simple/Deadlock.thy \ |
|
782 |
UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy \ |
|
783 |
UNITY/Simple/NSP_Bad.thy UNITY/Simple/Network.thy \ |
|
784 |
UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy \ |
|
785 |
UNITY/Simple/Token.thy UNITY/Comp/Alloc.thy UNITY/Comp/AllocBase.thy \ |
|
786 |
UNITY/Comp/AllocImpl.thy UNITY/Comp/Client.thy \ |
|
787 |
UNITY/Comp/Counter.thy UNITY/Comp/Counterc.thy \ |
|
788 |
UNITY/Comp/Handshake.thy UNITY/Comp/PriorityAux.thy \ |
|
789 |
UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \ |
|
790 |
UNITY/Comp/TimerArray.thy UNITY/document/root.tex |
|
| 28500 | 791 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL UNITY |
| 4777 | 792 |
|
793 |
||
| 10966 | 794 |
## HOL-Unix |
795 |
||
796 |
HOL-Unix: HOL $(LOG)/HOL-Unix.gz |
|
797 |
||
| 37742 | 798 |
$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy \ |
799 |
Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy \ |
|
| 10966 | 800 |
Unix/document/root.bib Unix/document/root.tex |
| 39156 | 801 |
@$(ISABELLE_TOOL) usedir -m no_brackets -m no_type_brackets $(OUT)/HOL Unix |
| 10966 | 802 |
|
|
27477
c64736fe2a1f
more precise dependencies for HOL-Word and HOL-NSA;
wenzelm
parents:
27470
diff
changeset
|
803 |
|
| 19203 | 804 |
## HOL-ZF |
805 |
||
806 |
HOL-ZF: HOL $(LOG)/HOL-ZF.gz |
|
807 |
||
|
39306
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
808 |
$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/LProd.thy \ |
| 27164 | 809 |
ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex |
| 28500 | 810 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF |
| 10966 | 811 |
|
|
27477
c64736fe2a1f
more precise dependencies for HOL-Word and HOL-NSA;
wenzelm
parents:
27470
diff
changeset
|
812 |
|
|
29399
ebcd69a00872
split of Imperative_HOL theories from HOL-Library
haftmann
parents:
29197
diff
changeset
|
813 |
## HOL-Imperative_HOL |
|
ebcd69a00872
split of Imperative_HOL theories from HOL-Library
haftmann
parents:
29197
diff
changeset
|
814 |
|
|
ebcd69a00872
split of Imperative_HOL theories from HOL-Library
haftmann
parents:
29197
diff
changeset
|
815 |
HOL-Imperative_HOL: HOL $(LOG)/HOL-Imperative_HOL.gz |
|
ebcd69a00872
split of Imperative_HOL theories from HOL-Library
haftmann
parents:
29197
diff
changeset
|
816 |
|
|
39306
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
817 |
$(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
818 |
Imperative_HOL/Array.thy \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
819 |
Imperative_HOL/Heap.thy \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
820 |
Imperative_HOL/Heap_Monad.thy \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
821 |
Imperative_HOL/Imperative_HOL.thy \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
822 |
Imperative_HOL/Imperative_HOL_ex.thy \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
823 |
Imperative_HOL/Mrec.thy \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
824 |
Imperative_HOL/Ref.thy \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
825 |
Imperative_HOL/ROOT.ML \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
826 |
Imperative_HOL/ex/Imperative_Quicksort.thy \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
827 |
Imperative_HOL/ex/Imperative_Reverse.thy \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
828 |
Imperative_HOL/ex/Linked_Lists.thy \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
829 |
Imperative_HOL/ex/SatChecker.thy \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
830 |
Imperative_HOL/ex/Sorted_List.thy \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
831 |
Imperative_HOL/ex/Subarray.thy \ |
|
30689
b14b2cc4e25e
moved Imperative_HOL examples to Imperative_HOL/ex
haftmann
parents:
30654
diff
changeset
|
832 |
Imperative_HOL/ex/Sublist.thy |
|
39306
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
833 |
@$(ISABELLE_TOOL) usedir -g true -m iff -m no_brackets $(OUT)/HOL Imperative_HOL |
|
29399
ebcd69a00872
split of Imperative_HOL theories from HOL-Library
haftmann
parents:
29197
diff
changeset
|
834 |
|
|
ebcd69a00872
split of Imperative_HOL theories from HOL-Library
haftmann
parents:
29197
diff
changeset
|
835 |
|
|
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
836 |
## HOL-Decision_Procs |
|
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
837 |
|
|
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
838 |
HOL-Decision_Procs: HOL $(LOG)/HOL-Decision_Procs.gz |
|
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
839 |
|
|
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
840 |
$(LOG)/HOL-Decision_Procs.gz: $(OUT)/HOL \ |
|
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
841 |
Decision_Procs/Approximation.thy \ |
|
33356
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
33348
diff
changeset
|
842 |
Decision_Procs/Commutative_Ring.thy \ |
|
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
33348
diff
changeset
|
843 |
Decision_Procs/Commutative_Ring_Complete.thy \ |
|
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
844 |
Decision_Procs/Cooper.thy \ |
| 35053 | 845 |
Decision_Procs/Decision_Procs.thy \ |
|
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
846 |
Decision_Procs/Dense_Linear_Order.thy \ |
|
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
847 |
Decision_Procs/Ferrack.thy \ |
|
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
848 |
Decision_Procs/MIR.thy \ |
| 35053 | 849 |
Decision_Procs/Parametric_Ferrante_Rackoff.thy \ |
850 |
Decision_Procs/Polynomial_List.thy \ |
|
| 37120 | 851 |
Decision_Procs/ROOT.ML \ |
| 35053 | 852 |
Decision_Procs/Reflected_Multivariate_Polynomial.thy \ |
853 |
Decision_Procs/commutative_ring_tac.ML \ |
|
854 |
Decision_Procs/cooper_tac.ML \ |
|
|
30429
39acdf031548
moved Decision_Procs examples to Decision_Procs/ex
haftmann
parents:
30400
diff
changeset
|
855 |
Decision_Procs/ex/Approximation_Ex.thy \ |
|
33356
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
33348
diff
changeset
|
856 |
Decision_Procs/ex/Commutative_Ring_Ex.thy \ |
| 35053 | 857 |
Decision_Procs/ex/Dense_Linear_Order_Ex.thy \ |
858 |
Decision_Procs/ferrack_tac.ML \ |
|
| 37120 | 859 |
Decision_Procs/ferrante_rackoff.ML \ |
860 |
Decision_Procs/ferrante_rackoff_data.ML \ |
|
861 |
Decision_Procs/langford.ML \ |
|
862 |
Decision_Procs/langford_data.ML \ |
|
863 |
Decision_Procs/mir_tac.ML |
|
|
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
864 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Decision_Procs |
|
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
865 |
|
|
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
866 |
|
| 30400 | 867 |
## HOL-Docs |
868 |
||
869 |
HOL-Docs: HOL $(LOG)/HOL-Docs.gz |
|
870 |
||
| 37742 | 871 |
$(LOG)/HOL-Docs.gz: $(OUT)/HOL Docs/Main_Doc.thy Docs/ROOT.ML \ |
| 30400 | 872 |
Docs/document/root.tex |
| 30440 | 873 |
@$(ISABELLE_TOOL) usedir -D generated $(OUT)/HOL Docs |
| 30400 | 874 |
|
875 |
||
|
39157
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
876 |
## HOL-Proofs |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
877 |
|
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
878 |
HOL-Proofs: Pure $(OUT)/HOL-Proofs |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
879 |
|
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
880 |
$(OUT)/HOL-Proofs: main.ML $(MAIN_DEPENDENCIES) |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
881 |
@$(ISABELLE_TOOL) usedir -b -f main.ML -g true -p 2 -q 0 $(OUT)/Pure HOL-Proofs |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
882 |
|
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
883 |
|
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
884 |
## HOL-Proofs-ex |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
885 |
|
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
886 |
HOL-Proofs-ex: HOL-Proofs $(LOG)/HOL-Proofs-ex.gz |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
887 |
|
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
888 |
$(LOG)/HOL-Proofs-ex.gz: $(OUT)/HOL-Proofs \ |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
889 |
Proofs/ex/ROOT.ML Proofs/ex/Hilbert_Classical.thy |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
890 |
@cd Proofs; $(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs ex |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
891 |
|
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
892 |
|
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
893 |
## HOL-Proofs-Extraction |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
894 |
|
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
895 |
HOL-Proofs-Extraction: HOL-Proofs $(LOG)/HOL-Proofs-Extraction.gz |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
896 |
|
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
897 |
$(LOG)/HOL-Proofs-Extraction.gz: $(OUT)/HOL-Proofs \ |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
898 |
Library/Efficient_Nat.thy Proofs/Extraction/Euclid.thy \ |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
899 |
Proofs/Extraction/Greatest_Common_Divisor.thy \ |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
900 |
Proofs/Extraction/Higman.thy Proofs/Extraction/Pigeonhole.thy \ |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
901 |
Proofs/Extraction/QuotRem.thy Proofs/Extraction/ROOT.ML \ |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
902 |
Proofs/Extraction/Util.thy Proofs/Extraction/Warshall.thy \ |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
903 |
Proofs/Extraction/document/root.tex \ |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
904 |
Proofs/Extraction/document/root.bib |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
905 |
@cd Proofs; $(ISABELLE_TOOL) usedir -p 2 -q 0 $(OUT)/HOL-Proofs Extraction |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
906 |
|
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
907 |
|
|
34205
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
908 |
## HOL-Proofs-Lambda |
| 2448 | 909 |
|
|
34205
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
910 |
HOL-Proofs-Lambda: HOL-Proofs $(LOG)/HOL-Proofs-Lambda.gz |
| 2448 | 911 |
|
|
39157
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
912 |
$(LOG)/HOL-Proofs-Lambda.gz: $(OUT)/HOL-Proofs \ |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
913 |
Proofs/Lambda/Commutation.thy Proofs/Lambda/Eta.thy \ |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
914 |
Proofs/Lambda/InductTermi.thy Proofs/Lambda/Lambda.thy \ |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
915 |
Proofs/Lambda/ListApplication.thy Proofs/Lambda/ListBeta.thy \ |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
916 |
Proofs/Lambda/ListOrder.thy Proofs/Lambda/NormalForm.thy \ |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
917 |
Proofs/Lambda/ParRed.thy Proofs/Lambda/Standardization.thy \ |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
918 |
Proofs/Lambda/StrongNorm.thy Proofs/Lambda/Type.thy \ |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
919 |
Proofs/Lambda/WeakNorm.thy Proofs/Lambda/ROOT.ML \ |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
920 |
Proofs/Lambda/document/root.bib Proofs/Lambda/document/root.tex |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
921 |
@cd Proofs; $(ISABELLE_TOOL) usedir -g true -m no_brackets -p 2 -q 0 $(OUT)/HOL-Proofs Lambda |
| 2448 | 922 |
|
923 |
||
| 9015 | 924 |
## HOL-Prolog |
925 |
||
926 |
HOL-Prolog: HOL $(LOG)/HOL-Prolog.gz |
|
927 |
||
| 27164 | 928 |
$(LOG)/HOL-Prolog.gz: $(OUT)/HOL Prolog/ROOT.ML Prolog/prolog.ML \ |
929 |
Prolog/HOHH.thy Prolog/Test.thy Prolog/Func.thy Prolog/Type.thy |
|
| 28500 | 930 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Prolog |
| 9015 | 931 |
|
932 |
||
| 8012 | 933 |
## HOL-MicroJava |
934 |
||
935 |
HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz |
|
936 |
||
| 27164 | 937 |
$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL Library/Executable_Set.thy \ |
938 |
MicroJava/ROOT.ML MicroJava/Comp/AuxLemmas.thy \ |
|
939 |
MicroJava/Comp/CorrComp.thy MicroJava/Comp/CorrCompTp.thy \ |
|
940 |
MicroJava/Comp/DefsComp.thy MicroJava/Comp/Index.thy \ |
|
941 |
MicroJava/Comp/LemmasComp.thy MicroJava/Comp/NatCanonify.thy \ |
|
942 |
MicroJava/Comp/TranslComp.thy MicroJava/Comp/TranslCompTp.thy \ |
|
943 |
MicroJava/Comp/TypeInf.thy MicroJava/J/Conform.thy \ |
|
944 |
MicroJava/J/Eval.thy MicroJava/J/JBasis.thy \ |
|
945 |
MicroJava/J/JTypeSafe.thy MicroJava/J/Decl.thy MicroJava/J/State.thy \ |
|
946 |
MicroJava/J/Term.thy MicroJava/J/Type.thy MicroJava/J/TypeRel.thy \ |
|
947 |
MicroJava/J/WellForm.thy MicroJava/J/Value.thy \ |
|
948 |
MicroJava/J/WellType.thy MicroJava/J/Example.thy \ |
|
949 |
MicroJava/J/JListExample.thy MicroJava/JVM/JVMExec.thy \ |
|
950 |
MicroJava/JVM/JVMInstructions.thy MicroJava/JVM/JVMState.thy \ |
|
951 |
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
|
952 |
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
|
953 |
MicroJava/DFA/Err.thy MicroJava/DFA/Kildall.thy \ |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33820
diff
changeset
|
954 |
MicroJava/DFA/LBVComplete.thy MicroJava/DFA/LBVCorrect.thy \ |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33820
diff
changeset
|
955 |
MicroJava/DFA/LBVSpec.thy MicroJava/DFA/Listn.thy \ |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33820
diff
changeset
|
956 |
MicroJava/DFA/Opt.thy MicroJava/DFA/Product.thy \ |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33820
diff
changeset
|
957 |
MicroJava/DFA/SemilatAlg.thy MicroJava/DFA/Semilat.thy \ |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33820
diff
changeset
|
958 |
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
|
959 |
MicroJava/DFA/Typing_Framework.thy MicroJava/BV/BVSpec.thy \ |
| 27164 | 960 |
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
|
961 |
MicroJava/BV/JType.thy MicroJava/BV/JVM.thy MicroJava/BV/JVMType.thy \ |
| 27164 | 962 |
MicroJava/BV/Effect.thy MicroJava/BV/EffectMono.thy \ |
963 |
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
|
964 |
MicroJava/BV/LBVJVM.thy MicroJava/document/root.bib \ |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33820
diff
changeset
|
965 |
MicroJava/document/root.tex MicroJava/document/introduction.tex |
| 28500 | 966 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL MicroJava |
| 11850 | 967 |
|
| 8012 | 968 |
|
| 11376 | 969 |
## HOL-NanoJava |
970 |
||
971 |
HOL-NanoJava: HOL $(LOG)/HOL-NanoJava.gz |
|
972 |
||
| 27164 | 973 |
$(LOG)/HOL-NanoJava.gz: $(OUT)/HOL NanoJava/ROOT.ML NanoJava/Term.thy \ |
974 |
NanoJava/Decl.thy NanoJava/TypeRel.thy NanoJava/State.thy \ |
|
975 |
NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy \ |
|
| 11376 | 976 |
NanoJava/document/root.bib NanoJava/document/root.tex |
| 28500 | 977 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NanoJava |
| 11850 | 978 |
|
| 8193 | 979 |
|
| 12855 | 980 |
## HOL-Bali |
981 |
||
982 |
HOL-Bali: HOL $(LOG)/HOL-Bali.gz |
|
983 |
||
|
33024
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
984 |
$(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/Bali.thy Bali/AxCompl.thy \ |
|
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
985 |
Bali/AxExample.thy Bali/AxSem.thy Bali/AxSound.thy Bali/Basis.thy \ |
|
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
986 |
Bali/Conform.thy Bali/Decl.thy Bali/DeclConcepts.thy Bali/Eval.thy \ |
|
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
987 |
Bali/Evaln.thy Bali/Example.thy Bali/Name.thy Bali/ROOT.ML \ |
|
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
988 |
Bali/State.thy Bali/Table.thy Bali/Term.thy Bali/Trans.thy \ |
|
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
989 |
Bali/Type.thy Bali/TypeRel.thy Bali/TypeSafe.thy Bali/Value.thy \ |
|
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
990 |
Bali/WellForm.thy Bali/DefiniteAssignment.thy \ |
|
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
991 |
Bali/DefiniteAssignmentCorrect.thy Bali/WellType.thy \ |
|
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
992 |
Bali/document/root.tex |
| 28500 | 993 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Bali |
| 12855 | 994 |
|
995 |
||
| 4518 | 996 |
## HOL-IOA |
997 |
||
998 |
HOL-IOA: HOL $(LOG)/HOL-IOA.gz |
|
| 2448 | 999 |
|
| 27164 | 1000 |
$(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.thy IOA/IOA.thy IOA/ROOT.ML \ |
1001 |
IOA/Solve.thy |
|
| 28500 | 1002 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL IOA |
| 4518 | 1003 |
|
1004 |
||
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
1005 |
## HOL-Lattice |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
1006 |
|
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
1007 |
HOL-Lattice: HOL $(LOG)/HOL-Lattice.gz |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
1008 |
|
| 27164 | 1009 |
$(LOG)/HOL-Lattice.gz: $(OUT)/HOL Lattice/Bounds.thy \ |
1010 |
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
|
1011 |
Lattice/ROOT.ML Lattice/document/root.tex |
| 28500 | 1012 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Lattice |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
1013 |
|
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
1014 |
|
| 4518 | 1015 |
## HOL-ex |
| 2448 | 1016 |
|
| 4518 | 1017 |
HOL-ex: HOL $(LOG)/HOL-ex.gz |
| 2448 | 1018 |
|
| 33439 | 1019 |
$(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy \ |
|
39157
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
1020 |
Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \ |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
1021 |
ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy ex/BT.thy \ |
|
40632
dc55e6752046
adding birthday paradoxon from some abandoned drawer
bulwahn
parents:
40582
diff
changeset
|
1022 |
ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradoxon.thy ex/CTL.thy \ |
|
dc55e6752046
adding birthday paradoxon from some abandoned drawer
bulwahn
parents:
40582
diff
changeset
|
1023 |
ex/Chinese.thy \ |
|
40281
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
40277
diff
changeset
|
1024 |
ex/Classical.thy ex/CodegenSML_Test.thy ex/Coercion_Examples.thy \ |
|
3c6198fd0937
Coercive subtyping via subtype constraints, by Dmitriy Traytel (21-Oct-2010).
wenzelm
parents:
40277
diff
changeset
|
1025 |
ex/Coherent.thy ex/Dedekind_Real.thy ex/Efficient_Nat_examples.thy \ |
|
39157
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
1026 |
ex/Eval_Examples.thy ex/Fundefs.thy ex/Gauge_Integration.thy \ |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
1027 |
ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \ |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
1028 |
ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \ |
|
40239
c4336e45f199
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
wenzelm
parents:
40178
diff
changeset
|
1029 |
ex/Iff_Oracle.thy ex/Induction_Schema.thy ex/InductiveInvariant.thy \ |
| 35329 | 1030 |
ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy \ |
|
39157
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
1031 |
ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy \ |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
1032 |
ex/Meson_Test.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \ |
|
40239
c4336e45f199
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
wenzelm
parents:
40178
diff
changeset
|
1033 |
ex/Normalization_by_Evaluation.thy ex/Numeral.thy ex/PER.thy \ |
|
c4336e45f199
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
wenzelm
parents:
40178
diff
changeset
|
1034 |
ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.thy \ |
| 40349 | 1035 |
ex/Quickcheck_Lattice_Examples.thy ex/Quicksort.thy ex/ROOT.ML \ |
1036 |
ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \ |
|
1037 |
ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \ |
|
1038 |
ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy \ |
|
1039 |
ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy \ |
|
1040 |
ex/Unification.thy ex/While_Combinator_Example.thy \ |
|
1041 |
ex/document/root.bib ex/document/root.tex ex/set.thy ex/svc_funcs.ML \ |
|
1042 |
ex/svc_test.thy |
|
| 28500 | 1043 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex |
| 2448 | 1044 |
|
1045 |
||
| 33026 | 1046 |
## HOL-Isar_Examples |
| 6445 | 1047 |
|
| 33026 | 1048 |
HOL-Isar_Examples: HOL $(LOG)/HOL-Isar_Examples.gz |
| 6445 | 1049 |
|
| 33026 | 1050 |
$(LOG)/HOL-Isar_Examples.gz: $(OUT)/HOL Isar_Examples/Basic_Logic.thy \ |
1051 |
Isar_Examples/Cantor.thy Isar_Examples/Drinker.thy \ |
|
1052 |
Isar_Examples/Expr_Compiler.thy Isar_Examples/Fibonacci.thy \ |
|
1053 |
Isar_Examples/Group.thy Isar_Examples/Hoare.thy \ |
|
1054 |
Isar_Examples/Hoare_Ex.thy Isar_Examples/Knaster_Tarski.thy \ |
|
1055 |
Isar_Examples/Mutilated_Checkerboard.thy \ |
|
1056 |
Isar_Examples/Nested_Datatype.thy Isar_Examples/Peirce.thy \ |
|
1057 |
Isar_Examples/Puzzle.thy Isar_Examples/Summation.thy \ |
|
1058 |
Isar_Examples/ROOT.ML Isar_Examples/document/proof.sty \ |
|
1059 |
Isar_Examples/document/root.bib Isar_Examples/document/root.tex \ |
|
| 37672 | 1060 |
Isar_Examples/document/style.tex Hoare/hoare_tac.ML \ |
1061 |
Number_Theory/Primes.thy |
|
| 33026 | 1062 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Isar_Examples |
| 6445 | 1063 |
|
1064 |
||
| 33028 | 1065 |
## HOL-SET_Protocol |
| 14199 | 1066 |
|
| 33028 | 1067 |
HOL-SET_Protocol: HOL $(LOG)/HOL-SET_Protocol.gz |
| 14199 | 1068 |
|
| 33028 | 1069 |
$(LOG)/HOL-SET_Protocol.gz: $(OUT)/HOL SET_Protocol/ROOT.ML \ |
1070 |
SET_Protocol/Message_SET.thy SET_Protocol/Event_SET.thy \ |
|
1071 |
SET_Protocol/Public_SET.thy SET_Protocol/Cardholder_Registration.thy \ |
|
1072 |
SET_Protocol/Merchant_Registration.thy SET_Protocol/Purchase.thy \ |
|
| 39757 | 1073 |
SET_Protocol/SET_Protocol.thy SET_Protocol/document/root.tex |
| 33028 | 1074 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL SET_Protocol |
| 14199 | 1075 |
|
1076 |
||
| 27421 | 1077 |
## HOL-Matrix |
| 14610 | 1078 |
|
| 28637 | 1079 |
HOL-Matrix: HOL $(LOG)/HOL-Matrix.gz |
| 17323 | 1080 |
|
|
37872
d83659570337
moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway;
wenzelm
parents:
37818
diff
changeset
|
1081 |
$(LOG)/HOL-Matrix.gz: $(OUT)/HOL Matrix/ComputeFloat.thy \ |
|
d83659570337
moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway;
wenzelm
parents:
37818
diff
changeset
|
1082 |
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
|
1083 |
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
|
1084 |
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
|
1085 |
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
|
1086 |
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
|
1087 |
Matrix/Compute_Oracle/linker.ML Matrix/Cplex.thy \ |
| 37764 | 1088 |
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
|
1089 |
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
|
1090 |
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
|
1091 |
Matrix/fspmlp.ML Matrix/matrixlp.ML Tools/float_arith.ML |
| 28500 | 1092 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Matrix |
| 16873 | 1093 |
|
| 14199 | 1094 |
|
| 4518 | 1095 |
## TLA |
1096 |
||
1097 |
TLA: HOL $(OUT)/TLA |
|
1098 |
||
| 27164 | 1099 |
$(OUT)/TLA: $(OUT)/HOL TLA/Action.thy TLA/Init.thy TLA/Intensional.thy \ |
| 21624 | 1100 |
TLA/ROOT.ML TLA/Stfun.thy TLA/TLA.thy |
| 28500 | 1101 |
@cd TLA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL TLA |
| 4518 | 1102 |
|
1103 |
||
1104 |
## TLA-Inc |
|
1105 |
||
1106 |
TLA-Inc: TLA $(LOG)/TLA-Inc.gz |
|
1107 |
||
| 21624 | 1108 |
$(LOG)/TLA-Inc.gz: $(OUT)/TLA TLA/Inc/Inc.thy |
| 28500 | 1109 |
@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Inc |
| 4518 | 1110 |
|
1111 |
||
1112 |
## TLA-Buffer |
|
1113 |
||
1114 |
TLA-Buffer: TLA $(LOG)/TLA-Buffer.gz |
|
| 2448 | 1115 |
|
|
33024
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
1116 |
$(LOG)/TLA-Buffer.gz: $(OUT)/TLA TLA/Buffer/Buffer.thy \ |
|
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
1117 |
TLA/Buffer/DBuffer.thy |
| 28500 | 1118 |
@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Buffer |
| 4518 | 1119 |
|
1120 |
||
1121 |
## TLA-Memory |
|
1122 |
||
1123 |
TLA-Memory: TLA $(LOG)/TLA-Memory.gz |
|
| 4447 | 1124 |
|
| 27164 | 1125 |
$(LOG)/TLA-Memory.gz: $(OUT)/TLA TLA/Memory/MemClerk.thy \ |
1126 |
TLA/Memory/MemClerkParameters.thy TLA/Memory/Memory.thy \ |
|
1127 |
TLA/Memory/MemoryImplementation.thy TLA/Memory/MemoryParameters.thy \ |
|
1128 |
TLA/Memory/ProcedureInterface.thy TLA/Memory/RPC.thy \ |
|
| 21624 | 1129 |
TLA/Memory/RPCMemoryParams.thy TLA/Memory/RPCParameters.thy |
| 28500 | 1130 |
@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Memory |
| 4518 | 1131 |
|
1132 |
||
| 33175 | 1133 |
## HOL-Multivariate_Analysis |
1134 |
||
| 36898 | 1135 |
HOL-Multivariate_Analysis: HOL $(OUT)/HOL-Multivariate_Analysis |
| 33175 | 1136 |
|
| 36937 | 1137 |
$(OUT)/HOL-Multivariate_Analysis: $(OUT)/HOL \ |
1138 |
Multivariate_Analysis/Brouwer_Fixpoint.thy \ |
|
| 37522 | 1139 |
Multivariate_Analysis/Cartesian_Euclidean_Space.thy \ |
| 36937 | 1140 |
Multivariate_Analysis/Convex_Euclidean_Space.thy \ |
1141 |
Multivariate_Analysis/Derivative.thy \ |
|
1142 |
Multivariate_Analysis/Determinants.thy \ |
|
1143 |
Multivariate_Analysis/Euclidean_Space.thy \ |
|
1144 |
Multivariate_Analysis/Fashoda.thy \ |
|
1145 |
Multivariate_Analysis/Finite_Cartesian_Product.thy \ |
|
1146 |
Multivariate_Analysis/Integration.certs \ |
|
1147 |
Multivariate_Analysis/Integration.thy \ |
|
| 38656 | 1148 |
Multivariate_Analysis/Gauge_Measure.thy \ |
| 36937 | 1149 |
Multivariate_Analysis/L2_Norm.thy \ |
1150 |
Multivariate_Analysis/Multivariate_Analysis.thy \ |
|
1151 |
Multivariate_Analysis/Operator_Norm.thy \ |
|
1152 |
Multivariate_Analysis/Path_Connected.thy \ |
|
1153 |
Multivariate_Analysis/ROOT.ML \ |
|
1154 |
Multivariate_Analysis/Real_Integration.thy \ |
|
1155 |
Multivariate_Analysis/Topology_Euclidean_Space.thy \ |
|
1156 |
Multivariate_Analysis/document/root.tex \ |
|
| 37742 | 1157 |
Multivariate_Analysis/normarith.ML Library/Glbs.thy \ |
1158 |
Library/Inner_Product.thy Library/Numeral_Type.thy \ |
|
| 36937 | 1159 |
Library/Convex.thy Library/FrechetDeriv.thy \ |
|
36649
bfd8c550faa6
Corrected imports; better approximation of dependencies.
hoelzl
parents:
36648
diff
changeset
|
1160 |
Library/Product_Vector.thy Library/Product_plus.thy |
| 36898 | 1161 |
@cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Multivariate_Analysis |
| 33175 | 1162 |
|
| 33285 | 1163 |
|
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33270
diff
changeset
|
1164 |
## HOL-Probability |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33270
diff
changeset
|
1165 |
|
| 38656 | 1166 |
HOL-Probability: HOL-Multivariate_Analysis $(OUT)/HOL-Probability |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33270
diff
changeset
|
1167 |
|
| 38656 | 1168 |
$(OUT)/HOL-Probability: $(OUT)/HOL-Multivariate_Analysis Probability/ROOT.ML \ |
| 37742 | 1169 |
Probability/Probability.thy Probability/Sigma_Algebra.thy \ |
| 38656 | 1170 |
Probability/Caratheodory.thy \ |
| 37742 | 1171 |
Probability/Borel.thy Probability/Measure.thy \ |
| 38656 | 1172 |
Probability/Lebesgue_Integration.thy Probability/Lebesgue_Measure.thy \ |
1173 |
Probability/Positive_Infinite_Real.thy Probability/Product_Measure.thy \ |
|
| 37742 | 1174 |
Probability/Probability_Space.thy Probability/Information.thy \ |
1175 |
Probability/ex/Dining_Cryptographers.thy Library/FuncSet.thy \ |
|
| 38656 | 1176 |
Probability/Lebesgue_Measure.thy \ |
1177 |
Library/Nat_Bijection.thy Library/Countable.thy |
|
1178 |
@cd Probability; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Multivariate_Analysis HOL-Probability |
|
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33270
diff
changeset
|
1179 |
|
|
39157
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
1180 |
|
| 19497 | 1181 |
## HOL-Nominal |
1182 |
||
1183 |
HOL-Nominal: HOL $(OUT)/HOL-Nominal |
|
1184 |
||
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
22167
diff
changeset
|
1185 |
$(OUT)/HOL-Nominal: $(OUT)/HOL Nominal/ROOT.ML \ |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
22167
diff
changeset
|
1186 |
Nominal/Nominal.thy \ |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
22167
diff
changeset
|
1187 |
Nominal/nominal_atoms.ML \ |
| 31936 | 1188 |
Nominal/nominal_datatype.ML \ |
|
22784
4637b69de71b
Added datatype_case.ML and nominal_fresh_fun.ML.
berghofe
parents:
22657
diff
changeset
|
1189 |
Nominal/nominal_fresh_fun.ML \ |
| 22247 | 1190 |
Nominal/nominal_induct.ML \ |
| 22314 | 1191 |
Nominal/nominal_inductive.ML \ |
| 28652 | 1192 |
Nominal/nominal_inductive2.ML \ |
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
22167
diff
changeset
|
1193 |
Nominal/nominal_permeq.ML \ |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
22167
diff
changeset
|
1194 |
Nominal/nominal_primrec.ML \ |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
22167
diff
changeset
|
1195 |
Nominal/nominal_thmdecls.ML \ |
|
39777
4f8f08362bf7
moved old_primrec source to nominal package, where it is still used
haftmann
parents:
39776
diff
changeset
|
1196 |
Nominal/old_primrec.ML \ |
| 21542 | 1197 |
Library/Infinite_Set.thy |
| 28500 | 1198 |
@cd Nominal; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Nominal |
| 19497 | 1199 |
|
1200 |
||
1201 |
## HOL-Nominal-Examples |
|
1202 |
||
1203 |
HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz |
|
1204 |
||
|
39157
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
1205 |
$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal \ |
|
32636
55a0be42327c
added session theory for Bali and Nominal_Examples
haftmann
parents:
32632
diff
changeset
|
1206 |
Nominal/Examples/Nominal_Examples.thy \ |
| 27163 | 1207 |
Nominal/Examples/CK_Machine.thy \ |
|
22073
c170dcbe6c9d
formalisation of Crary's chapter on logical relations
urbanc
parents:
22067
diff
changeset
|
1208 |
Nominal/Examples/CR.thy \ |
|
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
22819
diff
changeset
|
1209 |
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
|
1210 |
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
|
1211 |
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
|
1212 |
Nominal/Examples/Class3.thy \ |
|
22073
c170dcbe6c9d
formalisation of Crary's chapter on logical relations
urbanc
parents:
22067
diff
changeset
|
1213 |
Nominal/Examples/Compile.thy \ |
| 25725 | 1214 |
Nominal/Examples/Contexts.thy \ |
1215 |
Nominal/Examples/Crary.thy \ |
|
|
22073
c170dcbe6c9d
formalisation of Crary's chapter on logical relations
urbanc
parents:
22067
diff
changeset
|
1216 |
Nominal/Examples/Fsub.thy \ |
| 25725 | 1217 |
Nominal/Examples/Height.thy \ |
1218 |
Nominal/Examples/Lam_Funs.thy \ |
|
|
22073
c170dcbe6c9d
formalisation of Crary's chapter on logical relations
urbanc
parents:
22067
diff
changeset
|
1219 |
Nominal/Examples/Lambda_mu.thy \ |
| 25725 | 1220 |
Nominal/Examples/LocalWeakening.thy \ |
| 33189 | 1221 |
Nominal/Examples/Pattern.thy \ |
| 25725 | 1222 |
Nominal/Examples/ROOT.ML \ |
|
22073
c170dcbe6c9d
formalisation of Crary's chapter on logical relations
urbanc
parents:
22067
diff
changeset
|
1223 |
Nominal/Examples/SN.thy \ |
| 23144 | 1224 |
Nominal/Examples/SOS.thy \ |
|
27624
a925aa66e17a
Added Standardization theory to nominal examples.
berghofe
parents:
27484
diff
changeset
|
1225 |
Nominal/Examples/Standardization.thy \ |
|
24896
70f238757695
added the two new examples from Nominal to the build process
urbanc
parents:
24830
diff
changeset
|
1226 |
Nominal/Examples/Support.thy \ |
| 27032 | 1227 |
Nominal/Examples/Type_Preservation.thy \ |
| 25725 | 1228 |
Nominal/Examples/VC_Condition.thy \ |
| 26195 | 1229 |
Nominal/Examples/W.thy \ |
| 25725 | 1230 |
Nominal/Examples/Weakening.thy |
| 28500 | 1231 |
@cd Nominal; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Nominal Examples |
| 19497 | 1232 |
|
1233 |
||
| 24333 | 1234 |
## HOL-Word |
1235 |
||
1236 |
HOL-Word: HOL $(OUT)/HOL-Word |
|
1237 |
||
|
33024
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
1238 |
$(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML Library/Boolean_Algebra.thy \ |
| 37655 | 1239 |
Library/Numeral_Type.thy Word/Misc_Numeric.thy Word/Misc_Typedef.thy \ |
| 37659 | 1240 |
Word/Type_Length.thy Word/Bit_Representation.thy Word/Bit_Int.thy \ |
1241 |
Word/Bool_List_Representation.thy Word/Bit_Operations.thy \ |
|
| 37660 | 1242 |
Word/Word.thy Word/document/root.tex \ |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
1243 |
Word/document/root.bib Tools/SMT/smt_word.ML |
| 28500 | 1244 |
@cd Word; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Word |
| 24333 | 1245 |
|
1246 |
||
| 24442 | 1247 |
## HOL-Word-Examples |
1248 |
||
1249 |
HOL-Word-Examples: HOL-Word $(LOG)/HOL-Word-Examples.gz |
|
1250 |
||
| 27164 | 1251 |
$(LOG)/HOL-Word-Examples.gz: $(OUT)/HOL-Word Word/Examples/ROOT.ML \ |
| 24442 | 1252 |
Word/Examples/WordExamples.thy |
| 28500 | 1253 |
@cd Word; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Word Examples |
| 24442 | 1254 |
|
|
27477
c64736fe2a1f
more precise dependencies for HOL-Word and HOL-NSA;
wenzelm
parents:
27470
diff
changeset
|
1255 |
|
| 25171 | 1256 |
## HOL-Statespace |
1257 |
||
1258 |
HOL-Statespace: HOL $(LOG)/HOL-Statespace.gz |
|
1259 |
||
| 27164 | 1260 |
$(LOG)/HOL-Statespace.gz: $(OUT)/HOL Statespace/DistinctTreeProver.thy \ |
1261 |
Statespace/StateFun.thy Statespace/StateSpaceLocale.thy \ |
|
1262 |
Statespace/StateSpaceSyntax.thy Statespace/StateSpaceEx.thy \ |
|
1263 |
Statespace/distinct_tree_prover.ML Statespace/state_space.ML \ |
|
1264 |
Statespace/state_fun.ML Statespace/document/root.tex |
|
| 28500 | 1265 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Statespace |
| 24442 | 1266 |
|
|
27477
c64736fe2a1f
more precise dependencies for HOL-Word and HOL-NSA;
wenzelm
parents:
27470
diff
changeset
|
1267 |
|
| 27470 | 1268 |
## HOL-NSA |
1269 |
||
|
27477
c64736fe2a1f
more precise dependencies for HOL-Word and HOL-NSA;
wenzelm
parents:
27470
diff
changeset
|
1270 |
HOL-NSA: HOL $(OUT)/HOL-NSA |
| 27470 | 1271 |
|
|
33024
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
1272 |
$(OUT)/HOL-NSA: $(OUT)/HOL NSA/CLim.thy NSA/CStar.thy NSA/NSCA.thy \ |
|
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
1273 |
NSA/NSComplex.thy NSA/HDeriv.thy NSA/HLim.thy NSA/HLog.thy \ |
|
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
1274 |
NSA/HSEQ.thy NSA/HSeries.thy NSA/HTranscendental.thy \ |
|
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
1275 |
NSA/Hypercomplex.thy NSA/HyperDef.thy NSA/HyperNat.thy \ |
|
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
1276 |
NSA/Hyperreal.thy NSA/Filter.thy NSA/NatStar.thy NSA/NSA.thy \ |
|
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
1277 |
NSA/StarDef.thy NSA/Star.thy NSA/transfer.ML \ |
|
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
1278 |
Library/Infinite_Set.thy Library/Zorn.thy NSA/ROOT.ML |
| 28500 | 1279 |
@cd NSA; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-NSA |
| 27470 | 1280 |
|
|
27477
c64736fe2a1f
more precise dependencies for HOL-Word and HOL-NSA;
wenzelm
parents:
27470
diff
changeset
|
1281 |
|
| 27470 | 1282 |
## HOL-NSA-Examples |
1283 |
||
1284 |
HOL-NSA-Examples: HOL-NSA $(LOG)/HOL-NSA-Examples.gz |
|
1285 |
||
| 37742 | 1286 |
$(LOG)/HOL-NSA-Examples.gz: $(OUT)/HOL-NSA NSA/Examples/ROOT.ML \ |
| 27470 | 1287 |
NSA/Examples/NSPrimes.thy |
| 28500 | 1288 |
@cd NSA; $(ISABELLE_TOOL) usedir $(OUT)/HOL-NSA Examples |
| 27470 | 1289 |
|
|
27477
c64736fe2a1f
more precise dependencies for HOL-Word and HOL-NSA;
wenzelm
parents:
27470
diff
changeset
|
1290 |
|
| 32496 | 1291 |
## HOL-Mirabelle |
1292 |
||
1293 |
HOL-Mirabelle: HOL $(LOG)/HOL-Mirabelle.gz |
|
1294 |
||
|
33024
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
1295 |
$(LOG)/HOL-Mirabelle.gz: $(OUT)/HOL Mirabelle/Mirabelle_Test.thy \ |
|
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
1296 |
Mirabelle/Mirabelle.thy Mirabelle/Tools/mirabelle.ML \ |
|
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
1297 |
Mirabelle/ROOT.ML Mirabelle/Tools/mirabelle_arith.ML \ |
|
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
1298 |
Mirabelle/Tools/mirabelle_metis.ML \ |
|
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
1299 |
Mirabelle/Tools/mirabelle_quickcheck.ML \ |
|
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
1300 |
Mirabelle/Tools/mirabelle_refute.ML \ |
|
40634
dc124a486f94
adding dependencies to IsaMakefile; adding sledgehammer_tactic in Mirabelle_Test
bulwahn
parents:
40632
diff
changeset
|
1301 |
Mirabelle/Tools/mirabelle_sledgehammer.ML \ |
|
dc124a486f94
adding dependencies to IsaMakefile; adding sledgehammer_tactic in Mirabelle_Test
bulwahn
parents:
40632
diff
changeset
|
1302 |
Mirabelle/Tools/sledgehammer_tactic.ML |
| 32496 | 1303 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle |
1304 |
||
1305 |
||
|
36933
705b58fde476
more precise dependencies for HOL-Word-SMT_Examples;
wenzelm
parents:
36916
diff
changeset
|
1306 |
## HOL-Word-SMT_Examples |
|
32618
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
32558
diff
changeset
|
1307 |
|
|
36933
705b58fde476
more precise dependencies for HOL-Word-SMT_Examples;
wenzelm
parents:
36916
diff
changeset
|
1308 |
HOL-Word-SMT_Examples: HOL-Word $(LOG)/HOL-Word-SMT_Examples.gz |
|
32618
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
32558
diff
changeset
|
1309 |
|
|
36933
705b58fde476
more precise dependencies for HOL-Word-SMT_Examples;
wenzelm
parents:
36916
diff
changeset
|
1310 |
$(LOG)/HOL-Word-SMT_Examples.gz: $(OUT)/HOL-Word SMT_Examples/ROOT.ML \ |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
1311 |
SMT_Examples/SMT_Examples.thy SMT_Examples/SMT_Examples.certs \ |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
1312 |
SMT_Examples/SMT_Word_Examples.thy SMT_Examples/SMT_Tests.thy \ |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
1313 |
SMT_Examples/SMT_Word_Examples.certs SMT_Examples/SMT_Tests.certs |
|
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
1314 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL-Word SMT_Examples |
| 33010 | 1315 |
|
1316 |
||
| 33419 | 1317 |
## HOL-Boogie |
1318 |
||
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
1319 |
HOL-Boogie: HOL-Word $(OUT)/HOL-Boogie |
| 33419 | 1320 |
|
| 36901 | 1321 |
$(OUT)/HOL-Boogie: $(OUT)/HOL-Word Boogie/ROOT.ML Boogie/Boogie.thy \ |
| 33439 | 1322 |
Boogie/Tools/boogie_vcs.ML Boogie/Tools/boogie_loader.ML \ |
| 34069 | 1323 |
Boogie/Tools/boogie_commands.ML Boogie/Tools/boogie_tactics.ML |
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
1324 |
@cd Boogie; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-Boogie |
| 33419 | 1325 |
|
1326 |
||
1327 |
## HOL-Boogie_Examples |
|
1328 |
||
| 33439 | 1329 |
HOL-Boogie-Examples: HOL-Boogie $(LOG)/HOL-Boogie-Examples.gz |
| 33419 | 1330 |
|
| 33439 | 1331 |
$(LOG)/HOL-Boogie-Examples.gz: $(OUT)/HOL-Boogie \ |
1332 |
Boogie/Examples/ROOT.ML Boogie/Examples/Boogie_Max.thy \ |
|
1333 |
Boogie/Examples/Boogie_Max.b2i Boogie/Examples/Boogie_Dijkstra.thy \ |
|
1334 |
Boogie/Examples/VCC_Max.thy Boogie/Examples/Boogie_Dijkstra.b2i \ |
|
| 34996 | 1335 |
Boogie/Examples/VCC_Max.b2i Boogie/Examples/Boogie_Max.certs \ |
1336 |
Boogie/Examples/Boogie_Dijkstra.certs Boogie/Examples/VCC_Max.certs |
|
| 33419 | 1337 |
@cd Boogie; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Boogie Examples |
1338 |
||
1339 |
||
| 34965 | 1340 |
## HOL-Mutabelle |
1341 |
||
1342 |
HOL-Mutabelle: HOL $(LOG)/HOL-Mutabelle.gz |
|
1343 |
||
1344 |
$(LOG)/HOL-Mutabelle.gz: $(OUT)/HOL Mutabelle/MutabelleExtra.thy \ |
|
| 35959 | 1345 |
Mutabelle/ROOT.ML Mutabelle/mutabelle.ML \ |
| 34965 | 1346 |
Mutabelle/mutabelle_extra.ML |
1347 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mutabelle |
|
1348 |
||
1349 |
||
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
1350 |
## HOL-Quotient_Examples |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
1351 |
|
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
1352 |
HOL-Quotient_Examples: HOL $(LOG)/HOL-Quotient_Examples.gz |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
1353 |
|
| 35959 | 1354 |
$(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL \ |
| 37742 | 1355 |
Quotient_Examples/FSet.thy Quotient_Examples/Quotient_Int.thy \ |
|
36524
3909002beca5
Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
36403
diff
changeset
|
1356 |
Quotient_Examples/Quotient_Message.thy |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
1357 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
1358 |
|
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
1359 |
|
|
35950
791ce568d40a
moved examples for the predicate compiler into its own session Predicate_Compile_Examples to slenderise the HOL-ex session
bulwahn
parents:
35931
diff
changeset
|
1360 |
## HOL-Predicate_Compile_Examples |
|
791ce568d40a
moved examples for the predicate compiler into its own session Predicate_Compile_Examples to slenderise the HOL-ex session
bulwahn
parents:
35931
diff
changeset
|
1361 |
|
|
791ce568d40a
moved examples for the predicate compiler into its own session Predicate_Compile_Examples to slenderise the HOL-ex session
bulwahn
parents:
35931
diff
changeset
|
1362 |
HOL-Predicate_Compile_Examples: HOL $(LOG)/HOL-Predicate_Compile_Examples.gz |
|
791ce568d40a
moved examples for the predicate compiler into its own session Predicate_Compile_Examples to slenderise the HOL-ex session
bulwahn
parents:
35931
diff
changeset
|
1363 |
|
| 35959 | 1364 |
$(LOG)/HOL-Predicate_Compile_Examples.gz: $(OUT)/HOL \ |
|
35955
e657fb805c68
added predicate compiler quickcheck examples to new session Predicate_Compile_Examples
bulwahn
parents:
35953
diff
changeset
|
1365 |
Predicate_Compile_Examples/ROOT.ML \ |
|
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
39564
diff
changeset
|
1366 |
Predicate_Compile_Examples/Predicate_Compile_Tests.thy \ |
|
38074
31174744b9a2
adding example file for prolog code generation; adding prolog code generation example to IsaMakefile
bulwahn
parents:
38047
diff
changeset
|
1367 |
Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy \ |
|
38730
5bbdd9a9df62
adding hotel keycard example for prolog generation
bulwahn
parents:
38656
diff
changeset
|
1368 |
Predicate_Compile_Examples/Code_Prolog_Examples.thy \ |
|
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
39564
diff
changeset
|
1369 |
Predicate_Compile_Examples/Examples.thy \ |
| 39185 | 1370 |
Predicate_Compile_Examples/Context_Free_Grammar_Example.thy \ |
| 38948 | 1371 |
Predicate_Compile_Examples/Hotel_Example.thy \ |
|
40104
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
40067
diff
changeset
|
1372 |
Predicate_Compile_Examples/Hotel_Example_Prolog.thy \ |
|
82873a6f2b81
splitting Hotel Key card example into specification and the two tests for counter example generation
bulwahn
parents:
40067
diff
changeset
|
1373 |
Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy \ |
| 39186 | 1374 |
Predicate_Compile_Examples/IMP_1.thy \ |
1375 |
Predicate_Compile_Examples/IMP_2.thy \ |
|
1376 |
Predicate_Compile_Examples/IMP_3.thy \ |
|
1377 |
Predicate_Compile_Examples/IMP_4.thy \ |
|
|
39184
71f3f194b962
adding a List example (challenge from Tobias) for counterexample search
bulwahn
parents:
39183
diff
changeset
|
1378 |
Predicate_Compile_Examples/Lambda_Example.thy \ |
| 39188 | 1379 |
Predicate_Compile_Examples/List_Examples.thy \ |
1380 |
Predicate_Compile_Examples/Reg_Exp_Example.thy |
|
|
35950
791ce568d40a
moved examples for the predicate compiler into its own session Predicate_Compile_Examples to slenderise the HOL-ex session
bulwahn
parents:
35931
diff
changeset
|
1381 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Predicate_Compile_Examples |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
1382 |
|
| 35959 | 1383 |
|
| 4518 | 1384 |
## clean |
| 4447 | 1385 |
|
1386 |
clean: |
|
| 33450 | 1387 |
@rm -f $(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz \ |
1388 |
$(LOG)/HOL-Bali.gz $(LOG)/HOL-Base.gz \ |
|
1389 |
$(LOG)/HOL-Boogie-Examples.gz $(LOG)/HOL-Boogie.gz \ |
|
|
34205
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
1390 |
$(LOG)/HOL-Decision_Procs.gz $(LOG)/HOL-Hahn_Banach.gz \ |
|
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
1391 |
$(LOG)/HOL-Hoare.gz $(LOG)/HOL-Hoare_Parallel.gz \ |
|
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
1392 |
$(LOG)/HOL-IMP.gz $(LOG)/HOL-IMPP.gz $(LOG)/HOL-IOA.gz \ |
| 33450 | 1393 |
$(LOG)/HOL-Imperative_HOL.gz $(LOG)/HOL-Import.gz \ |
1394 |
$(LOG)/HOL-Induct.gz $(LOG)/HOL-Isar_Examples.gz \ |
|
|
34205
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
1395 |
$(LOG)/HOL-Lattice $(LOG)/HOL-Lattice.gz \ |
|
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
1396 |
$(LOG)/HOL-Lex.gz $(LOG)/HOL-Library.gz \ |
|
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
1397 |
$(LOG)/HOL-Main.gz $(LOG)/HOL-Matrix \ |
|
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
1398 |
$(LOG)/HOL-Matrix.gz $(LOG)/HOL-Metis_Examples.gz \ |
|
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
1399 |
$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-Mirabelle.gz \ |
| 33450 | 1400 |
$(LOG)/HOL-Multivariate_Analysis.gz \ |
1401 |
$(LOG)/HOL-NSA-Examples.gz $(LOG)/HOL-NSA.gz \ |
|
1402 |
$(LOG)/HOL-NanoJava.gz $(LOG)/HOL-Nitpick_Examples.gz \ |
|
1403 |
$(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-Nominal.gz \ |
|
1404 |
$(LOG)/HOL-Number_Theory.gz \ |
|
1405 |
$(LOG)/HOL-Old_Number_Theory.gz $(LOG)/HOL-Plain.gz \ |
|
| 35959 | 1406 |
$(LOG)/HOL-Predicate_Compile_Examples.gz \ |
| 33450 | 1407 |
$(LOG)/HOL-Probability.gz $(LOG)/HOL-Prolog.gz \ |
|
39157
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
1408 |
$(LOG)/HOL-Proofs.gz $(LOG)/HOL-Proofs-ex.gz \ |
|
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
1409 |
$(LOG)/HOL-Proofs-Extraction.gz \ |
|
34205
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
1410 |
$(LOG)/HOL-Proofs-Lambda.gz $(LOG)/HOL-SET_Protocol.gz \ |
|
36933
705b58fde476
more precise dependencies for HOL-Word-SMT_Examples;
wenzelm
parents:
36916
diff
changeset
|
1411 |
$(LOG)/HOL-Word-SMT_Examples.gz \ |
|
705b58fde476
more precise dependencies for HOL-Word-SMT_Examples;
wenzelm
parents:
36916
diff
changeset
|
1412 |
$(LOG)/HOL-Statespace.gz $(LOG)/HOL-Subst.gz \ |
|
705b58fde476
more precise dependencies for HOL-Word-SMT_Examples;
wenzelm
parents:
36916
diff
changeset
|
1413 |
$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz \ |
|
705b58fde476
more precise dependencies for HOL-Word-SMT_Examples;
wenzelm
parents:
36916
diff
changeset
|
1414 |
$(LOG)/HOL-Word-Examples.gz $(LOG)/HOL-Word.gz \ |
|
705b58fde476
more precise dependencies for HOL-Word-SMT_Examples;
wenzelm
parents:
36916
diff
changeset
|
1415 |
$(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz $(LOG)/HOL.gz \ |
|
705b58fde476
more precise dependencies for HOL-Word-SMT_Examples;
wenzelm
parents:
36916
diff
changeset
|
1416 |
$(LOG)/HOL4.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Inc.gz \ |
|
705b58fde476
more precise dependencies for HOL-Word-SMT_Examples;
wenzelm
parents:
36916
diff
changeset
|
1417 |
$(LOG)/TLA-Memory.gz $(LOG)/TLA.gz $(OUT)/HOL \ |
|
705b58fde476
more precise dependencies for HOL-Word-SMT_Examples;
wenzelm
parents:
36916
diff
changeset
|
1418 |
$(OUT)/HOL-Algebra $(OUT)/HOL-Base $(OUT)/HOL-Boogie \ |
|
705b58fde476
more precise dependencies for HOL-Word-SMT_Examples;
wenzelm
parents:
36916
diff
changeset
|
1419 |
$(OUT)/HOL-Main $(OUT)/HOL-Multivariate_Analysis \ |
|
705b58fde476
more precise dependencies for HOL-Word-SMT_Examples;
wenzelm
parents:
36916
diff
changeset
|
1420 |
$(OUT)/HOL-NSA $(OUT)/HOL-Nominal $(OUT)/HOL-Plain \ |
| 35931 | 1421 |
$(OUT)/HOL-Probability $(OUT)/HOL-Proofs \ |
| 36898 | 1422 |
$(OUT)/HOL-Word $(OUT)/HOL4 $(OUT)/TLA |