| author | wenzelm |
| Sat, 17 Mar 2012 12:52:40 +0100 | |
| changeset 46988 | 9f492f5b0cec |
| parent 46951 | 4e032ac36134 |
| child 47108 | 2a1953f0d20d |
| permissions | -rw-r--r-- |
| 2448 | 1 |
# |
2 |
# IsaMakefile for HOL |
|
3 |
# |
|
4 |
||
| 4518 | 5 |
## targets |
| 2448 | 6 |
|
| 4518 | 7 |
default: HOL |
|
33210
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset
|
8 |
|
|
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset
|
9 |
images: \ |
|
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset
|
10 |
HOL \ |
|
37691
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
11 |
HOL-Library \ |
|
33210
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset
|
12 |
HOL-Algebra \ |
| 33419 | 13 |
HOL-Boogie \ |
| 43917 | 14 |
HOL-IMP \ |
|
33210
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset
|
15 |
HOL-Multivariate_Analysis \ |
|
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset
|
16 |
HOL-NSA \ |
|
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset
|
17 |
HOL-Nominal \ |
|
34205
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
18 |
HOL-Proofs \ |
| 41566 | 19 |
HOL-SPARK \ |
|
33210
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset
|
20 |
HOL-Word \ |
| 40774 | 21 |
HOLCF \ |
22 |
IOA \ |
|
|
37691
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
23 |
TLA \ |
|
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
24 |
HOL-Base \ |
|
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
25 |
HOL-Main \ |
|
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
26 |
HOL-Plain |
| 10135 | 27 |
|
|
42138
e54a985daa61
added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
krauss
parents:
42071
diff
changeset
|
28 |
#Note: keep targets sorted |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
29 |
test: \ |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
30 |
HOL-Auth \ |
| 14031 | 31 |
HOL-Bali \ |
| 33439 | 32 |
HOL-Boogie-Examples \ |
|
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset
|
33 |
HOL-Hahn_Banach \ |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
34 |
HOL-Hoare \ |
|
32621
a073cb249a06
theory entry point for session Hoare_Parallel (now also with proper underscore)
haftmann
parents:
32618
diff
changeset
|
35 |
HOL-Hoare_Parallel \ |
| 40774 | 36 |
HOLCF-FOCUS \ |
37 |
HOLCF-IMP \ |
|
38 |
HOLCF-Library \ |
|
39 |
HOLCF-Tutorial \ |
|
40 |
HOLCF-ex \ |
|
| 46809 | 41 |
HOL-HOL4 \ |
42 |
HOL-HOL4-Imported \ |
|
43 |
HOL-HOL_Light \ |
|
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
44 |
HOL-IMPP \ |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
45 |
HOL-IOA \ |
| 40774 | 46 |
IOA-ABP \ |
47 |
IOA-NTP \ |
|
48 |
IOA-Storage \ |
|
49 |
IOA-ex \ |
|
|
29399
ebcd69a00872
split of Imperative_HOL theories from HOL-Library
haftmann
parents:
29197
diff
changeset
|
50 |
HOL-Imperative_HOL \ |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
51 |
HOL-Induct \ |
| 33026 | 52 |
HOL-Isar_Examples \ |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
53 |
HOL-Lattice \ |
| 37747 | 54 |
HOL-Library-Codegenerator_Test \ |
|
46988
9f492f5b0cec
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset
|
55 |
HOL-Matrix_LP \ |
| 33027 | 56 |
HOL-Metis_Examples \ |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
57 |
HOL-MicroJava \ |
| 32496 | 58 |
HOL-Mirabelle \ |
| 35536 | 59 |
HOL-Mutabelle \ |
| 11376 | 60 |
HOL-NanoJava \ |
|
33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset
|
61 |
HOL-Nitpick_Examples \ |
| 32479 | 62 |
HOL-Number_Theory \ |
63 |
HOL-Old_Number_Theory \ |
|
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
64 |
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
|
65 |
HOL-Predicate_Compile_Examples \ |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
66 |
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
|
67 |
HOL-Proofs-ex \ |
|
34205
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
68 |
HOL-Proofs-Lambda \ |
| 33028 | 69 |
HOL-SET_Protocol \ |
| 41569 | 70 |
HOL-SPARK-Examples \ |
| 45044 | 71 |
HOL-SPARK-Manual \ |
|
36933
705b58fde476
more precise dependencies for HOL-Word-SMT_Examples;
wenzelm
parents:
36916
diff
changeset
|
72 |
HOL-Word-SMT_Examples \ |
| 25171 | 73 |
HOL-Statespace \ |
|
33210
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset
|
74 |
TLA-Buffer \ |
|
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset
|
75 |
TLA-Inc \ |
|
94ae82a4452f
recovered sort indentation for "sort position", as documented in the file;
wenzelm
parents:
33204
diff
changeset
|
76 |
TLA-Memory \ |
|
43804
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
43800
diff
changeset
|
77 |
HOL-TPTP \ |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
78 |
HOL-UNITY \ |
| 10966 | 79 |
HOL-Unix \ |
| 24442 | 80 |
HOL-Word-Examples \ |
| 24325 | 81 |
HOL-ZF |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
82 |
# ^ this is the sort position |
| 10614 | 83 |
|
| 46785 | 84 |
generate: \ |
| 46808 | 85 |
HOL-HOL4-Generate \ |
86 |
HOL-HOL_Light-Generate |
|
| 46785 | 87 |
|
| 45860 | 88 |
benchmark: \ |
89 |
HOL-Datatype_Benchmark \ |
|
90 |
HOL-Record_Benchmark |
|
91 |
||
|
42138
e54a985daa61
added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
krauss
parents:
42071
diff
changeset
|
92 |
images-no-smlnj: \ |
|
e54a985daa61
added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
krauss
parents:
42071
diff
changeset
|
93 |
HOL-Probability |
| 4518 | 94 |
|
|
42138
e54a985daa61
added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
krauss
parents:
42071
diff
changeset
|
95 |
test-no-smlnj: \ |
|
e54a985daa61
added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
krauss
parents:
42071
diff
changeset
|
96 |
HOL-ex \ |
|
e54a985daa61
added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
krauss
parents:
42071
diff
changeset
|
97 |
HOL-Decision_Procs \ |
|
e54a985daa61
added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
krauss
parents:
42071
diff
changeset
|
98 |
HOL-Proofs-Extraction \ |
|
e54a985daa61
added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
krauss
parents:
42071
diff
changeset
|
99 |
HOL-Nominal-Examples |
|
e54a985daa61
added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
krauss
parents:
42071
diff
changeset
|
100 |
|
|
e54a985daa61
added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
krauss
parents:
42071
diff
changeset
|
101 |
all: test-no-smlnj test images-no-smlnj images |
|
46701
879f5c76ffb6
reactivated Find_Unused_Assms_Examples to avoid untested / dead stuff in the repository;
wenzelm
parents:
46664
diff
changeset
|
102 |
full: all benchmark HOL-Quickcheck_Examples |
|
42138
e54a985daa61
added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
krauss
parents:
42071
diff
changeset
|
103 |
smlnj: test images |
| 4518 | 104 |
|
| 45860 | 105 |
|
| 4518 | 106 |
## global settings |
107 |
||
108 |
SRC = $(ISABELLE_HOME)/src |
|
| 3118 | 109 |
OUT = $(ISABELLE_OUTPUT) |
| 4447 | 110 |
LOG = $(OUT)/log |
| 2448 | 111 |
|
| 4518 | 112 |
|
113 |
## HOL |
|
| 2448 | 114 |
|
| 28393 | 115 |
HOL: Pure $(OUT)/HOL |
| 27368 | 116 |
|
| 29505 | 117 |
HOL-Base: Pure $(OUT)/HOL-Base |
118 |
||
| 27368 | 119 |
HOL-Plain: Pure $(OUT)/HOL-Plain |
| 4518 | 120 |
|
| 28401 | 121 |
HOL-Main: Pure $(OUT)/HOL-Main |
122 |
||
| 4518 | 123 |
Pure: |
| 28500 | 124 |
@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
|
125 |
|
| 27694 | 126 |
$(OUT)/Pure: Pure |
127 |
||
| 36073 | 128 |
BASE_DEPENDENCIES = $(OUT)/Pure \ |
|
30160
5f7b17941730
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset
|
129 |
$(SRC)/Provers/blast.ML \ |
|
5f7b17941730
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset
|
130 |
$(SRC)/Provers/clasimp.ML \ |
|
5f7b17941730
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset
|
131 |
$(SRC)/Provers/classical.ML \ |
|
5f7b17941730
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset
|
132 |
$(SRC)/Provers/hypsubst.ML \ |
|
5f7b17941730
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset
|
133 |
$(SRC)/Provers/quantifier1.ML \ |
|
5f7b17941730
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset
|
134 |
$(SRC)/Provers/splitter.ML \ |
| 31771 | 135 |
$(SRC)/Tools/Code/code_haskell.ML \ |
136 |
$(SRC)/Tools/Code/code_ml.ML \ |
|
|
38970
53d1ee3d98b8
factored out generic part of Scala serializer into code_namespace.ML
haftmann
parents:
38965
diff
changeset
|
137 |
$(SRC)/Tools/Code/code_namespace.ML \ |
| 31771 | 138 |
$(SRC)/Tools/Code/code_preproc.ML \ |
139 |
$(SRC)/Tools/Code/code_printer.ML \ |
|
| 39402 | 140 |
$(SRC)/Tools/Code/code_runtime.ML \ |
| 34945 | 141 |
$(SRC)/Tools/Code/code_scala.ML \ |
| 37442 | 142 |
$(SRC)/Tools/Code/code_simp.ML \ |
| 31771 | 143 |
$(SRC)/Tools/Code/code_target.ML \ |
144 |
$(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
|
145 |
$(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
|
146 |
$(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
|
147 |
$(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
|
148 |
$(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
|
149 |
$(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
|
150 |
$(SRC)/Tools/atomize_elim.ML \ |
| 44120 | 151 |
$(SRC)/Tools/cache_io.ML \ |
| 41827 | 152 |
$(SRC)/Tools/case_product.ML \ |
|
30160
5f7b17941730
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset
|
153 |
$(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
|
154 |
$(SRC)/Tools/cong_tac.ML \ |
|
30160
5f7b17941730
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset
|
155 |
$(SRC)/Tools/eqsubst.ML \ |
|
5f7b17941730
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset
|
156 |
$(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
|
157 |
$(SRC)/Tools/induct_tacs.ML \ |
|
45014
0e847655b2d8
New proof method "induction" that gives induction hypotheses the name IH.
nipkow
parents:
44962
diff
changeset
|
158 |
$(SRC)/Tools/induction.ML \ |
|
30165
6ee87f67d9cd
moved generic intuitionistic prover to src/Tools/intuitionistic.ML;
wenzelm
parents:
30160
diff
changeset
|
159 |
$(SRC)/Tools/intuitionistic.ML \ |
|
37781
2fbbf0a48cef
moved misc legacy stuff from OldGoals to Misc_Legacy;
wenzelm
parents:
37779
diff
changeset
|
160 |
$(SRC)/Tools/misc_legacy.ML \ |
|
30160
5f7b17941730
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset
|
161 |
$(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
|
162 |
$(SRC)/Tools/project_rule.ML \ |
|
30973
304ab57afa6e
observe distinction between Pure/Tools and Tools more closely
haftmann
parents:
30954
diff
changeset
|
163 |
$(SRC)/Tools/quickcheck.ML \ |
|
40116
9ed3711366c8
introduced manual version of "Auto Solve" as "solve_direct"
blanchet
parents:
40067
diff
changeset
|
164 |
$(SRC)/Tools/solve_direct.ML \ |
| 43614 | 165 |
$(SRC)/Tools/subtyping.ML \ |
| 43018 | 166 |
$(SRC)/Tools/try.ML \ |
|
30160
5f7b17941730
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents:
30101
diff
changeset
|
167 |
$(SRC)/Tools/value.ML \ |
| 29505 | 168 |
HOL.thy \ |
169 |
Tools/hologic.ML \ |
|
| 36073 | 170 |
Tools/simpdata.ML |
| 29505 | 171 |
|
172 |
$(OUT)/HOL-Base: base.ML $(BASE_DEPENDENCIES) |
|
| 29523 | 173 |
@$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base |
| 29505 | 174 |
|
|
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
|
175 |
PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES) \ |
|
40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset
|
176 |
$(SRC)/Provers/Arith/cancel_div_mod.ML \ |
|
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset
|
177 |
$(SRC)/Provers/Arith/cancel_sums.ML \ |
|
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset
|
178 |
$(SRC)/Provers/Arith/fast_lin_arith.ML \ |
|
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset
|
179 |
$(SRC)/Provers/order.ML \ |
|
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset
|
180 |
$(SRC)/Provers/trancl.ML \ |
|
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset
|
181 |
$(SRC)/Tools/Metis/metis.ML \ |
|
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset
|
182 |
$(SRC)/Tools/rat.ML \ |
|
43691
c00febb8e39c
moved ATP dependencies to HOL-Plain, where they belong
blanchet
parents:
43614
diff
changeset
|
183 |
ATP.thy \ |
|
44860
56101fa00193
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
haftmann
parents:
44818
diff
changeset
|
184 |
Complete_Lattices.thy \ |
| 40108 | 185 |
Complete_Partial_Order.thy \ |
| 27368 | 186 |
Datatype.thy \ |
187 |
Extraction.thy \ |
|
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35039
diff
changeset
|
188 |
Fields.thy \ |
| 27368 | 189 |
Finite_Set.thy \ |
190 |
Fun.thy \ |
|
191 |
FunDef.thy \ |
|
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35039
diff
changeset
|
192 |
Groups.thy \ |
| 27368 | 193 |
Inductive.thy \ |
194 |
Lattices.thy \ |
|
| 39945 | 195 |
Meson.thy \ |
| 39946 | 196 |
Metis.thy \ |
| 27368 | 197 |
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
|
198 |
Option.thy \ |
| 27368 | 199 |
Orderings.thy \ |
| 40108 | 200 |
Partial_Function.thy \ |
| 27368 | 201 |
Plain.thy \ |
202 |
Power.thy \ |
|
203 |
Product_Type.thy \ |
|
204 |
Relation.thy \ |
|
|
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35039
diff
changeset
|
205 |
Rings.thy \ |
| 27368 | 206 |
SAT.thy \ |
207 |
Set.thy \ |
|
208 |
Sum_Type.thy \ |
|
|
43691
c00febb8e39c
moved ATP dependencies to HOL-Plain, where they belong
blanchet
parents:
43614
diff
changeset
|
209 |
Tools/ATP/atp_problem.ML \ |
| 46320 | 210 |
Tools/ATP/atp_problem_generate.ML \ |
|
43691
c00febb8e39c
moved ATP dependencies to HOL-Plain, where they belong
blanchet
parents:
43614
diff
changeset
|
211 |
Tools/ATP/atp_proof.ML \ |
| 46320 | 212 |
Tools/ATP/atp_proof_reconstruct.ML \ |
213 |
Tools/ATP/atp_proof_redirect.ML \ |
|
|
43691
c00febb8e39c
moved ATP dependencies to HOL-Plain, where they belong
blanchet
parents:
43614
diff
changeset
|
214 |
Tools/ATP/atp_systems.ML \ |
|
c00febb8e39c
moved ATP dependencies to HOL-Plain, where they belong
blanchet
parents:
43614
diff
changeset
|
215 |
Tools/ATP/atp_util.ML \ |
|
40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset
|
216 |
Tools/Datatype/datatype.ML \ |
| 31771 | 217 |
Tools/Datatype/datatype_aux.ML \ |
218 |
Tools/Datatype/datatype_case.ML \ |
|
219 |
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
|
220 |
Tools/Datatype/datatype_data.ML \ |
| 31771 | 221 |
Tools/Datatype/datatype_prop.ML \ |
222 |
Tools/Datatype/datatype_realizer.ML \ |
|
|
45897
65cef0298158
clarified modules that contribute to datatype package;
wenzelm
parents:
45890
diff
changeset
|
223 |
Tools/Datatype/primrec.ML \ |
| 45890 | 224 |
Tools/Datatype/rep_datatype.ML \ |
| 31771 | 225 |
Tools/Function/context_tree.ML \ |
|
40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset
|
226 |
Tools/Function/fun.ML \ |
|
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset
|
227 |
Tools/Function/function.ML \ |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
33098
diff
changeset
|
228 |
Tools/Function/function_common.ML \ |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
33098
diff
changeset
|
229 |
Tools/Function/function_core.ML \ |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
33098
diff
changeset
|
230 |
Tools/Function/function_lib.ML \ |
| 33471 | 231 |
Tools/Function/induction_schema.ML \ |
| 31771 | 232 |
Tools/Function/lexicographic_order.ML \ |
233 |
Tools/Function/measure_functions.ML \ |
|
234 |
Tools/Function/mutual.ML \ |
|
| 40108 | 235 |
Tools/Function/partial_function.ML \ |
| 33083 | 236 |
Tools/Function/pat_completeness.ML \ |
| 31771 | 237 |
Tools/Function/pattern_split.ML \ |
| 33100 | 238 |
Tools/Function/relation.ML \ |
| 31771 | 239 |
Tools/Function/scnp_reconstruct.ML \ |
240 |
Tools/Function/scnp_solve.ML \ |
|
241 |
Tools/Function/size.ML \ |
|
242 |
Tools/Function/sum_tree.ML \ |
|
243 |
Tools/Function/termination.ML \ |
|
| 39940 | 244 |
Tools/Meson/meson.ML \ |
245 |
Tools/Meson/meson_clausify.ML \ |
|
| 39948 | 246 |
Tools/Meson/meson_tactic.ML \ |
| 46320 | 247 |
Tools/Metis/metis_generate.ML \ |
| 39946 | 248 |
Tools/Metis/metis_reconstruct.ML \ |
|
44651
5d6a11e166cf
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
blanchet
parents:
44516
diff
changeset
|
249 |
Tools/Metis/metis_tactic.ML \ |
|
40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset
|
250 |
Tools/abel_cancel.ML \ |
|
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset
|
251 |
Tools/arith_data.ML \ |
|
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset
|
252 |
Tools/cnf_funcs.ML \ |
|
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset
|
253 |
Tools/dseq.ML \ |
| 45890 | 254 |
Tools/enriched_type.ML \ |
|
40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset
|
255 |
Tools/inductive.ML \ |
|
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset
|
256 |
Tools/inductive_realizer.ML \ |
|
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset
|
257 |
Tools/inductive_set.ML \ |
|
44087
8e491cb8841c
load lambda-lifting structure earlier, so it can be used in Metis
blanchet
parents:
44014
diff
changeset
|
258 |
Tools/lambda_lifting.ML \ |
|
40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset
|
259 |
Tools/lin_arith.ML \ |
|
44087
8e491cb8841c
load lambda-lifting structure earlier, so it can be used in Metis
blanchet
parents:
44014
diff
changeset
|
260 |
Tools/monomorph.ML \ |
|
30496
7cdcc9dd95cb
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
haftmann
parents:
30457
diff
changeset
|
261 |
Tools/nat_arith.ML \ |
| 27368 | 262 |
Tools/prop_logic.ML \ |
263 |
Tools/refute.ML \ |
|
264 |
Tools/rewrite_hol_proof.ML \ |
|
265 |
Tools/sat_funcs.ML \ |
|
266 |
Tools/sat_solver.ML \ |
|
267 |
Tools/split_rule.ML \ |
|
| 46641 | 268 |
Tools/try0.ML \ |
|
31723
f5cafe803b55
discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents:
31706
diff
changeset
|
269 |
Tools/typedef.ML \ |
| 27368 | 270 |
Transitive_Closure.thy \ |
271 |
Typedef.thy \ |
|
|
40939
2c150063cd4d
setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents:
40863
diff
changeset
|
272 |
Wellfounded.thy |
|
28312
f0838044f034
different session branches for HOL-Plain vs. Plain
haftmann
parents:
28243
diff
changeset
|
273 |
|
|
f0838044f034
different session branches for HOL-Plain vs. Plain
haftmann
parents:
28243
diff
changeset
|
274 |
$(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES) |
| 28500 | 275 |
@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain |
| 27368 | 276 |
|
| 28401 | 277 |
MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \ |
|
35725
4d7e3cc9c52c
Big_Operators now in Main rather than Plain src/HOL/Wellfounded.thy
haftmann
parents:
35719
diff
changeset
|
278 |
Big_Operators.thy \ |
| 32657 | 279 |
Code_Evaluation.thy \ |
|
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset
|
280 |
Code_Numeral.thy \ |
|
33296
a3924d1069e5
moved theory Divides after theory Nat_Numeral; tuned some proof texts
haftmann
parents:
33272
diff
changeset
|
281 |
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
|
282 |
DSequence.thy \ |
| 27368 | 283 |
Equiv_Relations.thy \ |
|
40650
d40b347d5b0b
adding Enum to HOL-Main image and removing it from HOL-Library
bulwahn
parents:
40634
diff
changeset
|
284 |
Enum.thy \ |
| 27368 | 285 |
Groebner_Basis.thy \ |
286 |
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
|
287 |
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
|
288 |
Lazy_Sequence.thy \ |
| 27421 | 289 |
List.thy \ |
290 |
Main.thy \ |
|
291 |
Map.thy \ |
|
| 30925 | 292 |
Nat_Numeral.thy \ |
|
33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33298
diff
changeset
|
293 |
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
|
294 |
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
|
295 |
New_Random_Sequence.thy \ |
|
36915
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
296 |
Nitpick.thy \ |
|
33356
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
33348
diff
changeset
|
297 |
Numeral_Simprocs.thy \ |
| 27421 | 298 |
Presburger.thy \ |
|
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46650
diff
changeset
|
299 |
Predicate.thy \ |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33210
diff
changeset
|
300 |
Predicate_Compile.thy \ |
|
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31186
diff
changeset
|
301 |
Quickcheck.thy \ |
| 41919 | 302 |
Quickcheck_Exhaustive.thy \ |
| 43310 | 303 |
Quickcheck_Narrowing.thy \ |
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
304 |
Quotient.thy \ |
|
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31186
diff
changeset
|
305 |
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
|
306 |
Random_Sequence.thy \ |
| 39271 | 307 |
Record.thy \ |
| 36916 | 308 |
Refute.thy \ |
|
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36700
diff
changeset
|
309 |
Semiring_Normalization.thy \ |
| 27421 | 310 |
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
|
311 |
Sledgehammer.thy \ |
| 36898 | 312 |
SMT.thy \ |
|
31048
ac146fc38b51
refined HOL string theories and corresponding ML fragments
haftmann
parents:
31036
diff
changeset
|
313 |
String.thy \ |
|
31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
31186
diff
changeset
|
314 |
Typerep.thy \ |
| 27421 | 315 |
$(SRC)/Provers/Arith/assoc_fold.ML \ |
316 |
$(SRC)/Provers/Arith/cancel_numeral_factor.ML \ |
|
317 |
$(SRC)/Provers/Arith/cancel_numerals.ML \ |
|
318 |
$(SRC)/Provers/Arith/combine_numerals.ML \ |
|
319 |
$(SRC)/Provers/Arith/extract_common_term.ML \ |
|
|
33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33298
diff
changeset
|
320 |
Tools/choice_specification.ML \ |
| 39564 | 321 |
Tools/code_evaluation.ML \ |
| 41919 | 322 |
Tools/groebner.ML \ |
|
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31060
diff
changeset
|
323 |
Tools/int_arith.ML \ |
|
31055
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
31048
diff
changeset
|
324 |
Tools/list_code.ML \ |
|
41463
edbf0a86fb1c
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
bulwahn
parents:
41426
diff
changeset
|
325 |
Tools/list_to_set_comprehension.ML \ |
|
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31060
diff
changeset
|
326 |
Tools/nat_numeral_simprocs.ML \ |
|
36915
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
327 |
Tools/Nitpick/kodkod.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
328 |
Tools/Nitpick/kodkod_sat.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
329 |
Tools/Nitpick/nitpick.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
330 |
Tools/Nitpick/nitpick_hol.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
331 |
Tools/Nitpick/nitpick_isar.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
332 |
Tools/Nitpick/nitpick_kodkod.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
333 |
Tools/Nitpick/nitpick_model.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
334 |
Tools/Nitpick/nitpick_mono.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
335 |
Tools/Nitpick/nitpick_nut.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
336 |
Tools/Nitpick/nitpick_peephole.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
337 |
Tools/Nitpick/nitpick_preproc.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
338 |
Tools/Nitpick/nitpick_rep.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
339 |
Tools/Nitpick/nitpick_scope.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
340 |
Tools/Nitpick/nitpick_tests.ML \ |
|
7c429a484c74
move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong
blanchet
parents:
36901
diff
changeset
|
341 |
Tools/Nitpick/nitpick_util.ML \ |
| 27421 | 342 |
Tools/numeral.ML \ |
|
31068
f591144b0f17
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
haftmann
parents:
31060
diff
changeset
|
343 |
Tools/numeral_simprocs.ML \ |
| 27421 | 344 |
Tools/numeral_syntax.ML \ |
|
40141
0e8a4e27a685
adding new predicate compiler files to the IsaMakefile
bulwahn
parents:
40123
diff
changeset
|
345 |
Tools/Predicate_Compile/core_data.ML \ |
|
0e8a4e27a685
adding new predicate compiler files to the IsaMakefile
bulwahn
parents:
40123
diff
changeset
|
346 |
Tools/Predicate_Compile/mode_inference.ML \ |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33210
diff
changeset
|
347 |
Tools/Predicate_Compile/predicate_compile_aux.ML \ |
|
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
36032
diff
changeset
|
348 |
Tools/Predicate_Compile/predicate_compile_compilations.ML \ |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33210
diff
changeset
|
349 |
Tools/Predicate_Compile/predicate_compile_core.ML \ |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33210
diff
changeset
|
350 |
Tools/Predicate_Compile/predicate_compile_data.ML \ |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33210
diff
changeset
|
351 |
Tools/Predicate_Compile/predicate_compile_fun.ML \ |
|
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33210
diff
changeset
|
352 |
Tools/Predicate_Compile/predicate_compile.ML \ |
|
40141
0e8a4e27a685
adding new predicate compiler files to the IsaMakefile
bulwahn
parents:
40123
diff
changeset
|
353 |
Tools/Predicate_Compile/predicate_compile_proof.ML \ |
|
36032
dfd30b5b4e73
adding specialisation of predicates to the predicate compiler
bulwahn
parents:
35972
diff
changeset
|
354 |
Tools/Predicate_Compile/predicate_compile_specialisation.ML \ |
|
33250
5c2af18a3237
including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck
bulwahn
parents:
33210
diff
changeset
|
355 |
Tools/Predicate_Compile/predicate_compile_pred.ML \ |
| 27421 | 356 |
Tools/Qelim/cooper.ML \ |
| 36803 | 357 |
Tools/Qelim/cooper_procedure.ML \ |
| 27421 | 358 |
Tools/Qelim/qelim.ML \ |
|
41920
d4fb7a418152
moving exhaustive_generators.ML to Quickcheck directory
bulwahn
parents:
41919
diff
changeset
|
359 |
Tools/Quickcheck/exhaustive_generators.ML \ |
| 41924 | 360 |
Tools/Quickcheck/random_generators.ML \ |
|
41928
05abcee548a1
adaptions in generators using the common functions
bulwahn
parents:
41927
diff
changeset
|
361 |
Tools/Quickcheck/quickcheck_common.ML \ |
| 43310 | 362 |
Tools/Quickcheck/narrowing_generators.ML \ |
363 |
Tools/Quickcheck/Narrowing_Engine.hs \ |
|
364 |
Tools/Quickcheck/PNF_Narrowing_Engine.hs \ |
|
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
365 |
Tools/Quotient/quotient_def.ML \ |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
366 |
Tools/Quotient/quotient_info.ML \ |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
367 |
Tools/Quotient/quotient_tacs.ML \ |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
368 |
Tools/Quotient/quotient_term.ML \ |
| 45680 | 369 |
Tools/Quotient/quotient_type.ML \ |
|
38394
3142c1e21a0e
moved Record.thy from session Plain to Main; avoid variable name acc
haftmann
parents:
38282
diff
changeset
|
370 |
Tools/record.ML \ |
|
36753
5cf4e9128f22
renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents:
36751
diff
changeset
|
371 |
Tools/semiring_normalizer.ML \ |
|
41042
8275f52ac991
load "try" after "Metis" and move "Async_Manager" back to Sledgehammer
blanchet
parents:
41023
diff
changeset
|
372 |
Tools/Sledgehammer/async_manager.ML \ |
| 38986 | 373 |
Tools/Sledgehammer/sledgehammer_filter.ML \ |
374 |
Tools/Sledgehammer/sledgehammer_minimize.ML \ |
|
|
35866
513074557e06
move the Sledgehammer Isar commands together into one file;
blanchet
parents:
35865
diff
changeset
|
375 |
Tools/Sledgehammer/sledgehammer_isar.ML \ |
|
41087
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41065
diff
changeset
|
376 |
Tools/Sledgehammer/sledgehammer_provers.ML \ |
|
d7b5fd465198
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
blanchet
parents:
41065
diff
changeset
|
377 |
Tools/Sledgehammer/sledgehammer_run.ML \ |
| 35967 | 378 |
Tools/Sledgehammer/sledgehammer_util.ML \ |
| 36898 | 379 |
Tools/SMT/smtlib_interface.ML \ |
| 40277 | 380 |
Tools/SMT/smt_builtin.ML \ |
|
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40420
diff
changeset
|
381 |
Tools/SMT/smt_config.ML \ |
|
41426
09615ed31f04
re-implemented support for datatypes (including records and typedefs);
boehmes
parents:
41413
diff
changeset
|
382 |
Tools/SMT/smt_datatypes.ML \ |
|
40424
7550b2cba1cb
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents:
40420
diff
changeset
|
383 |
Tools/SMT/smt_failure.ML \ |
| 36898 | 384 |
Tools/SMT/smt_normalize.ML \ |
|
40162
7f58a9a843c2
joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents:
40141
diff
changeset
|
385 |
Tools/SMT/smt_setup_solvers.ML \ |
| 36898 | 386 |
Tools/SMT/smt_solver.ML \ |
387 |
Tools/SMT/smt_translate.ML \ |
|
|
40662
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40650
diff
changeset
|
388 |
Tools/SMT/smt_utils.ML \ |
| 36898 | 389 |
Tools/SMT/z3_interface.ML \ |
390 |
Tools/SMT/z3_model.ML \ |
|
391 |
Tools/SMT/z3_proof_literals.ML \ |
|
|
40662
798aad2229c0
added prove reconstruction for injective functions;
boehmes
parents:
40650
diff
changeset
|
392 |
Tools/SMT/z3_proof_methods.ML \ |
| 36898 | 393 |
Tools/SMT/z3_proof_parser.ML \ |
394 |
Tools/SMT/z3_proof_reconstruction.ML \ |
|
395 |
Tools/SMT/z3_proof_tools.ML \ |
|
|
31055
2cf6efca6c71
proper structures for list and string code generation stuff
haftmann
parents:
31048
diff
changeset
|
396 |
Tools/string_code.ML \ |
| 27421 | 397 |
Tools/string_syntax.ML \ |
|
33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33298
diff
changeset
|
398 |
Tools/transfer.ML \ |
| 28401 | 399 |
|
400 |
$(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES) |
|
| 28500 | 401 |
@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main |
| 28401 | 402 |
|
|
34205
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
403 |
HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \ |
| 30096 | 404 |
Archimedean_Field.thy \ |
|
32733
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32674
diff
changeset
|
405 |
Complex.thy \ |
|
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset
|
406 |
Complex_Main.thy \ |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset
|
407 |
Deriv.thy \ |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset
|
408 |
Fact.thy \ |
| 32479 | 409 |
GCD.thy \ |
|
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset
|
410 |
Lim.thy \ |
| 31352 | 411 |
Limits.thy \ |
|
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset
|
412 |
Ln.thy \ |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset
|
413 |
Log.thy \ |
| 32479 | 414 |
Lubs.thy \ |
|
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset
|
415 |
MacLaurin.thy \ |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset
|
416 |
NthRoot.thy \ |
|
32733
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32674
diff
changeset
|
417 |
Parity.thy \ |
|
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32674
diff
changeset
|
418 |
RComplete.thy \ |
| 35372 | 419 |
Rat.thy \ |
|
32733
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32674
diff
changeset
|
420 |
Real.thy \ |
|
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32674
diff
changeset
|
421 |
RealDef.thy \ |
|
71618deaf777
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
wenzelm
parents:
32674
diff
changeset
|
422 |
RealVector.thy \ |
|
29197
6d4cb27ed19c
adapted HOL source structure to distribution layout
haftmann
parents:
29181
diff
changeset
|
423 |
SEQ.thy \ |
|
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset
|
424 |
Series.thy \ |
|
33269
3b7e2dbbd684
New theory SupInf of the supremum and infimum operators for sets of reals.
paulson
parents:
33083
diff
changeset
|
425 |
SupInf.thy \ |
|
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset
|
426 |
Taylor.thy \ |
|
40839
48e01d16dd17
activate subtyping/coercions in theory Complex_Main;
wenzelm
parents:
40837
diff
changeset
|
427 |
Tools/SMT/smt_real.ML \ |
|
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28905
diff
changeset
|
428 |
Tools/float_syntax.ML \ |
|
40839
48e01d16dd17
activate subtyping/coercions in theory Complex_Main;
wenzelm
parents:
40837
diff
changeset
|
429 |
Transcendental.thy |
|
34205
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
430 |
|
|
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
431 |
$(OUT)/HOL: ROOT.ML $(HOL_DEPENDENCIES) |
|
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
432 |
@$(ISABELLE_TOOL) usedir -b -g true $(OUT)/Pure HOL |
|
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
433 |
|
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
7513
diff
changeset
|
434 |
|
| 10255 | 435 |
## HOL-Library |
436 |
||
|
37691
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
437 |
HOL-Library: HOL $(OUT)/HOL-Library |
| 10255 | 438 |
|
|
38137
6fda94059baa
renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents:
38119
diff
changeset
|
439 |
$(OUT)/HOL-Library: $(OUT)/HOL Library/ROOT.ML \ |
|
37691
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
440 |
$(SRC)/HOL/Tools/float_arith.ML $(SRC)/Tools/float.ML \ |
|
37818
dd65033fed78
load cache_io before code generator; moved adhoc-overloading to generic tools
haftmann
parents:
37790
diff
changeset
|
441 |
Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy \ |
|
46238
9ace9e5b79be
renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)
bulwahn
parents:
46237
diff
changeset
|
442 |
Library/AList.thy Library/AList_Mapping.thy \ |
|
44897
787983a08bfb
moving connection of association lists to Mappings into a separate theory
bulwahn
parents:
44860
diff
changeset
|
443 |
Library/BigO.thy Library/Binomial.thy \ |
| 37968 | 444 |
Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy \ |
| 37662 | 445 |
Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy \ |
| 43919 | 446 |
Library/Code_Char_ord.thy Library/Code_Integer.thy \ |
447 |
Library/Code_Natural.thy Library/Code_Prolog.thy \ |
|
| 45483 | 448 |
Library/Code_Real_Approx_By_Float.thy \ |
| 43919 | 449 |
Tools/Predicate_Compile/code_prolog.ML Library/ContNotDenum.thy \ |
|
44236
b73b7832b384
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents:
44145
diff
changeset
|
450 |
Library/Cset.thy Library/Cset_Monad.thy Library/Continuity.thy \ |
|
45748
cf79cc09cab4
remove Library/Diagonalize.thy, because Library/Nat_Bijection.thy includes all the same functionality
huffman
parents:
45716
diff
changeset
|
451 |
Library/Convex.thy Library/Countable.thy \ |
|
46238
9ace9e5b79be
renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)
bulwahn
parents:
46237
diff
changeset
|
452 |
Library/DAList.thy Library/Dlist.thy Library/Dlist_Cset.thy \ |
|
9ace9e5b79be
renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)
bulwahn
parents:
46237
diff
changeset
|
453 |
Library/Efficient_Nat.thy Library/Eval_Witness.thy \ |
|
44236
b73b7832b384
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents:
44145
diff
changeset
|
454 |
Library/Extended_Real.thy Library/Extended_Nat.thy Library/Float.thy \ |
| 43919 | 455 |
Library/Formal_Power_Series.thy Library/Fraction_Field.thy \ |
456 |
Library/FrechetDeriv.thy Library/Cset.thy Library/FuncSet.thy \ |
|
|
44236
b73b7832b384
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents:
44145
diff
changeset
|
457 |
Library/Function_Algebras.thy \ |
|
b73b7832b384
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents:
44145
diff
changeset
|
458 |
Library/Fundamental_Theorem_Algebra.thy Library/Glbs.thy \ |
|
b73b7832b384
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents:
44145
diff
changeset
|
459 |
Library/Indicator_Function.thy Library/Infinite_Set.thy \ |
|
b73b7832b384
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents:
44145
diff
changeset
|
460 |
Library/Inner_Product.thy Library/Kleene_Algebra.thy \ |
|
b73b7832b384
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents:
44145
diff
changeset
|
461 |
Library/LaTeXsugar.thy Library/Lattice_Algebras.thy \ |
|
b73b7832b384
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents:
44145
diff
changeset
|
462 |
Library/Lattice_Syntax.thy Library/Library.thy Library/List_Cset.thy \ |
|
b73b7832b384
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents:
44145
diff
changeset
|
463 |
Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy \ |
|
45990
b7b905b23b2a
incorporated More_Set and More_List into the Main body -- to be consolidated later
haftmann
parents:
45985
diff
changeset
|
464 |
Library/Monad_Syntax.thy \ |
|
44236
b73b7832b384
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents:
44145
diff
changeset
|
465 |
Library/Multiset.thy Library/Nat_Bijection.thy \ |
|
b73b7832b384
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents:
44145
diff
changeset
|
466 |
Library/Numeral_Type.thy Library/Old_Recdef.thy \ |
|
b73b7832b384
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents:
44145
diff
changeset
|
467 |
Library/OptionalSugar.thy Library/Order_Relation.thy \ |
|
b73b7832b384
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents:
44145
diff
changeset
|
468 |
Library/Permutation.thy Library/Permutations.thy \ |
|
b73b7832b384
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents:
44145
diff
changeset
|
469 |
Library/Poly_Deriv.thy Library/Polynomial.thy \ |
|
b73b7832b384
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents:
44145
diff
changeset
|
470 |
Library/Predicate_Compile_Quickcheck.thy Library/Preorder.thy \ |
|
b73b7832b384
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents:
44145
diff
changeset
|
471 |
Library/Product_Vector.thy Library/Product_ord.thy \ |
|
b73b7832b384
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents:
44145
diff
changeset
|
472 |
Library/Product_plus.thy Library/Product_Lattice.thy \ |
|
b73b7832b384
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents:
44145
diff
changeset
|
473 |
Library/Quickcheck_Types.thy Library/Quotient_List.thy \ |
|
b73b7832b384
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents:
44145
diff
changeset
|
474 |
Library/Quotient_Option.thy Library/Quotient_Product.thy \ |
| 45074 | 475 |
Library/Quotient_Set.thy Library/Quotient_Sum.thy \ |
476 |
Library/Quotient_Syntax.thy Library/Quotient_Type.thy Library/RBT.thy \ |
|
477 |
Library/RBT_Impl.thy Library/RBT_Mapping.thy Library/README.html \ |
|
478 |
Library/Saturated.thy Library/Set_Algebras.thy \ |
|
479 |
Library/State_Monad.thy Library/Ramsey.thy \ |
|
|
44818
27ba81ad0890
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
44657
diff
changeset
|
480 |
Library/Reflection.thy Library/Sublist_Order.thy \ |
|
27ba81ad0890
theory of saturated naturals contributed by Peter Gammie
haftmann
parents:
44657
diff
changeset
|
481 |
Library/Sum_of_Squares.thy Library/Sum_of_Squares/sos_wrapper.ML \ |
| 41474 | 482 |
Library/Sum_of_Squares/sum_of_squares.ML \ |
|
42071
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
42064
diff
changeset
|
483 |
Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy \ |
|
44014
88bd7d74a2c1
moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef
krauss
parents:
44013
diff
changeset
|
484 |
Library/Wfrec.thy Library/While_Combinator.thy Library/Zorn.thy \ |
|
37818
dd65033fed78
load cache_io before code generator; moved adhoc-overloading to generic tools
haftmann
parents:
37790
diff
changeset
|
485 |
$(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML \ |
| 37789 | 486 |
Library/reflection.ML Library/reify_data.ML \ |
|
44013
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
44006
diff
changeset
|
487 |
Library/document/root.bib Library/document/root.tex \ |
|
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
44006
diff
changeset
|
488 |
Tools/TFL/casesplit.ML Tools/TFL/dcterm.ML Tools/TFL/post.ML \ |
|
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
44006
diff
changeset
|
489 |
Tools/TFL/rules.ML Tools/TFL/tfl.ML Tools/TFL/thms.ML \ |
|
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
44006
diff
changeset
|
490 |
Tools/TFL/thry.ML Tools/TFL/usyntax.ML Tools/TFL/utils.ML \ |
|
5cfc1c36ae97
moved recdef package to HOL/Library/Old_Recdef.thy
krauss
parents:
44006
diff
changeset
|
491 |
Tools/recdef.ML |
|
38137
6fda94059baa
renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
wenzelm
parents:
38119
diff
changeset
|
492 |
@cd Library; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL-Library |
| 10255 | 493 |
|
494 |
||
|
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset
|
495 |
## HOL-Hahn_Banach |
| 27421 | 496 |
|
|
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset
|
497 |
HOL-Hahn_Banach: HOL $(LOG)/HOL-Hahn_Banach.gz |
| 27421 | 498 |
|
|
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset
|
499 |
$(LOG)/HOL-Hahn_Banach.gz: $(OUT)/HOL Hahn_Banach/Bounds.thy \ |
|
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset
|
500 |
Hahn_Banach/Function_Norm.thy Hahn_Banach/Function_Order.thy \ |
|
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset
|
501 |
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
|
502 |
Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Hahn_Banach/Linearform.thy \ |
|
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset
|
503 |
Hahn_Banach/Normed_Space.thy Hahn_Banach/README.html \ |
|
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset
|
504 |
Hahn_Banach/ROOT.ML Hahn_Banach/Subspace.thy \ |
|
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset
|
505 |
Hahn_Banach/Vector_Space.thy Hahn_Banach/Zorn_Lemma.thy \ |
|
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset
|
506 |
Hahn_Banach/document/root.bib Hahn_Banach/document/root.tex |
|
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
31771
diff
changeset
|
507 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hahn_Banach |
| 27421 | 508 |
|
509 |
||
| 4518 | 510 |
## HOL-Induct |
| 2473 | 511 |
|
| 4518 | 512 |
HOL-Induct: HOL $(LOG)/HOL-Induct.gz |
| 3125 | 513 |
|
|
33688
1a97dcd8dc6a
moved old SList, LList, LFilter to AFP/Lazy-Lists-II;
wenzelm
parents:
33649
diff
changeset
|
514 |
$(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
|
515 |
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
|
516 |
Induct/QuoDataType.thy Induct/ROOT.ML Induct/Sexp.thy \ |
| 35249 | 517 |
Induct/Sigma_Algebra.thy Induct/ABexp.thy Induct/SList.thy \ |
518 |
Induct/Term.thy Induct/Tree.thy Induct/document/root.tex |
|
| 28500 | 519 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Induct |
| 3125 | 520 |
|
521 |
||
| 4518 | 522 |
## HOL-IMP |
523 |
||
| 43917 | 524 |
HOL-IMP: HOL $(OUT)/HOL-IMP |
| 2448 | 525 |
|
| 45112 | 526 |
$(OUT)/HOL-IMP: $(OUT)/HOL \ |
| 45747 | 527 |
IMP/ACom.thy IMP/Abs_Int0_fun.thy IMP/Abs_State.thy IMP/Abs_Int0.thy \ |
| 45112 | 528 |
IMP/Abs_Int0_const.thy IMP/Abs_Int1.thy IMP/Abs_Int1_ivl.thy \ |
529 |
IMP/Abs_Int2.thy IMP/Abs_Int_Den/Abs_Int_den0_fun.thy \ |
|
| 45111 | 530 |
IMP/Abs_Int_Den/Abs_State_den.thy IMP/Abs_Int_Den/Abs_Int_den0.thy \ |
531 |
IMP/Abs_Int_Den/Abs_Int_den0_const.thy IMP/Abs_Int_Den/Abs_Int_den1.thy \ |
|
532 |
IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy IMP/Abs_Int_Den/Abs_Int_den2.thy \ |
|
| 45885 | 533 |
IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy IMP/Big_Step.thy IMP/C_like.thy \ |
| 46232 | 534 |
IMP/Collecting.thy IMP/Collecting_list.thy IMP/Collecting1.thy IMP/Com.thy \ |
535 |
IMP/Compiler.thy IMP/Comp_Rev.thy \ |
|
536 |
IMP/Def_Ass.thy IMP/Def_Ass_Big.thy IMP/Def_Ass_Exp.thy \ |
|
| 43158 | 537 |
IMP/Def_Ass_Small.thy IMP/Def_Ass_Sound_Big.thy \ |
538 |
IMP/Def_Ass_Sound_Small.thy IMP/Denotation.thy IMP/Hoare.thy \ |
|
539 |
IMP/HoareT.thy IMP/Hoare_Examples.thy IMP/Hoare_Sound_Complete.thy \ |
|
| 45812 | 540 |
IMP/Live.thy IMP/Live_True.thy IMP/OO.thy IMP/Poly_Types.thy IMP/Procs.thy \ |
| 43158 | 541 |
IMP/Procs_Dyn_Vars_Dyn.thy IMP/Procs_Stat_Vars_Dyn.thy \ |
542 |
IMP/Procs_Stat_Vars_Stat.thy IMP/Sec_Type_Expr.thy IMP/Sec_Typing.thy \ |
|
543 |
IMP/Sec_TypingT.thy IMP/Small_Step.thy IMP/Star.thy IMP/Types.thy \ |
|
| 45716 | 544 |
IMP/VC.thy IMP/Vars.thy \ |
| 27164 | 545 |
IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib |
|
45320
9d7b52c8eb01
moved latex generation for HOL-IMP out of distribution
kleing
parents:
45319
diff
changeset
|
546 |
@cd IMP && $(ISABELLE_TOOL) usedir -g true -b $(OUT)/HOL HOL-IMP |
| 2448 | 547 |
|
| 8179 | 548 |
## HOL-IMPP |
549 |
||
550 |
HOL-IMPP: HOL $(LOG)/HOL-IMPP.gz |
|
551 |
||
| 27164 | 552 |
$(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy \ |
| 19803 | 553 |
IMPP/Natural.thy IMPP/Hoare.thy IMPP/Misc.thy IMPP/EvenOdd.thy |
| 28500 | 554 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL IMPP |
| 8179 | 555 |
|
556 |
||
| 46785 | 557 |
## Import sessions |
558 |
||
| 46808 | 559 |
IMPORTER_BASIC_DEPENDENCIES = \ |
560 |
Import/Importer.thy \ |
|
| 46806 | 561 |
Import/shuffler.ML \ |
562 |
Import/import_rews.ML \ |
|
563 |
Import/proof_kernel.ML \ |
|
564 |
Import/replay.ML \ |
|
565 |
Import/import.ML |
|
| 46795 | 566 |
|
| 46808 | 567 |
IMPORTER_HOL4_COMPATIBILITY_DEDEPENDENCIES = \ |
| 46785 | 568 |
Import/HOL4/ROOT.ML \ |
569 |
Import/HOL4/Compatibility.thy |
|
| 14516 | 570 |
|
| 46808 | 571 |
IMPORTER_HOL_LIGHT_COMPATIBILITY_DEDEPENDENCIES = \ |
| 46785 | 572 |
Import/HOL_Light/ROOT.ML \ |
| 46795 | 573 |
Import/HOL_Light/HOLLightInt.thy \ |
574 |
Import/HOL_Light/HOLLightList.thy \ |
|
575 |
Import/HOL_Light/HOLLightReal.thy \ |
|
| 46785 | 576 |
Import/HOL_Light/Compatibility.thy |
| 46808 | 577 |
|
578 |
HOL-HOL4: $(LOG)/HOL-HOL4.gz |
|
579 |
||
580 |
$(LOG)/HOL-HOL4.gz: $(OUT)/HOL \ |
|
581 |
$(IMPORTER_BASIC_DEPENDENCIES) \ |
|
582 |
$(IMPORTER_HOL4_COMPATIBILITY_DEDEPENDENCIES) |
|
583 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Import/HOL4 |
|
584 |
||
585 |
HOL-HOL_Light: $(LOG)/HOL-HOL_Light.gz |
|
| 14516 | 586 |
|
| 46808 | 587 |
$(LOG)/HOL-HOL_Light.gz: $(OUT)/HOL \ |
588 |
$(IMPORTER_BASIC_DEPENDENCIES) \ |
|
589 |
$(IMPORTER_HOL_LIGHT_COMPATIBILITY_DEDEPENDENCIES) |
|
590 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Import/HOL_Light |
|
| 17323 | 591 |
|
| 46808 | 592 |
HOL-HOL4-Imported: $(LOG)/HOL-HOL4-Imported.gz |
593 |
||
594 |
$(LOG)/HOL-HOL4-Imported.gz: $(OUT)/HOL \ |
|
595 |
$(IMPORTER_BASIC_DEPENDENCIES) \ |
|
596 |
$(IMPORTER_HOL4_COMPATIBILITY_DEDEPENDENCIES) \ |
|
| 46785 | 597 |
Import/HOL4/imported.ML \ |
| 46795 | 598 |
Import/HOL4/Imported.thy \ |
599 |
Import/HOL4/Generated/HOL4Base.thy \ |
|
600 |
Import/HOL4/Generated/HOL4Prob.thy \ |
|
601 |
Import/HOL4/Generated/HOL4Real.thy \ |
|
602 |
Import/HOL4/Generated/HOL4Vec.thy \ |
|
603 |
Import/HOL4/Generated/HOL4Word32.thy \ |
|
604 |
Import/HOL4/Generated/arithmetic.imp \ |
|
605 |
Import/HOL4/Generated/bits.imp \ |
|
606 |
Import/HOL4/Generated/boolean_sequence.imp \ |
|
607 |
Import/HOL4/Generated/bool.imp \ |
|
608 |
Import/HOL4/Generated/bword_arith.imp \ |
|
609 |
Import/HOL4/Generated/bword_bitop.imp \ |
|
610 |
Import/HOL4/Generated/bword_num.imp \ |
|
611 |
Import/HOL4/Generated/combin.imp \ |
|
612 |
Import/HOL4/Generated/divides.imp \ |
|
613 |
Import/HOL4/Generated/hrat.imp \ |
|
614 |
Import/HOL4/Generated/hreal.imp \ |
|
615 |
Import/HOL4/Generated/ind_type.imp \ |
|
616 |
Import/HOL4/Generated/lim.imp \ |
|
617 |
Import/HOL4/Generated/list.imp \ |
|
618 |
Import/HOL4/Generated/marker.imp \ |
|
619 |
Import/HOL4/Generated/nets.imp \ |
|
620 |
Import/HOL4/Generated/numeral.imp \ |
|
621 |
Import/HOL4/Generated/num.imp \ |
|
622 |
Import/HOL4/Generated/one.imp \ |
|
623 |
Import/HOL4/Generated/operator.imp \ |
|
624 |
Import/HOL4/Generated/option.imp \ |
|
625 |
Import/HOL4/Generated/pair.imp \ |
|
626 |
Import/HOL4/Generated/poly.imp \ |
|
627 |
Import/HOL4/Generated/powser.imp \ |
|
628 |
Import/HOL4/Generated/pred_set.imp \ |
|
629 |
Import/HOL4/Generated/prime.imp \ |
|
630 |
Import/HOL4/Generated/prim_rec.imp \ |
|
631 |
Import/HOL4/Generated/prob_algebra.imp \ |
|
632 |
Import/HOL4/Generated/prob_canon.imp \ |
|
633 |
Import/HOL4/Generated/prob_extra.imp \ |
|
634 |
Import/HOL4/Generated/prob.imp \ |
|
635 |
Import/HOL4/Generated/prob_indep.imp \ |
|
636 |
Import/HOL4/Generated/prob_pseudo.imp \ |
|
637 |
Import/HOL4/Generated/prob_uniform.imp \ |
|
638 |
Import/HOL4/Generated/realax.imp \ |
|
639 |
Import/HOL4/Generated/real.imp \ |
|
640 |
Import/HOL4/Generated/relation.imp \ |
|
641 |
Import/HOL4/Generated/res_quan.imp \ |
|
642 |
Import/HOL4/Generated/rich_list.imp \ |
|
643 |
Import/HOL4/Generated/seq.imp \ |
|
644 |
Import/HOL4/Generated/state_transformer.imp \ |
|
645 |
Import/HOL4/Generated/sum.imp \ |
|
646 |
Import/HOL4/Generated/topology.imp \ |
|
647 |
Import/HOL4/Generated/transc.imp \ |
|
648 |
Import/HOL4/Generated/word32.imp \ |
|
649 |
Import/HOL4/Generated/word_base.imp \ |
|
650 |
Import/HOL4/Generated/word_bitop.imp \ |
|
651 |
Import/HOL4/Generated/word_num.imp |
|
| 46808 | 652 |
@$(ISABELLE_TOOL) usedir -f imported.ML -s HOL4-Imported -p 0 $(OUT)/HOL Import/HOL4 |
653 |
||
654 |
HOL-HOL_Light-Imported: $(LOG)/HOL-HOL_Light-Imported.gz |
|
| 14516 | 655 |
|
| 46808 | 656 |
$(LOG)/HOL-HOL_Light-Imported.gz: $(OUT)/HOL \ |
657 |
$(IMPORTER_BASIC_DEPENDENCIES) \ |
|
658 |
$(IMPORTER_HOL_LIGHT_COMPATIBILITY_DEDEPENDENCIES) \ |
|
| 46785 | 659 |
Import/HOL_Light/imported.ML \ |
| 46795 | 660 |
Import/HOL_Light/Imported.thy \ |
661 |
Import/HOL_Light/Generated/HOLLight.thy \ |
|
662 |
Import/HOL_Light/Generated/hollight.imp |
|
| 46808 | 663 |
@$(ISABELLE_TOOL) usedir -f imported.ML -s HOL_Light-Imported -p 0 $(OUT)/HOL Import/HOL_Light |
664 |
||
665 |
HOL-HOL4-Generate: $(LOG)/Import-HOL4-Generate.gz |
|
| 14516 | 666 |
|
| 46808 | 667 |
$(LOG)/Import-HOL4-Generate.gz: $(OUT)/HOL \ |
668 |
$(IMPORTER_BASIC_DEPENDENCIES) \ |
|
669 |
$(IMPORTER_HOL4_COMPATIBILITY_DEDEPENDENCIES) \ |
|
| 46785 | 670 |
Import/HOL4/generate.ML \ |
| 46795 | 671 |
Import/HOL4/Generate.thy \ |
672 |
Import/HOL4/Template/GenHOL4Base.thy \ |
|
673 |
Import/HOL4/Template/GenHOL4Prob.thy \ |
|
674 |
Import/HOL4/Template/GenHOL4Real.thy \ |
|
675 |
Import/HOL4/Template/GenHOL4Vec.thy \ |
|
676 |
Import/HOL4/Template/GenHOL4Word32.thy |
|
| 46808 | 677 |
@$(ISABELLE_TOOL) usedir -f generate.ML -s HOL4-Generate -p 0 $(OUT)/HOL Import/HOL4 |
678 |
||
679 |
HOL-HOL_Light-Generate: $(LOG)/Import-HOL_Light-Generate.gz |
|
| 14516 | 680 |
|
| 46808 | 681 |
$(LOG)/Import-HOL_Light-Generate.gz: $(OUT)/HOL \ |
682 |
$(IMPORTER_BASIC_DEPENDENCIES) \ |
|
683 |
$(IMPORTER_HOL_LIGHT_COMPATIBILITY_DEDEPENDENCIES) \ |
|
| 46785 | 684 |
Import/HOL_Light/generate.ML \ |
| 46795 | 685 |
Import/HOL_Light/Generate.thy \ |
686 |
Import/HOL_Light/Template/GenHOLLight.thy |
|
| 46808 | 687 |
@$(ISABELLE_TOOL) usedir -f generate.ML -s HOL_Light-Generate -p 0 $(OUT)/HOL Import/HOL_Light |
| 17645 | 688 |
|
| 14516 | 689 |
|
| 32479 | 690 |
## HOL-Number_Theory |
| 31719 | 691 |
|
| 32479 | 692 |
HOL-Number_Theory: HOL $(LOG)/HOL-Number_Theory.gz |
| 31719 | 693 |
|
| 32479 | 694 |
$(LOG)/HOL-Number_Theory.gz: $(OUT)/HOL $(ALGEBRA_DEPENDENCIES) \ |
| 31771 | 695 |
Library/Multiset.thy \ |
| 32479 | 696 |
Number_Theory/Binomial.thy \ |
697 |
Number_Theory/Cong.thy \ |
|
698 |
Number_Theory/Fib.thy \ |
|
699 |
Number_Theory/MiscAlgebra.thy \ |
|
700 |
Number_Theory/Number_Theory.thy \ |
|
701 |
Number_Theory/Residues.thy \ |
|
702 |
Number_Theory/UniqueFactorization.thy \ |
|
703 |
Number_Theory/ROOT.ML |
|
704 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Number_Theory |
|
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
41973
diff
changeset
|
705 |
|
| 31719 | 706 |
|
| 32479 | 707 |
## HOL-Old_Number_Theory |
| 9510 | 708 |
|
| 32479 | 709 |
HOL-Old_Number_Theory: HOL $(LOG)/HOL-Old_Number_Theory.gz |
| 9510 | 710 |
|
| 37021 | 711 |
$(LOG)/HOL-Old_Number_Theory.gz: $(OUT)/HOL Library/Permutation.thy \ |
712 |
Old_Number_Theory/Primes.thy Old_Number_Theory/Fib.thy \ |
|
713 |
Old_Number_Theory/Factorization.thy Old_Number_Theory/BijectionRel.thy\ |
|
714 |
Old_Number_Theory/Chinese.thy Old_Number_Theory/EulerFermat.thy \ |
|
715 |
Old_Number_Theory/IntFact.thy Old_Number_Theory/IntPrimes.thy \ |
|
716 |
Old_Number_Theory/WilsonBij.thy Old_Number_Theory/WilsonRuss.thy \ |
|
717 |
Old_Number_Theory/Finite2.thy Old_Number_Theory/Int2.thy \ |
|
718 |
Old_Number_Theory/EvenOdd.thy Old_Number_Theory/Residues.thy \ |
|
719 |
Old_Number_Theory/Euler.thy Old_Number_Theory/Gauss.thy \ |
|
| 32479 | 720 |
Old_Number_Theory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy \ |
| 37021 | 721 |
Old_Number_Theory/Legacy_GCD.thy Old_Number_Theory/Pocklington.thy \ |
722 |
Old_Number_Theory/ROOT.ML |
|
| 32479 | 723 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Old_Number_Theory |
| 9510 | 724 |
|
725 |
||
| 4518 | 726 |
## HOL-Hoare |
727 |
||
728 |
HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz |
|
| 2448 | 729 |
|
| 27164 | 730 |
$(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.thy Hoare/Examples.thy \ |
| 42153 | 731 |
Hoare/Hoare.thy Hoare/hoare_syntax.ML Hoare/hoare_tac.ML \ |
732 |
Hoare/Heap.thy Hoare/Hoare_Logic.thy Hoare/Hoare_Logic_Abort.thy \ |
|
| 27164 | 733 |
Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy Hoare/ROOT.ML \ |
734 |
Hoare/ExamplesAbort.thy Hoare/HeapSyntaxAbort.thy \ |
|
| 42153 | 735 |
Hoare/SchorrWaite.thy Hoare/Separation.thy Hoare/SepLogHeap.thy \ |
736 |
Hoare/document/root.tex Hoare/document/root.bib |
|
| 28500 | 737 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Hoare |
| 2448 | 738 |
|
739 |
||
|
32621
a073cb249a06
theory entry point for session Hoare_Parallel (now also with proper underscore)
haftmann
parents:
32618
diff
changeset
|
740 |
## HOL-Hoare_Parallel |
| 12996 | 741 |
|
|
32621
a073cb249a06
theory entry point for session Hoare_Parallel (now also with proper underscore)
haftmann
parents:
32618
diff
changeset
|
742 |
HOL-Hoare_Parallel: HOL $(LOG)/HOL-Hoare_Parallel.gz |
| 12996 | 743 |
|
|
32621
a073cb249a06
theory entry point for session Hoare_Parallel (now also with proper underscore)
haftmann
parents:
32618
diff
changeset
|
744 |
$(LOG)/HOL-Hoare_Parallel.gz: $(OUT)/HOL Hoare_Parallel/Gar_Coll.thy \ |
| 33439 | 745 |
Hoare_Parallel/Graph.thy Hoare_Parallel/Hoare_Parallel.thy \ |
746 |
Hoare_Parallel/Mul_Gar_Coll.thy Hoare_Parallel/OG_Com.thy \ |
|
747 |
Hoare_Parallel/OG_Examples.thy Hoare_Parallel/OG_Hoare.thy \ |
|
748 |
Hoare_Parallel/OG_Syntax.thy Hoare_Parallel/OG_Tactics.thy \ |
|
749 |
Hoare_Parallel/OG_Tran.thy Hoare_Parallel/Quote_Antiquote.thy \ |
|
750 |
Hoare_Parallel/RG_Com.thy Hoare_Parallel/RG_Examples.thy \ |
|
751 |
Hoare_Parallel/RG_Hoare.thy Hoare_Parallel/RG_Syntax.thy \ |
|
752 |
Hoare_Parallel/RG_Tran.thy Hoare_Parallel/ROOT.ML \ |
|
753 |
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
|
754 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hoare_Parallel |
| 12996 | 755 |
|
756 |
||
| 37747 | 757 |
## HOL-Library-Codegenerator_Test |
|
37691
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
758 |
|
| 37747 | 759 |
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
|
760 |
|
| 37747 | 761 |
$(LOG)/HOL-Library-Codegenerator_Test.gz: $(OUT)/HOL-Library \ |
| 37742 | 762 |
Codegenerator_Test/ROOT.ML \ |
763 |
Codegenerator_Test/Candidates.thy \ |
|
|
37691
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
764 |
Codegenerator_Test/Candidates_Pretty.thy \ |
|
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
765 |
Codegenerator_Test/Generate.thy \ |
|
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
766 |
Codegenerator_Test/Generate_Pretty.thy |
|
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
767 |
@$(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
|
768 |
|
|
4915de09b4d3
build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test
haftmann
parents:
37672
diff
changeset
|
769 |
|
| 33027 | 770 |
## HOL-Metis_Examples |
| 23449 | 771 |
|
| 33027 | 772 |
HOL-Metis_Examples: HOL $(LOG)/HOL-Metis_Examples.gz |
| 23449 | 773 |
|
| 41144 | 774 |
$(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML \ |
| 43197 | 775 |
Metis_Examples/Abstraction.thy Metis_Examples/Big_O.thy \ |
776 |
Metis_Examples/Binary_Tree.thy Metis_Examples/Clausification.thy \ |
|
777 |
Metis_Examples/Message.thy Metis_Examples/Proxies.thy \ |
|
778 |
Metis_Examples/Sets.thy Metis_Examples/Tarski.thy \ |
|
779 |
Metis_Examples/Trans_Closure.thy Metis_Examples/Type_Encodings.thy |
|
| 33027 | 780 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples |
| 23449 | 781 |
|
782 |
||
|
33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset
|
783 |
## HOL-Nitpick_Examples |
|
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset
|
784 |
|
|
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset
|
785 |
HOL-Nitpick_Examples: HOL $(LOG)/HOL-Nitpick_Examples.gz |
|
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset
|
786 |
|
| 34126 | 787 |
$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \ |
788 |
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
|
789 |
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
|
790 |
Nitpick_Examples/Integer_Nits.thy Nitpick_Examples/Manual_Nits.thy \ |
| 45035 | 791 |
Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy \ |
792 |
Nitpick_Examples/Nitpick_Examples.thy Nitpick_Examples/Pattern_Nits.thy \ |
|
793 |
Nitpick_Examples/Record_Nits.thy Nitpick_Examples/Refute_Nits.thy \ |
|
794 |
Nitpick_Examples/Special_Nits.thy Nitpick_Examples/Tests_Nits.thy \ |
|
795 |
Nitpick_Examples/Typedef_Nits.thy Nitpick_Examples/minipick.ML |
|
|
33197
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset
|
796 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples |
|
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset
|
797 |
|
|
de6285ebcc05
continuation of Nitpick's integration into Isabelle;
blanchet
parents:
33192
diff
changeset
|
798 |
|
|
7999
7acf6eb8eec1
Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
7985
diff
changeset
|
799 |
## HOL-Algebra |
|
7acf6eb8eec1
Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
7985
diff
changeset
|
800 |
|
| 33439 | 801 |
HOL-Algebra: HOL $(OUT)/HOL-Algebra |
|
7999
7acf6eb8eec1
Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
7985
diff
changeset
|
802 |
|
| 31771 | 803 |
ALGEBRA_DEPENDENCIES = $(OUT)/HOL \ |
804 |
Algebra/ROOT.ML \ |
|
805 |
Library/Binomial.thy \ |
|
806 |
Library/FuncSet.thy \ |
|
807 |
Library/Multiset.thy \ |
|
808 |
Library/Permutation.thy \ |
|
| 32479 | 809 |
Number_Theory/Primes.thy \ |
| 31771 | 810 |
Algebra/AbelCoset.thy \ |
811 |
Algebra/Bij.thy \ |
|
812 |
Algebra/Congruence.thy \ |
|
813 |
Algebra/Coset.thy \ |
|
814 |
Algebra/Divisibility.thy \ |
|
815 |
Algebra/Exponent.thy \ |
|
816 |
Algebra/FiniteProduct.thy \ |
|
817 |
Algebra/Group.thy \ |
|
818 |
Algebra/Ideal.thy \ |
|
819 |
Algebra/IntRing.thy \ |
|
820 |
Algebra/Lattice.thy \ |
|
821 |
Algebra/Module.thy \ |
|
822 |
Algebra/QuotRing.thy \ |
|
823 |
Algebra/Ring.thy \ |
|
824 |
Algebra/RingHom.thy \ |
|
825 |
Algebra/Sylow.thy \ |
|
826 |
Algebra/UnivPoly.thy \ |
|
827 |
Algebra/abstract/Abstract.thy \ |
|
828 |
Algebra/abstract/Factor.thy \ |
|
829 |
Algebra/abstract/Field.thy \ |
|
830 |
Algebra/abstract/Ideal2.thy \ |
|
831 |
Algebra/abstract/PID.thy \ |
|
832 |
Algebra/abstract/Ring2.thy \ |
|
833 |
Algebra/abstract/RingHomo.thy \ |
|
834 |
Algebra/document/root.tex \ |
|
835 |
Algebra/document/root.tex \ |
|
836 |
Algebra/poly/LongDiv.thy \ |
|
837 |
Algebra/poly/PolyHomo.thy \ |
|
838 |
Algebra/poly/Polynomial.thy \ |
|
839 |
Algebra/poly/UnivPoly2.thy \ |
|
840 |
Algebra/ringsimp.ML |
|
841 |
||
| 33448 | 842 |
$(OUT)/HOL-Algebra: $(ALGEBRA_DEPENDENCIES) |
| 28500 | 843 |
@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
|
844 |
|
|
27477
c64736fe2a1f
more precise dependencies for HOL-Word and HOL-NSA;
wenzelm
parents:
27470
diff
changeset
|
845 |
|
| 4518 | 846 |
## HOL-Auth |
| 3819 | 847 |
|
| 4518 | 848 |
HOL-Auth: HOL $(LOG)/HOL-Auth.gz |
| 3819 | 849 |
|
| 28098 | 850 |
$(LOG)/HOL-Auth.gz: $(OUT)/HOL \ |
| 37021 | 851 |
Auth/Auth_Shared.thy Auth/Auth_Public.thy Auth/All_Symmetric.thy \ |
852 |
Auth/Guard/Auth_Guard_Shared.thy \ |
|
853 |
Auth/Guard/Auth_Guard_Public.thy \ |
|
| 32632 | 854 |
Auth/Smartcard/Auth_Smartcard.thy Auth/All_Symmetric.thy \ |
| 27164 | 855 |
Auth/CertifiedEmail.thy Auth/Event.thy Auth/Message.thy \ |
856 |
Auth/NS_Public.thy Auth/NS_Public_Bad.thy Auth/NS_Shared.thy \ |
|
857 |
Auth/OtwayRees.thy Auth/OtwayReesBella.thy Auth/OtwayRees_AN.thy \ |
|
858 |
Auth/OtwayRees_Bad.thy Auth/Public.thy Auth/ROOT.ML Auth/Recur.thy \ |
|
859 |
Auth/Shared.thy Auth/TLS.thy Auth/WooLam.thy Auth/Kerberos_BAN.thy \ |
|
860 |
Auth/Kerberos_BAN_Gets.thy Auth/KerberosIV.thy \ |
|
861 |
Auth/KerberosIV_Gets.thy Auth/KerberosV.thy Auth/Yahalom.thy \ |
|
862 |
Auth/Yahalom2.thy Auth/Yahalom_Bad.thy Auth/ZhouGollmann.thy \ |
|
863 |
Auth/Guard/Analz.thy Auth/Guard/Extensions.thy Auth/Guard/GuardK.thy \ |
|
864 |
Auth/Guard/Guard_Public.thy Auth/Guard/Guard_Shared.thy \ |
|
865 |
Auth/Guard/Guard.thy Auth/Guard/List_Msg.thy \ |
|
866 |
Auth/Guard/Guard_NS_Public.thy Auth/Guard/Guard_OtwayRees.thy \ |
|
867 |
Auth/Guard/P1.thy Auth/Guard/P2.thy Auth/Guard/Proto.thy \ |
|
868 |
Auth/Guard/Guard_Yahalom.thy Auth/Smartcard/EventSC.thy \ |
|
869 |
Auth/Smartcard/ShoupRubinBella.thy Auth/Smartcard/ShoupRubin.thy \ |
|
870 |
Auth/Smartcard/Smartcard.thy Auth/document/root.tex |
|
| 28500 | 871 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Auth |
| 2448 | 872 |
|
873 |
||
| 4777 | 874 |
## HOL-UNITY |
875 |
||
876 |
HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz |
|
877 |
||
| 27164 | 878 |
$(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \ |
|
41892
2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;
wenzelm
parents:
41854
diff
changeset
|
879 |
UNITY/UNITY_Main.thy UNITY/UNITY_tactics.ML UNITY/Comp.thy \ |
|
2386fb64feaf
eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;
wenzelm
parents:
41854
diff
changeset
|
880 |
UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy \ |
| 27164 | 881 |
UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy UNITY/Guar.thy \ |
882 |
UNITY/Lift_prog.thy UNITY/ListOrder.thy UNITY/ProgressSets.thy \ |
|
883 |
UNITY/PPROD.thy UNITY/Project.thy UNITY/Rename.thy \ |
|
884 |
UNITY/Transformers.thy UNITY/SubstAx.thy UNITY/UNITY.thy \ |
|
885 |
UNITY/Union.thy UNITY/WFair.thy UNITY/Simple/Channel.thy \ |
|
886 |
UNITY/Simple/Common.thy UNITY/Simple/Deadlock.thy \ |
|
887 |
UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy \ |
|
888 |
UNITY/Simple/NSP_Bad.thy UNITY/Simple/Network.thy \ |
|
889 |
UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy \ |
|
890 |
UNITY/Simple/Token.thy UNITY/Comp/Alloc.thy UNITY/Comp/AllocBase.thy \ |
|
891 |
UNITY/Comp/AllocImpl.thy UNITY/Comp/Client.thy \ |
|
892 |
UNITY/Comp/Counter.thy UNITY/Comp/Counterc.thy \ |
|
893 |
UNITY/Comp/Handshake.thy UNITY/Comp/PriorityAux.thy \ |
|
894 |
UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \ |
|
895 |
UNITY/Comp/TimerArray.thy UNITY/document/root.tex |
|
| 28500 | 896 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL UNITY |
| 4777 | 897 |
|
898 |
||
| 10966 | 899 |
## HOL-Unix |
900 |
||
901 |
HOL-Unix: HOL $(LOG)/HOL-Unix.gz |
|
902 |
||
|
44236
b73b7832b384
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents:
44145
diff
changeset
|
903 |
$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/List_Prefix.thy Unix/ROOT.ML \ |
|
b73b7832b384
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents:
44145
diff
changeset
|
904 |
Unix/Nested_Environment.thy Unix/Unix.thy Unix/document/root.bib \ |
|
b73b7832b384
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
wenzelm
parents:
44145
diff
changeset
|
905 |
Unix/document/root.tex |
| 39156 | 906 |
@$(ISABELLE_TOOL) usedir -m no_brackets -m no_type_brackets $(OUT)/HOL Unix |
| 10966 | 907 |
|
|
27477
c64736fe2a1f
more precise dependencies for HOL-Word and HOL-NSA;
wenzelm
parents:
27470
diff
changeset
|
908 |
|
| 19203 | 909 |
## HOL-ZF |
910 |
||
911 |
HOL-ZF: HOL $(LOG)/HOL-ZF.gz |
|
912 |
||
|
39306
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
913 |
$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/LProd.thy \ |
| 27164 | 914 |
ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex |
| 28500 | 915 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF |
| 10966 | 916 |
|
|
27477
c64736fe2a1f
more precise dependencies for HOL-Word and HOL-NSA;
wenzelm
parents:
27470
diff
changeset
|
917 |
|
|
29399
ebcd69a00872
split of Imperative_HOL theories from HOL-Library
haftmann
parents:
29197
diff
changeset
|
918 |
## HOL-Imperative_HOL |
|
ebcd69a00872
split of Imperative_HOL theories from HOL-Library
haftmann
parents:
29197
diff
changeset
|
919 |
|
|
ebcd69a00872
split of Imperative_HOL theories from HOL-Library
haftmann
parents:
29197
diff
changeset
|
920 |
HOL-Imperative_HOL: HOL $(LOG)/HOL-Imperative_HOL.gz |
|
ebcd69a00872
split of Imperative_HOL theories from HOL-Library
haftmann
parents:
29197
diff
changeset
|
921 |
|
|
39306
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
922 |
$(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
923 |
Imperative_HOL/Array.thy \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
924 |
Imperative_HOL/Heap.thy \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
925 |
Imperative_HOL/Heap_Monad.thy \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
926 |
Imperative_HOL/Imperative_HOL.thy \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
927 |
Imperative_HOL/Imperative_HOL_ex.thy \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
928 |
Imperative_HOL/Mrec.thy \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
929 |
Imperative_HOL/Ref.thy \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
930 |
Imperative_HOL/ROOT.ML \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
931 |
Imperative_HOL/ex/Imperative_Quicksort.thy \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
932 |
Imperative_HOL/ex/Imperative_Reverse.thy \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
933 |
Imperative_HOL/ex/Linked_Lists.thy \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
934 |
Imperative_HOL/ex/SatChecker.thy \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
935 |
Imperative_HOL/ex/Sorted_List.thy \ |
|
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
936 |
Imperative_HOL/ex/Subarray.thy \ |
|
30689
b14b2cc4e25e
moved Imperative_HOL examples to Imperative_HOL/ex
haftmann
parents:
30654
diff
changeset
|
937 |
Imperative_HOL/ex/Sublist.thy |
|
39306
c1f3992c9097
print mode for Imperative HOL overview; tuned and more accurate dependencies
haftmann
parents:
39271
diff
changeset
|
938 |
@$(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
|
939 |
|
|
ebcd69a00872
split of Imperative_HOL theories from HOL-Library
haftmann
parents:
29197
diff
changeset
|
940 |
|
|
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
941 |
## HOL-Decision_Procs |
|
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
942 |
|
|
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
943 |
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
|
944 |
|
|
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
945 |
$(LOG)/HOL-Decision_Procs.gz: $(OUT)/HOL \ |
|
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
946 |
Decision_Procs/Approximation.thy \ |
|
33356
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
33348
diff
changeset
|
947 |
Decision_Procs/Commutative_Ring.thy \ |
|
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
33348
diff
changeset
|
948 |
Decision_Procs/Commutative_Ring_Complete.thy \ |
|
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
949 |
Decision_Procs/Cooper.thy \ |
| 35053 | 950 |
Decision_Procs/Decision_Procs.thy \ |
|
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
951 |
Decision_Procs/Dense_Linear_Order.thy \ |
|
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
952 |
Decision_Procs/Ferrack.thy \ |
|
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
953 |
Decision_Procs/MIR.thy \ |
| 35053 | 954 |
Decision_Procs/Parametric_Ferrante_Rackoff.thy \ |
955 |
Decision_Procs/Polynomial_List.thy \ |
|
| 37120 | 956 |
Decision_Procs/ROOT.ML \ |
| 35053 | 957 |
Decision_Procs/Reflected_Multivariate_Polynomial.thy \ |
958 |
Decision_Procs/commutative_ring_tac.ML \ |
|
959 |
Decision_Procs/cooper_tac.ML \ |
|
|
30429
39acdf031548
moved Decision_Procs examples to Decision_Procs/ex
haftmann
parents:
30400
diff
changeset
|
960 |
Decision_Procs/ex/Approximation_Ex.thy \ |
|
33356
9157d0f9f00e
moved Commutative_Ring into session Decision_Procs
haftmann
parents:
33348
diff
changeset
|
961 |
Decision_Procs/ex/Commutative_Ring_Ex.thy \ |
| 35053 | 962 |
Decision_Procs/ex/Dense_Linear_Order_Ex.thy \ |
963 |
Decision_Procs/ferrack_tac.ML \ |
|
| 37120 | 964 |
Decision_Procs/ferrante_rackoff.ML \ |
965 |
Decision_Procs/ferrante_rackoff_data.ML \ |
|
966 |
Decision_Procs/langford.ML \ |
|
967 |
Decision_Procs/langford_data.ML \ |
|
968 |
Decision_Procs/mir_tac.ML |
|
|
29823
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
969 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Decision_Procs |
|
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
970 |
|
|
0ab754d13ccd
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
haftmann
parents:
29813
diff
changeset
|
971 |
|
|
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
|
972 |
## 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
|
973 |
|
|
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
|
974 |
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
|
975 |
|
|
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
|
976 |
$(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
|
977 |
@$(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
|
978 |
|
|
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
|
979 |
|
|
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
|
980 |
## 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
|
981 |
|
|
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
|
982 |
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
|
983 |
|
|
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
|
984 |
$(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
|
985 |
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
|
986 |
@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
|
987 |
|
|
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
|
988 |
|
|
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
|
989 |
## 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
|
990 |
|
|
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
|
991 |
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
|
992 |
|
|
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
|
993 |
$(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
|
994 |
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
|
995 |
Proofs/Extraction/Greatest_Common_Divisor.thy \ |
|
45047
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
45044
diff
changeset
|
996 |
Proofs/Extraction/Higman.thy Proofs/Extraction/Higman_Extraction.thy \ |
|
3aa8d3c391a4
Moved extraction part of Higman's lemma to separate theory to allow reuse in
berghofe
parents:
45044
diff
changeset
|
997 |
Proofs/Extraction/Pigeonhole.thy \ |
|
39157
b98909faaea8
more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
39156
diff
changeset
|
998 |
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
|
999 |
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
|
1000 |
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
|
1001 |
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
|
1002 |
@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
|
1003 |
|
|
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
|
1004 |
|
|
34205
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
1005 |
## HOL-Proofs-Lambda |
| 2448 | 1006 |
|
|
34205
f69cd974bc4e
explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.;
wenzelm
parents:
34126
diff
changeset
|
1007 |
HOL-Proofs-Lambda: HOL-Proofs $(LOG)/HOL-Proofs-Lambda.gz |
| 2448 | 1008 |
|
|
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
|
1009 |
$(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
|
1010 |
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
|
1011 |
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
|
1012 |
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
|
1013 |
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
|
1014 |
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
|
1015 |
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
|
1016 |
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
|
1017 |
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
|
1018 |
@cd Proofs; $(ISABELLE_TOOL) usedir -g true -m no_brackets -p 2 -q 0 $(OUT)/HOL-Proofs Lambda |
| 2448 | 1019 |
|
1020 |
||
| 9015 | 1021 |
## HOL-Prolog |
1022 |
||
1023 |
HOL-Prolog: HOL $(LOG)/HOL-Prolog.gz |
|
1024 |
||
| 27164 | 1025 |
$(LOG)/HOL-Prolog.gz: $(OUT)/HOL Prolog/ROOT.ML Prolog/prolog.ML \ |
1026 |
Prolog/HOHH.thy Prolog/Test.thy Prolog/Func.thy Prolog/Type.thy |
|
| 28500 | 1027 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Prolog |
| 9015 | 1028 |
|
1029 |
||
| 8012 | 1030 |
## HOL-MicroJava |
1031 |
||
1032 |
HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz |
|
1033 |
||
| 46722 | 1034 |
$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL MicroJava/ROOT.ML \ |
1035 |
MicroJava/Comp/AuxLemmas.thy MicroJava/Comp/CorrComp.thy \ |
|
1036 |
MicroJava/Comp/CorrCompTp.thy MicroJava/Comp/DefsComp.thy \ |
|
1037 |
MicroJava/Comp/Index.thy MicroJava/Comp/LemmasComp.thy \ |
|
| 27164 | 1038 |
MicroJava/Comp/TranslComp.thy MicroJava/Comp/TranslCompTp.thy \ |
1039 |
MicroJava/Comp/TypeInf.thy MicroJava/J/Conform.thy \ |
|
1040 |
MicroJava/J/Eval.thy MicroJava/J/JBasis.thy \ |
|
1041 |
MicroJava/J/JTypeSafe.thy MicroJava/J/Decl.thy MicroJava/J/State.thy \ |
|
1042 |
MicroJava/J/Term.thy MicroJava/J/Type.thy MicroJava/J/TypeRel.thy \ |
|
1043 |
MicroJava/J/WellForm.thy MicroJava/J/Value.thy \ |
|
1044 |
MicroJava/J/WellType.thy MicroJava/J/Example.thy \ |
|
1045 |
MicroJava/J/JListExample.thy MicroJava/JVM/JVMExec.thy \ |
|
1046 |
MicroJava/JVM/JVMInstructions.thy MicroJava/JVM/JVMState.thy \ |
|
1047 |
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
|
1048 |
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
|
1049 |
MicroJava/DFA/Err.thy MicroJava/DFA/Kildall.thy \ |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33820
diff
changeset
|
1050 |
MicroJava/DFA/LBVComplete.thy MicroJava/DFA/LBVCorrect.thy \ |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33820
diff
changeset
|
1051 |
MicroJava/DFA/LBVSpec.thy MicroJava/DFA/Listn.thy \ |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33820
diff
changeset
|
1052 |
MicroJava/DFA/Opt.thy MicroJava/DFA/Product.thy \ |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33820
diff
changeset
|
1053 |
MicroJava/DFA/SemilatAlg.thy MicroJava/DFA/Semilat.thy \ |
| 46722 | 1054 |
MicroJava/DFA/Semilattices.thy \ |
1055 |
MicroJava/DFA/Typing_Framework_err.thy \ |
|
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33820
diff
changeset
|
1056 |
MicroJava/DFA/Typing_Framework.thy MicroJava/BV/BVSpec.thy \ |
| 27164 | 1057 |
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
|
1058 |
MicroJava/BV/JType.thy MicroJava/BV/JVM.thy MicroJava/BV/JVMType.thy \ |
| 27164 | 1059 |
MicroJava/BV/Effect.thy MicroJava/BV/EffectMono.thy \ |
1060 |
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
|
1061 |
MicroJava/BV/LBVJVM.thy MicroJava/document/root.bib \ |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33820
diff
changeset
|
1062 |
MicroJava/document/root.tex MicroJava/document/introduction.tex |
| 28500 | 1063 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL MicroJava |
| 11850 | 1064 |
|
| 8012 | 1065 |
|
| 11376 | 1066 |
## HOL-NanoJava |
1067 |
||
1068 |
HOL-NanoJava: HOL $(LOG)/HOL-NanoJava.gz |
|
1069 |
||
| 27164 | 1070 |
$(LOG)/HOL-NanoJava.gz: $(OUT)/HOL NanoJava/ROOT.ML NanoJava/Term.thy \ |
1071 |
NanoJava/Decl.thy NanoJava/TypeRel.thy NanoJava/State.thy \ |
|
1072 |
NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy \ |
|
| 11376 | 1073 |
NanoJava/document/root.bib NanoJava/document/root.tex |
| 28500 | 1074 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NanoJava |
| 11850 | 1075 |
|
| 8193 | 1076 |
|
| 12855 | 1077 |
## HOL-Bali |
1078 |
||
1079 |
HOL-Bali: HOL $(LOG)/HOL-Bali.gz |
|
1080 |
||
|
41960
8a399da4cde1
eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;
wenzelm
parents:
41928
diff
changeset
|
1081 |
$(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/AxCompl.thy Bali/AxExample.thy \ |
|
8a399da4cde1
eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;
wenzelm
parents:
41928
diff
changeset
|
1082 |
Bali/AxSem.thy Bali/AxSound.thy Bali/Basis.thy Bali/Conform.thy \ |
|
8a399da4cde1
eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;
wenzelm
parents:
41928
diff
changeset
|
1083 |
Bali/Decl.thy Bali/DeclConcepts.thy Bali/Eval.thy Bali/Evaln.thy \ |
|
8a399da4cde1
eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;
wenzelm
parents:
41928
diff
changeset
|
1084 |
Bali/Example.thy Bali/Name.thy Bali/ROOT.ML Bali/State.thy \ |
|
8a399da4cde1
eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;
wenzelm
parents:
41928
diff
changeset
|
1085 |
Bali/Table.thy Bali/Term.thy Bali/Trans.thy Bali/Type.thy \ |
|
8a399da4cde1
eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;
wenzelm
parents:
41928
diff
changeset
|
1086 |
Bali/TypeRel.thy Bali/TypeSafe.thy Bali/Value.thy Bali/WellForm.thy \ |
|
8a399da4cde1
eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;
wenzelm
parents:
41928
diff
changeset
|
1087 |
Bali/DefiniteAssignment.thy Bali/DefiniteAssignmentCorrect.thy \ |
|
8a399da4cde1
eliminated Bali.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 9b19cbb0af28;
wenzelm
parents:
41928
diff
changeset
|
1088 |
Bali/WellType.thy Bali/document/root.tex |
| 28500 | 1089 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Bali |
| 12855 | 1090 |
|
1091 |
||
| 4518 | 1092 |
## HOL-IOA |
1093 |
||
1094 |
HOL-IOA: HOL $(LOG)/HOL-IOA.gz |
|
| 2448 | 1095 |
|
| 27164 | 1096 |
$(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.thy IOA/IOA.thy IOA/ROOT.ML \ |
1097 |
IOA/Solve.thy |
|
| 28500 | 1098 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL IOA |
| 4518 | 1099 |
|
1100 |
||
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
1101 |
## HOL-Lattice |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
1102 |
|
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
1103 |
HOL-Lattice: HOL $(LOG)/HOL-Lattice.gz |
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
1104 |
|
| 27164 | 1105 |
$(LOG)/HOL-Lattice.gz: $(OUT)/HOL Lattice/Bounds.thy \ |
1106 |
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
|
1107 |
Lattice/ROOT.ML Lattice/document/root.tex |
| 28500 | 1108 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Lattice |
|
10157
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
1109 |
|
|
6d3987f3aad9
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
wenzelm
parents:
10143
diff
changeset
|
1110 |
|
| 4518 | 1111 |
## HOL-ex |
| 2448 | 1112 |
|
| 4518 | 1113 |
HOL-ex: HOL $(LOG)/HOL-ex.gz |
| 2448 | 1114 |
|
| 33439 | 1115 |
$(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
|
1116 |
Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \ |
| 44276 | 1117 |
ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy ex/BT.thy \ |
1118 |
ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradox.thy ex/CTL.thy \ |
|
1119 |
ex/Case_Product.thy ex/Chinese.thy ex/Classical.thy \ |
|
|
45170
7dd207fe7b6e
removing invocations of the evaluation method based on the old code generator
bulwahn
parents:
45112
diff
changeset
|
1120 |
ex/Coercion_Examples.thy ex/Coherent.thy \ |
| 44276 | 1121 |
ex/Dedekind_Real.thy ex/Efficient_Nat_examples.thy \ |
|
46395
f56be74d7f51
adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
46324
diff
changeset
|
1122 |
ex/Eval_Examples.thy ex/Executable_Relation.thy ex/Fundefs.thy \ |
|
f56be74d7f51
adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
46324
diff
changeset
|
1123 |
ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy \ |
|
f56be74d7f51
adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
46324
diff
changeset
|
1124 |
ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy \ |
|
f56be74d7f51
adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
46324
diff
changeset
|
1125 |
ex/Higher_Order_Logic.thy ex/Iff_Oracle.thy ex/Induction_Schema.thy \ |
|
44962
5554ed48b13f
finite sequences as useful as introductory example;
wenzelm
parents:
44913
diff
changeset
|
1126 |
ex/Interpretation_with_Defs.thy ex/Intuitionistic.thy \ |
|
5554ed48b13f
finite sequences as useful as introductory example;
wenzelm
parents:
44913
diff
changeset
|
1127 |
ex/Lagrange.thy ex/List_to_Set_Comprehension_Examples.thy \ |
|
5554ed48b13f
finite sequences as useful as introductory example;
wenzelm
parents:
44913
diff
changeset
|
1128 |
ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy ex/Meson_Test.thy \ |
|
5554ed48b13f
finite sequences as useful as introductory example;
wenzelm
parents:
44913
diff
changeset
|
1129 |
ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \ |
|
46558
fdb84c40e074
renamed ex/Numeral.thy to ex/Numeral_Representation.thy
huffman
parents:
46395
diff
changeset
|
1130 |
ex/Normalization_by_Evaluation.thy ex/Numeral_Representation.thy \ |
|
fdb84c40e074
renamed ex/Numeral.thy to ex/Numeral_Representation.thy
huffman
parents:
46395
diff
changeset
|
1131 |
ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \ |
| 46585 | 1132 |
ex/Quicksort.thy ex/ROOT.ML \ |
| 44276 | 1133 |
ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy \ |
1134 |
ex/SAT_Examples.thy ex/Serbian.thy ex/Set_Theory.thy \ |
|
|
45224
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
45190
diff
changeset
|
1135 |
ex/Set_Algebras.thy ex/Simproc_Tests.thy ex/SVC_Oracle.thy \ |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
45190
diff
changeset
|
1136 |
ex/sledgehammer_tactics.ML ex/Seq.thy ex/Sqrt.thy ex/Sqrt_Script.thy \ |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
45190
diff
changeset
|
1137 |
ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy \ |
|
b1d5b3820d82
add HOL/ex/Simproc_Tests.thy: testing for Tools/numeral_simprocs.ML
huffman
parents:
45190
diff
changeset
|
1138 |
ex/Tree23.thy ex/Unification.thy ex/While_Combinator_Example.thy \ |
| 44276 | 1139 |
ex/document/root.bib ex/document/root.tex ex/svc_funcs.ML \ |
1140 |
ex/svc_test.thy ../Tools/interpretation_with_defs.ML |
|
| 28500 | 1141 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex |
| 2448 | 1142 |
|
1143 |
||
| 33026 | 1144 |
## HOL-Isar_Examples |
| 6445 | 1145 |
|
| 33026 | 1146 |
HOL-Isar_Examples: HOL $(LOG)/HOL-Isar_Examples.gz |
| 6445 | 1147 |
|
| 33026 | 1148 |
$(LOG)/HOL-Isar_Examples.gz: $(OUT)/HOL Isar_Examples/Basic_Logic.thy \ |
1149 |
Isar_Examples/Cantor.thy Isar_Examples/Drinker.thy \ |
|
1150 |
Isar_Examples/Expr_Compiler.thy Isar_Examples/Fibonacci.thy \ |
|
1151 |
Isar_Examples/Group.thy Isar_Examples/Hoare.thy \ |
|
1152 |
Isar_Examples/Hoare_Ex.thy Isar_Examples/Knaster_Tarski.thy \ |
|
1153 |
Isar_Examples/Mutilated_Checkerboard.thy \ |
|
1154 |
Isar_Examples/Nested_Datatype.thy Isar_Examples/Peirce.thy \ |
|
1155 |
Isar_Examples/Puzzle.thy Isar_Examples/Summation.thy \ |
|
1156 |
Isar_Examples/ROOT.ML Isar_Examples/document/proof.sty \ |
|
1157 |
Isar_Examples/document/root.bib Isar_Examples/document/root.tex \ |
|
| 37672 | 1158 |
Isar_Examples/document/style.tex Hoare/hoare_tac.ML \ |
1159 |
Number_Theory/Primes.thy |
|
| 33026 | 1160 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Isar_Examples |
| 6445 | 1161 |
|
1162 |
||
| 33028 | 1163 |
## HOL-SET_Protocol |
| 14199 | 1164 |
|
| 33028 | 1165 |
HOL-SET_Protocol: HOL $(LOG)/HOL-SET_Protocol.gz |
| 14199 | 1166 |
|
| 33028 | 1167 |
$(LOG)/HOL-SET_Protocol.gz: $(OUT)/HOL SET_Protocol/ROOT.ML \ |
1168 |
SET_Protocol/Message_SET.thy SET_Protocol/Event_SET.thy \ |
|
1169 |
SET_Protocol/Public_SET.thy SET_Protocol/Cardholder_Registration.thy \ |
|
1170 |
SET_Protocol/Merchant_Registration.thy SET_Protocol/Purchase.thy \ |
|
| 39757 | 1171 |
SET_Protocol/SET_Protocol.thy SET_Protocol/document/root.tex |
| 33028 | 1172 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL SET_Protocol |
| 14199 | 1173 |
|
1174 |
||
|
46988
9f492f5b0cec
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset
|
1175 |
## HOL-Matrix_LP |
| 14610 | 1176 |
|
|
46988
9f492f5b0cec
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset
|
1177 |
HOL-Matrix_LP: HOL $(LOG)/HOL-Matrix_LP.gz |
| 17323 | 1178 |
|
|
46988
9f492f5b0cec
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset
|
1179 |
$(LOG)/HOL-Matrix_LP.gz: $(OUT)/HOL Matrix_LP/ComputeFloat.thy \ |
|
9f492f5b0cec
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset
|
1180 |
Matrix_LP/ComputeHOL.thy Matrix_LP/ComputeNumeral.thy \ |
|
9f492f5b0cec
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset
|
1181 |
Matrix_LP/Compute_Oracle/Compute_Oracle.thy \ |
|
9f492f5b0cec
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset
|
1182 |
Matrix_LP/Compute_Oracle/am.ML \ |
|
9f492f5b0cec
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset
|
1183 |
Matrix_LP/Compute_Oracle/am_compiler.ML \ |
|
9f492f5b0cec
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset
|
1184 |
Matrix_LP/Compute_Oracle/am_ghc.ML \ |
|
9f492f5b0cec
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset
|
1185 |
Matrix_LP/Compute_Oracle/am_interpreter.ML \ |
|
9f492f5b0cec
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset
|
1186 |
Matrix_LP/Compute_Oracle/am_sml.ML \ |
|
9f492f5b0cec
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset
|
1187 |
Matrix_LP/Compute_Oracle/compute.ML \ |
|
9f492f5b0cec
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset
|
1188 |
Matrix_LP/Compute_Oracle/linker.ML Matrix_LP/Cplex.thy \ |
|
9f492f5b0cec
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset
|
1189 |
Matrix_LP/CplexMatrixConverter.ML Matrix_LP/Cplex_tools.ML \ |
|
9f492f5b0cec
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset
|
1190 |
Matrix_LP/FloatSparseMatrixBuilder.ML Matrix_LP/LP.thy \ |
|
9f492f5b0cec
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset
|
1191 |
Matrix_LP/Matrix.thy Matrix_LP/ROOT.ML Matrix_LP/SparseMatrix.thy \ |
|
9f492f5b0cec
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset
|
1192 |
Matrix_LP/document/root.tex Matrix_LP/fspmlp.ML \ |
|
9f492f5b0cec
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset
|
1193 |
Matrix_LP/matrixlp.ML Tools/float_arith.ML |
|
9f492f5b0cec
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset
|
1194 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Matrix_LP |
| 16873 | 1195 |
|
| 14199 | 1196 |
|
| 4518 | 1197 |
## TLA |
1198 |
||
1199 |
TLA: HOL $(OUT)/TLA |
|
1200 |
||
| 27164 | 1201 |
$(OUT)/TLA: $(OUT)/HOL TLA/Action.thy TLA/Init.thy TLA/Intensional.thy \ |
| 21624 | 1202 |
TLA/ROOT.ML TLA/Stfun.thy TLA/TLA.thy |
| 28500 | 1203 |
@cd TLA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL TLA |
| 4518 | 1204 |
|
1205 |
||
1206 |
## TLA-Inc |
|
1207 |
||
1208 |
TLA-Inc: TLA $(LOG)/TLA-Inc.gz |
|
1209 |
||
| 21624 | 1210 |
$(LOG)/TLA-Inc.gz: $(OUT)/TLA TLA/Inc/Inc.thy |
| 28500 | 1211 |
@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Inc |
| 4518 | 1212 |
|
1213 |
||
1214 |
## TLA-Buffer |
|
1215 |
||
1216 |
TLA-Buffer: TLA $(LOG)/TLA-Buffer.gz |
|
| 2448 | 1217 |
|
|
33024
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
1218 |
$(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
|
1219 |
TLA/Buffer/DBuffer.thy |
| 28500 | 1220 |
@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Buffer |
| 4518 | 1221 |
|
1222 |
||
1223 |
## TLA-Memory |
|
1224 |
||
1225 |
TLA-Memory: TLA $(LOG)/TLA-Memory.gz |
|
| 4447 | 1226 |
|
| 27164 | 1227 |
$(LOG)/TLA-Memory.gz: $(OUT)/TLA TLA/Memory/MemClerk.thy \ |
1228 |
TLA/Memory/MemClerkParameters.thy TLA/Memory/Memory.thy \ |
|
1229 |
TLA/Memory/MemoryImplementation.thy TLA/Memory/MemoryParameters.thy \ |
|
1230 |
TLA/Memory/ProcedureInterface.thy TLA/Memory/RPC.thy \ |
|
| 21624 | 1231 |
TLA/Memory/RPCMemoryParams.thy TLA/Memory/RPCParameters.thy |
| 28500 | 1232 |
@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Memory |
| 4518 | 1233 |
|
1234 |
||
|
43804
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
43800
diff
changeset
|
1235 |
## HOL-TPTP |
|
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
43800
diff
changeset
|
1236 |
|
|
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
43800
diff
changeset
|
1237 |
HOL-TPTP: HOL $(LOG)/HOL-TPTP.gz |
|
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
43800
diff
changeset
|
1238 |
|
| 46951 | 1239 |
$(LOG)/HOL-TPTP.gz: $(OUT)/HOL \ |
1240 |
TPTP/ATP_Problem_Import.thy \ |
|
1241 |
TPTP/ATP_Theory_Export.thy \ |
|
1242 |
TPTP/CASC_Setup.thy \ |
|
|
43804
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
43800
diff
changeset
|
1243 |
TPTP/ROOT.ML \ |
| 46951 | 1244 |
TPTP/TPTP_Parser.thy \ |
1245 |
TPTP/TPTP_Parser/ml_yacc_lib.ML \ |
|
1246 |
TPTP/TPTP_Parser/tptp_interpret.ML \ |
|
1247 |
TPTP/TPTP_Parser/tptp_lexyacc.ML \ |
|
1248 |
TPTP/TPTP_Parser/tptp_parser.ML \ |
|
1249 |
TPTP/TPTP_Parser/tptp_problem_name.ML \ |
|
1250 |
TPTP/TPTP_Parser/tptp_syntax.ML \ |
|
1251 |
TPTP/TPTP_Parser_Test.thy \ |
|
| 46324 | 1252 |
TPTP/atp_problem_import.ML \ |
| 46951 | 1253 |
TPTP/atp_theory_export.ML |
|
45087
3417c1b91e3c
reverted 09cdc4209d25 for formal reasons: it did not say what was "broken" nor "fixed", but broke IsaMakefile dependencies;
wenzelm
parents:
45074
diff
changeset
|
1254 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL TPTP |
|
43804
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
43800
diff
changeset
|
1255 |
|
|
eb9be23db2b7
cleanly separate TPTP related files from other examples
blanchet
parents:
43800
diff
changeset
|
1256 |
|
| 33175 | 1257 |
## HOL-Multivariate_Analysis |
1258 |
||
| 36898 | 1259 |
HOL-Multivariate_Analysis: HOL $(OUT)/HOL-Multivariate_Analysis |
| 33175 | 1260 |
|
| 36937 | 1261 |
$(OUT)/HOL-Multivariate_Analysis: $(OUT)/HOL \ |
1262 |
Multivariate_Analysis/Brouwer_Fixpoint.thy \ |
|
| 37522 | 1263 |
Multivariate_Analysis/Cartesian_Euclidean_Space.thy \ |
| 36937 | 1264 |
Multivariate_Analysis/Convex_Euclidean_Space.thy \ |
1265 |
Multivariate_Analysis/Derivative.thy \ |
|
1266 |
Multivariate_Analysis/Determinants.thy \ |
|
1267 |
Multivariate_Analysis/Euclidean_Space.thy \ |
|
|
41980
28b51effc5ed
split Extended_Reals into parts for Library and Multivariate_Analysis
hoelzl
parents:
41973
diff
changeset
|
1268 |
Multivariate_Analysis/Extended_Real_Limits.thy \ |
| 36937 | 1269 |
Multivariate_Analysis/Fashoda.thy \ |
1270 |
Multivariate_Analysis/Finite_Cartesian_Product.thy \ |
|
1271 |
Multivariate_Analysis/Integration.certs \ |
|
1272 |
Multivariate_Analysis/Integration.thy \ |
|
1273 |
Multivariate_Analysis/L2_Norm.thy \ |
|
| 44288 | 1274 |
Multivariate_Analysis/Linear_Algebra.thy \ |
| 36937 | 1275 |
Multivariate_Analysis/Multivariate_Analysis.thy \ |
|
44516
d9a496ae5d9d
move everything related to 'norm' method into new theory file Norm_Arith.thy
huffman
parents:
44374
diff
changeset
|
1276 |
Multivariate_Analysis/Norm_Arith.thy \ |
| 36937 | 1277 |
Multivariate_Analysis/Operator_Norm.thy \ |
1278 |
Multivariate_Analysis/Path_Connected.thy \ |
|
1279 |
Multivariate_Analysis/ROOT.ML \ |
|
1280 |
Multivariate_Analysis/Real_Integration.thy \ |
|
1281 |
Multivariate_Analysis/Topology_Euclidean_Space.thy \ |
|
1282 |
Multivariate_Analysis/document/root.tex \ |
|
| 37742 | 1283 |
Multivariate_Analysis/normarith.ML Library/Glbs.thy \ |
| 43920 | 1284 |
Library/Extended_Real.thy Library/Indicator_Function.thy \ |
|
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41980
diff
changeset
|
1285 |
Library/Inner_Product.thy Library/Numeral_Type.thy Library/Convex.thy \ |
|
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41980
diff
changeset
|
1286 |
Library/FrechetDeriv.thy Library/Product_Vector.thy \ |
| 44288 | 1287 |
Library/Product_plus.thy Library/Sum_of_Squares.thy |
| 36898 | 1288 |
@cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Multivariate_Analysis |
| 33175 | 1289 |
|
| 33285 | 1290 |
|
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33270
diff
changeset
|
1291 |
## HOL-Probability |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
33270
diff
changeset
|
1292 |
|
| 38656 | 1293 |
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
|
1294 |
|
| 40863 | 1295 |
$(OUT)/HOL-Probability: $(OUT)/HOL-Multivariate_Analysis \ |
|
42146
5b52c6a9c627
split Product_Measure into Binary_Product_Measure and Finite_Product_Measure
hoelzl
parents:
42138
diff
changeset
|
1296 |
Probability/Binary_Product_Measure.thy Probability/Borel_Space.thy \ |
|
5b52c6a9c627
split Product_Measure into Binary_Product_Measure and Finite_Product_Measure
hoelzl
parents:
42138
diff
changeset
|
1297 |
Probability/Caratheodory.thy Probability/Complete_Measure.thy \ |
|
43556
0d78c8d31d0d
move conditional expectation to its own theory file
hoelzl
parents:
43524
diff
changeset
|
1298 |
Probability/Conditional_Probability.thy \ |
|
40860
a6df324752da
More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
hoelzl
parents:
40839
diff
changeset
|
1299 |
Probability/ex/Dining_Cryptographers.thy \ |
|
a6df324752da
More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
hoelzl
parents:
40839
diff
changeset
|
1300 |
Probability/ex/Koepf_Duermuth_Countermeasure.thy \ |
| 42147 | 1301 |
Probability/Finite_Product_Measure.thy \ |
|
42861
16375b493b64
Add formalization of probabilistic independence for families of sets
hoelzl
parents:
42841
diff
changeset
|
1302 |
Probability/Independent_Family.thy \ |
| 42147 | 1303 |
Probability/Infinite_Product_Measure.thy Probability/Information.thy \ |
|
42146
5b52c6a9c627
split Product_Measure into Binary_Product_Measure and Finite_Product_Measure
hoelzl
parents:
42138
diff
changeset
|
1304 |
Probability/Lebesgue_Integration.thy Probability/Lebesgue_Measure.thy \ |
| 42148 | 1305 |
Probability/Measure.thy Probability/Probability_Measure.thy \ |
|
42146
5b52c6a9c627
split Product_Measure into Binary_Product_Measure and Finite_Product_Measure
hoelzl
parents:
42138
diff
changeset
|
1306 |
Probability/Probability.thy Probability/Radon_Nikodym.thy \ |
|
40860
a6df324752da
More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability.
hoelzl
parents:
40839
diff
changeset
|
1307 |
Probability/ROOT.ML Probability/Sigma_Algebra.thy \ |
|
42146
5b52c6a9c627
split Product_Measure into Binary_Product_Measure and Finite_Product_Measure
hoelzl
parents:
42138
diff
changeset
|
1308 |
Library/Countable.thy Library/FuncSet.thy Library/Nat_Bijection.thy |
| 38656 | 1309 |
@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
|
1310 |
|
|
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
|
1311 |
|
| 19497 | 1312 |
## HOL-Nominal |
1313 |
||
1314 |
HOL-Nominal: HOL $(OUT)/HOL-Nominal |
|
1315 |
||
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
22167
diff
changeset
|
1316 |
$(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
|
1317 |
Nominal/Nominal.thy \ |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
22167
diff
changeset
|
1318 |
Nominal/nominal_atoms.ML \ |
| 31936 | 1319 |
Nominal/nominal_datatype.ML \ |
|
22784
4637b69de71b
Added datatype_case.ML and nominal_fresh_fun.ML.
berghofe
parents:
22657
diff
changeset
|
1320 |
Nominal/nominal_fresh_fun.ML \ |
| 22247 | 1321 |
Nominal/nominal_induct.ML \ |
| 22314 | 1322 |
Nominal/nominal_inductive.ML \ |
| 28652 | 1323 |
Nominal/nominal_inductive2.ML \ |
|
22245
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
22167
diff
changeset
|
1324 |
Nominal/nominal_permeq.ML \ |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
22167
diff
changeset
|
1325 |
Nominal/nominal_primrec.ML \ |
|
1b8f4ef50c48
moved the infrastructure from the nominal_tags file to nominal_thmdecls
urbanc
parents:
22167
diff
changeset
|
1326 |
Nominal/nominal_thmdecls.ML \ |
| 21542 | 1327 |
Library/Infinite_Set.thy |
| 28500 | 1328 |
@cd Nominal; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Nominal |
| 19497 | 1329 |
|
1330 |
||
1331 |
## HOL-Nominal-Examples |
|
1332 |
||
1333 |
HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz |
|
1334 |
||
|
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
|
1335 |
$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal \ |
|
32636
55a0be42327c
added session theory for Bali and Nominal_Examples
haftmann
parents:
32632
diff
changeset
|
1336 |
Nominal/Examples/Nominal_Examples.thy \ |
| 27163 | 1337 |
Nominal/Examples/CK_Machine.thy \ |
|
22073
c170dcbe6c9d
formalisation of Crary's chapter on logical relations
urbanc
parents:
22067
diff
changeset
|
1338 |
Nominal/Examples/CR.thy \ |
|
22821
15b2e7ec1f3b
alternative and much simpler proof for Church-Rosser of Beta-Reduction
urbanc
parents:
22819
diff
changeset
|
1339 |
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
|
1340 |
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
|
1341 |
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
|
1342 |
Nominal/Examples/Class3.thy \ |
|
22073
c170dcbe6c9d
formalisation of Crary's chapter on logical relations
urbanc
parents:
22067
diff
changeset
|
1343 |
Nominal/Examples/Compile.thy \ |
| 25725 | 1344 |
Nominal/Examples/Contexts.thy \ |
1345 |
Nominal/Examples/Crary.thy \ |
|
|
22073
c170dcbe6c9d
formalisation of Crary's chapter on logical relations
urbanc
parents:
22067
diff
changeset
|
1346 |
Nominal/Examples/Fsub.thy \ |
| 25725 | 1347 |
Nominal/Examples/Height.thy \ |
1348 |
Nominal/Examples/Lam_Funs.thy \ |
|
|
22073
c170dcbe6c9d
formalisation of Crary's chapter on logical relations
urbanc
parents:
22067
diff
changeset
|
1349 |
Nominal/Examples/Lambda_mu.thy \ |
| 25725 | 1350 |
Nominal/Examples/LocalWeakening.thy \ |
| 33189 | 1351 |
Nominal/Examples/Pattern.thy \ |
| 25725 | 1352 |
Nominal/Examples/ROOT.ML \ |
|
22073
c170dcbe6c9d
formalisation of Crary's chapter on logical relations
urbanc
parents:
22067
diff
changeset
|
1353 |
Nominal/Examples/SN.thy \ |
| 23144 | 1354 |
Nominal/Examples/SOS.thy \ |
|
27624
a925aa66e17a
Added Standardization theory to nominal examples.
berghofe
parents:
27484
diff
changeset
|
1355 |
Nominal/Examples/Standardization.thy \ |
|
24896
70f238757695
added the two new examples from Nominal to the build process
urbanc
parents:
24830
diff
changeset
|
1356 |
Nominal/Examples/Support.thy \ |
| 27032 | 1357 |
Nominal/Examples/Type_Preservation.thy \ |
| 25725 | 1358 |
Nominal/Examples/VC_Condition.thy \ |
| 26195 | 1359 |
Nominal/Examples/W.thy \ |
| 25725 | 1360 |
Nominal/Examples/Weakening.thy |
| 28500 | 1361 |
@cd Nominal; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Nominal Examples |
| 19497 | 1362 |
|
1363 |
||
| 24333 | 1364 |
## HOL-Word |
1365 |
||
1366 |
HOL-Word: HOL $(OUT)/HOL-Word |
|
1367 |
||
|
33024
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
1368 |
$(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML Library/Boolean_Algebra.thy \ |
| 37655 | 1369 |
Library/Numeral_Type.thy Word/Misc_Numeric.thy Word/Misc_Typedef.thy \ |
| 37659 | 1370 |
Word/Type_Length.thy Word/Bit_Representation.thy Word/Bit_Int.thy \ |
1371 |
Word/Bool_List_Representation.thy Word/Bit_Operations.thy \ |
|
| 37660 | 1372 |
Word/Word.thy Word/document/root.tex \ |
|
41060
4199fdcfa3c0
moved smt_word.ML into the directory of the Word library
boehmes
parents:
40969
diff
changeset
|
1373 |
Word/document/root.bib Word/Tools/smt_word.ML |
| 28500 | 1374 |
@cd Word; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Word |
| 24333 | 1375 |
|
1376 |
||
| 24442 | 1377 |
## HOL-Word-Examples |
1378 |
||
1379 |
HOL-Word-Examples: HOL-Word $(LOG)/HOL-Word-Examples.gz |
|
1380 |
||
| 27164 | 1381 |
$(LOG)/HOL-Word-Examples.gz: $(OUT)/HOL-Word Word/Examples/ROOT.ML \ |
| 24442 | 1382 |
Word/Examples/WordExamples.thy |
| 28500 | 1383 |
@cd Word; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Word Examples |
| 24442 | 1384 |
|
|
27477
c64736fe2a1f
more precise dependencies for HOL-Word and HOL-NSA;
wenzelm
parents:
27470
diff
changeset
|
1385 |
|
| 25171 | 1386 |
## HOL-Statespace |
1387 |
||
1388 |
HOL-Statespace: HOL $(LOG)/HOL-Statespace.gz |
|
1389 |
||
| 45357 | 1390 |
$(LOG)/HOL-Statespace.gz: $(OUT)/HOL Statespace/ROOT.ML \ |
1391 |
Statespace/DistinctTreeProver.thy Statespace/StateFun.thy \ |
|
1392 |
Statespace/StateSpaceLocale.thy Statespace/StateSpaceSyntax.thy \ |
|
1393 |
Statespace/StateSpaceEx.thy Statespace/distinct_tree_prover.ML \ |
|
1394 |
Statespace/state_space.ML Statespace/state_fun.ML \ |
|
1395 |
Statespace/document/root.tex |
|
| 28500 | 1396 |
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Statespace |
| 24442 | 1397 |
|
|
27477
c64736fe2a1f
more precise dependencies for HOL-Word and HOL-NSA;
wenzelm
parents:
27470
diff
changeset
|
1398 |
|
| 27470 | 1399 |
## HOL-NSA |
1400 |
||
|
27477
c64736fe2a1f
more precise dependencies for HOL-Word and HOL-NSA;
wenzelm
parents:
27470
diff
changeset
|
1401 |
HOL-NSA: HOL $(OUT)/HOL-NSA |
| 27470 | 1402 |
|
|
33024
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
1403 |
$(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
|
1404 |
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
|
1405 |
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
|
1406 |
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
|
1407 |
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
|
1408 |
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
|
1409 |
Library/Infinite_Set.thy Library/Zorn.thy NSA/ROOT.ML |
| 28500 | 1410 |
@cd NSA; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-NSA |
| 27470 | 1411 |
|
|
27477
c64736fe2a1f
more precise dependencies for HOL-Word and HOL-NSA;
wenzelm
parents:
27470
diff
changeset
|
1412 |
|
| 27470 | 1413 |
## HOL-NSA-Examples |
1414 |
||
1415 |
HOL-NSA-Examples: HOL-NSA $(LOG)/HOL-NSA-Examples.gz |
|
1416 |
||
| 37742 | 1417 |
$(LOG)/HOL-NSA-Examples.gz: $(OUT)/HOL-NSA NSA/Examples/ROOT.ML \ |
| 27470 | 1418 |
NSA/Examples/NSPrimes.thy |
| 28500 | 1419 |
@cd NSA; $(ISABELLE_TOOL) usedir $(OUT)/HOL-NSA Examples |
| 27470 | 1420 |
|
|
27477
c64736fe2a1f
more precise dependencies for HOL-Word and HOL-NSA;
wenzelm
parents:
27470
diff
changeset
|
1421 |
|
| 32496 | 1422 |
## HOL-Mirabelle |
1423 |
||
1424 |
HOL-Mirabelle: HOL $(LOG)/HOL-Mirabelle.gz |
|
1425 |
||
|
33024
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
1426 |
$(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
|
1427 |
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
|
1428 |
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
|
1429 |
Mirabelle/Tools/mirabelle_metis.ML \ |
|
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
1430 |
Mirabelle/Tools/mirabelle_quickcheck.ML \ |
|
60a098883d81
more accurate dependencies for HOL-SMT, which is a session with image;
wenzelm
parents:
33010
diff
changeset
|
1431 |
Mirabelle/Tools/mirabelle_refute.ML \ |
|
40634
dc124a486f94
adding dependencies to IsaMakefile; adding sledgehammer_tactic in Mirabelle_Test
bulwahn
parents:
40632
diff
changeset
|
1432 |
Mirabelle/Tools/mirabelle_sledgehammer.ML \ |
| 41407 | 1433 |
Mirabelle/Tools/mirabelle_sledgehammer_filter.ML \ |
|
42071
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
42064
diff
changeset
|
1434 |
ex/sledgehammer_tactics.ML Mirabelle/lib/Tools/mirabelle \ |
|
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
42064
diff
changeset
|
1435 |
Mirabelle/lib/scripts/mirabelle.pl Library/FrechetDeriv.thy \ |
|
04577a7e0c51
move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex"
blanchet
parents:
42064
diff
changeset
|
1436 |
Library/Inner_Product.thy |
| 32496 | 1437 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle |
|
42035
fb155c75072d
small test case for main mirabelle functionality, which easily breaks without noticing
krauss
parents:
41981
diff
changeset
|
1438 |
@cd Library; $(ISABELLE_TOOL) mirabelle -q arith Inner_Product.thy # some arbitrary small test case |
| 32496 | 1439 |
|
1440 |
||
|
36933
705b58fde476
more precise dependencies for HOL-Word-SMT_Examples;
wenzelm
parents:
36916
diff
changeset
|
1441 |
## HOL-Word-SMT_Examples |
|
32618
42865636d006
added new method "smt": an oracle-based connection to external SMT solvers
boehmes
parents:
32558
diff
changeset
|
1442 |
|
|
36933
705b58fde476
more precise dependencies for HOL-Word-SMT_Examples;
wenzelm
parents:
36916
diff
changeset
|
1443 |
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
|
1444 |
|
|
36933
705b58fde476
more precise dependencies for HOL-Word-SMT_Examples;
wenzelm
parents:
36916
diff
changeset
|
1445 |
$(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
|
1446 |
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
|
1447 |
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
|
1448 |
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
|
1449 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL-Word SMT_Examples |
| 33010 | 1450 |
|
1451 |
||
| 33419 | 1452 |
## HOL-Boogie |
1453 |
||
|
36899
bcd6fce5bf06
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents:
36898
diff
changeset
|
1454 |
HOL-Boogie: HOL-Word $(OUT)/HOL-Boogie |
| 33419 | 1455 |
|
| 36901 | 1456 |
$(OUT)/HOL-Boogie: $(OUT)/HOL-Word Boogie/ROOT.ML Boogie/Boogie.thy \ |
| 33439 | 1457 |
Boogie/Tools/boogie_vcs.ML Boogie/Tools/boogie_loader.ML \ |
| 34069 | 1458 |
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
|
1459 |
@cd Boogie; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-Boogie |
| 33419 | 1460 |
|
1461 |
||
1462 |
## HOL-Boogie_Examples |
|
1463 |
||
| 33439 | 1464 |
HOL-Boogie-Examples: HOL-Boogie $(LOG)/HOL-Boogie-Examples.gz |
| 33419 | 1465 |
|
| 33439 | 1466 |
$(LOG)/HOL-Boogie-Examples.gz: $(OUT)/HOL-Boogie \ |
1467 |
Boogie/Examples/ROOT.ML Boogie/Examples/Boogie_Max.thy \ |
|
1468 |
Boogie/Examples/Boogie_Max.b2i Boogie/Examples/Boogie_Dijkstra.thy \ |
|
1469 |
Boogie/Examples/VCC_Max.thy Boogie/Examples/Boogie_Dijkstra.b2i \ |
|
| 34996 | 1470 |
Boogie/Examples/VCC_Max.b2i Boogie/Examples/Boogie_Max.certs \ |
1471 |
Boogie/Examples/Boogie_Dijkstra.certs Boogie/Examples/VCC_Max.certs |
|
| 33419 | 1472 |
@cd Boogie; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Boogie Examples |
1473 |
||
1474 |
||
| 41566 | 1475 |
## HOL-SPARK |
1476 |
||
1477 |
HOL-SPARK: HOL-Word $(OUT)/HOL-SPARK |
|
1478 |
||
1479 |
$(OUT)/HOL-SPARK: $(OUT)/HOL-Word SPARK/ROOT.ML \ |
|
1480 |
SPARK/SPARK.thy SPARK/SPARK_Setup.thy \ |
|
1481 |
SPARK/Tools/fdl_lexer.ML SPARK/Tools/fdl_parser.ML \ |
|
1482 |
SPARK/Tools/spark_commands.ML SPARK/Tools/spark_vcs.ML |
|
1483 |
@cd SPARK; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SPARK |
|
1484 |
||
1485 |
||
1486 |
## HOL-SPARK-Examples |
|
1487 |
||
1488 |
HOL-SPARK-Examples: HOL-SPARK $(LOG)/HOL-SPARK-Examples.gz |
|
1489 |
||
1490 |
$(LOG)/HOL-SPARK-Examples.gz: $(OUT)/HOL-SPARK \ |
|
1491 |
SPARK/Examples/ROOT.ML \ |
|
1492 |
SPARK/Examples/Gcd/Greatest_Common_Divisor.thy \ |
|
1493 |
SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.fdl \ |
|
1494 |
SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.rls \ |
|
1495 |
SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.siv \ |
|
1496 |
SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy \ |
|
1497 |
SPARK/Examples/Liseq/liseq/liseq_length.fdl \ |
|
1498 |
SPARK/Examples/Liseq/liseq/liseq_length.rls \ |
|
1499 |
SPARK/Examples/Liseq/liseq/liseq_length.siv \ |
|
1500 |
SPARK/Examples/RIPEMD-160/F.thy SPARK/Examples/RIPEMD-160/Hash.thy \ |
|
1501 |
SPARK/Examples/RIPEMD-160/K_L.thy SPARK/Examples/RIPEMD-160/K_R.thy \ |
|
1502 |
SPARK/Examples/RIPEMD-160/R_L.thy \ |
|
1503 |
SPARK/Examples/RIPEMD-160/RMD_Lemmas.thy \ |
|
1504 |
SPARK/Examples/RIPEMD-160/RMD_Specification.thy \ |
|
1505 |
SPARK/Examples/RIPEMD-160/RMD.thy SPARK/Examples/RIPEMD-160/Round.thy \ |
|
1506 |
SPARK/Examples/RIPEMD-160/R_R.thy SPARK/Examples/RIPEMD-160/S_L.thy \ |
|
1507 |
SPARK/Examples/RIPEMD-160/S_R.thy \ |
|
1508 |
SPARK/Examples/RIPEMD-160/rmd/f.fdl \ |
|
1509 |
SPARK/Examples/RIPEMD-160/rmd/f.rls \ |
|
1510 |
SPARK/Examples/RIPEMD-160/rmd/f.siv \ |
|
1511 |
SPARK/Examples/RIPEMD-160/rmd/hash.fdl \ |
|
1512 |
SPARK/Examples/RIPEMD-160/rmd/hash.rls \ |
|
1513 |
SPARK/Examples/RIPEMD-160/rmd/hash.siv \ |
|
1514 |
SPARK/Examples/RIPEMD-160/rmd/k_l.fdl \ |
|
1515 |
SPARK/Examples/RIPEMD-160/rmd/k_l.rls \ |
|
1516 |
SPARK/Examples/RIPEMD-160/rmd/k_l.siv \ |
|
1517 |
SPARK/Examples/RIPEMD-160/rmd/k_r.fdl \ |
|
1518 |
SPARK/Examples/RIPEMD-160/rmd/k_r.rls \ |
|
1519 |
SPARK/Examples/RIPEMD-160/rmd/k_r.siv \ |
|
1520 |
SPARK/Examples/RIPEMD-160/rmd/r_l.fdl \ |
|
1521 |
SPARK/Examples/RIPEMD-160/rmd/r_l.rls \ |
|
1522 |
SPARK/Examples/RIPEMD-160/rmd/r_l.siv \ |
|
1523 |
SPARK/Examples/RIPEMD-160/rmd/round.fdl \ |
|
1524 |
SPARK/Examples/RIPEMD-160/rmd/round.rls \ |
|
1525 |
SPARK/Examples/RIPEMD-160/rmd/round.siv \ |
|
1526 |
SPARK/Examples/RIPEMD-160/rmd/r_r.fdl \ |
|
1527 |
SPARK/Examples/RIPEMD-160/rmd/r_r.rls \ |
|
1528 |
SPARK/Examples/RIPEMD-160/rmd/r_r.siv \ |
|
1529 |
SPARK/Examples/RIPEMD-160/rmd/s_l.fdl \ |
|
1530 |
SPARK/Examples/RIPEMD-160/rmd/s_l.rls \ |
|
1531 |
SPARK/Examples/RIPEMD-160/rmd/s_l.siv \ |
|
1532 |
SPARK/Examples/RIPEMD-160/rmd/s_r.fdl \ |
|
1533 |
SPARK/Examples/RIPEMD-160/rmd/s_r.rls \ |
|
1534 |
SPARK/Examples/RIPEMD-160/rmd/s_r.siv |
|
1535 |
@cd SPARK; $(ISABELLE_TOOL) usedir $(OUT)/HOL-SPARK Examples |
|
1536 |
||
1537 |
||
| 45044 | 1538 |
## HOL-SPARK-Manual |
1539 |
||
1540 |
HOL-SPARK-Manual: HOL-SPARK $(LOG)/HOL-SPARK-Manual.gz |
|
1541 |
||
1542 |
$(LOG)/HOL-SPARK-Manual.gz: $(OUT)/HOL-SPARK \ |
|
1543 |
SPARK/Manual/ROOT.ML \ |
|
1544 |
SPARK/Manual/Complex_Types.thy \ |
|
1545 |
SPARK/Manual/Example_Verification.thy \ |
|
1546 |
SPARK/Manual/Proc1.thy \ |
|
1547 |
SPARK/Manual/Proc2.thy \ |
|
1548 |
SPARK/Manual/Reference.thy \ |
|
1549 |
SPARK/Manual/Simple_Greatest_Common_Divisor.thy \ |
|
1550 |
SPARK/Manual/VC_Principles.thy \ |
|
1551 |
SPARK/Manual/complex_types_app/initialize.fdl \ |
|
1552 |
SPARK/Manual/complex_types_app/initialize.rls \ |
|
1553 |
SPARK/Manual/complex_types_app/initialize.siv \ |
|
1554 |
SPARK/Manual/loop_invariant/proc1.fdl \ |
|
1555 |
SPARK/Manual/loop_invariant/proc1.rls \ |
|
1556 |
SPARK/Manual/loop_invariant/proc1.siv \ |
|
1557 |
SPARK/Manual/loop_invariant/proc2.fdl \ |
|
1558 |
SPARK/Manual/loop_invariant/proc2.rls \ |
|
1559 |
SPARK/Manual/loop_invariant/proc2.siv \ |
|
1560 |
SPARK/Manual/simple_greatest_common_divisor/g_c_d.fdl \ |
|
1561 |
SPARK/Manual/simple_greatest_common_divisor/g_c_d.rls \ |
|
1562 |
SPARK/Manual/simple_greatest_common_divisor/g_c_d.siv \ |
|
1563 |
SPARK/Manual/document/complex_types.ads \ |
|
1564 |
SPARK/Manual/document/complex_types_app.adb \ |
|
1565 |
SPARK/Manual/document/complex_types_app.ads \ |
|
1566 |
SPARK/Manual/document/loop_invariant.adb \ |
|
1567 |
SPARK/Manual/document/loop_invariant.ads \ |
|
1568 |
SPARK/Manual/document/Simple_Gcd.adb \ |
|
1569 |
SPARK/Manual/document/Simple_Gcd.ads \ |
|
1570 |
SPARK/Manual/document/intro.tex \ |
|
1571 |
SPARK/Manual/document/root.tex \ |
|
1572 |
SPARK/Manual/document/root.bib \ |
|
1573 |
SPARK/Examples/Gcd/Greatest_Common_Divisor.thy \ |
|
1574 |
SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.fdl \ |
|
1575 |
SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.rls \ |
|
1576 |
SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.siv |
|
1577 |
@cd SPARK; $(ISABELLE_TOOL) usedir $(OUT)/HOL-SPARK Manual |
|
1578 |
||
1579 |
||
| 34965 | 1580 |
## HOL-Mutabelle |
1581 |
||
1582 |
HOL-Mutabelle: HOL $(LOG)/HOL-Mutabelle.gz |
|
1583 |
||
1584 |
$(LOG)/HOL-Mutabelle.gz: $(OUT)/HOL Mutabelle/MutabelleExtra.thy \ |
|
| 35959 | 1585 |
Mutabelle/ROOT.ML Mutabelle/mutabelle.ML \ |
| 34965 | 1586 |
Mutabelle/mutabelle_extra.ML |
1587 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mutabelle |
|
1588 |
||
| 46585 | 1589 |
## HOL-Quickcheck_Examples |
1590 |
||
1591 |
HOL-Quickcheck_Examples: HOL $(LOG)/HOL-Quickcheck_Examples.gz |
|
1592 |
||
1593 |
$(LOG)/HOL-Quickcheck_Examples.gz: $(OUT)/HOL \ |
|
| 46591 | 1594 |
Quickcheck_Examples/Find_Unused_Assms_Examples.thy \ |
| 46585 | 1595 |
Quickcheck_Examples/Quickcheck_Examples.thy \ |
1596 |
Quickcheck_Examples/Quickcheck_Lattice_Examples.thy \ |
|
1597 |
Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy |
|
1598 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quickcheck_Examples |
|
| 34965 | 1599 |
|
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
1600 |
## HOL-Quotient_Examples |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
1601 |
|
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
1602 |
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
|
1603 |
|
| 35959 | 1604 |
$(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL \ |
|
45319
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
1605 |
Quotient_Examples/DList.thy Quotient_Examples/Quotient_Cset.thy \ |
|
2b002c6b0f7d
renaming Quotient_Set and List_Quotient_Set to Quotient_Cset and List_Quotient_Cset to avoid name clash with existing Quotient_Set (again, cf. 66823a0066db)
bulwahn
parents:
45267
diff
changeset
|
1606 |
Quotient_Examples/FSet.thy Quotient_Examples/List_Quotient_Cset.thy \ |
|
45536
5b0b1dc2e40f
adding a preliminary example to show how the quotient_definition package can be generalized
bulwahn
parents:
45483
diff
changeset
|
1607 |
Quotient_Examples/Quotient_Int.thy Quotient_Examples/Quotient_Message.thy \ |
| 45800 | 1608 |
Quotient_Examples/Lift_Set.thy Quotient_Examples/Lift_RBT.thy \ |
1609 |
Quotient_Examples/Lift_Fun.thy |
|
|
35222
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
1610 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples |
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
1611 |
|
|
4f1fba00f66d
Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
35151
diff
changeset
|
1612 |
|
|
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
|
1613 |
## 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
|
1614 |
|
|
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
|
1615 |
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
|
1616 |
|
| 35959 | 1617 |
$(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
|
1618 |
Predicate_Compile_Examples/ROOT.ML \ |
|
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
39564
diff
changeset
|
1619 |
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
|
1620 |
Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy \ |
|
38730
5bbdd9a9df62
adding hotel keycard example for prolog generation
bulwahn
parents:
38656
diff
changeset
|
1621 |
Predicate_Compile_Examples/Code_Prolog_Examples.thy \ |
|
39655
8ad7fe9d6f0b
splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
bulwahn
parents:
39564
diff
changeset
|
1622 |
Predicate_Compile_Examples/Examples.thy \ |
| 39185 | 1623 |
Predicate_Compile_Examples/Context_Free_Grammar_Example.thy \ |
| 38948 | 1624 |
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
|
1625 |
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
|
1626 |
Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy \ |
| 39186 | 1627 |
Predicate_Compile_Examples/IMP_1.thy \ |
1628 |
Predicate_Compile_Examples/IMP_2.thy \ |
|
1629 |
Predicate_Compile_Examples/IMP_3.thy \ |
|
1630 |
Predicate_Compile_Examples/IMP_4.thy \ |
|
|
39184
71f3f194b962
adding a List example (challenge from Tobias) for counterexample search
bulwahn
parents:
39183
diff
changeset
|
1631 |
Predicate_Compile_Examples/Lambda_Example.thy \ |
| 39188 | 1632 |
Predicate_Compile_Examples/List_Examples.thy \ |
1633 |
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
|
1634 |
@$(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
|
1635 |
|
| 35959 | 1636 |
|
| 40774 | 1637 |
## HOLCF |
1638 |
||
1639 |
HOLCF: HOL $(OUT)/HOLCF |
|
1640 |
||
1641 |
$(OUT)/HOLCF: $(OUT)/HOL \ |
|
1642 |
HOLCF/ROOT.ML \ |
|
1643 |
HOLCF/Adm.thy \ |
|
1644 |
HOLCF/Algebraic.thy \ |
|
|
41286
3d7685a4a5ff
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
huffman
parents:
41285
diff
changeset
|
1645 |
HOLCF/Bifinite.thy \ |
| 40774 | 1646 |
HOLCF/Cfun.thy \ |
| 41284 | 1647 |
HOLCF/Compact_Basis.thy \ |
| 40774 | 1648 |
HOLCF/Completion.thy \ |
1649 |
HOLCF/Cont.thy \ |
|
1650 |
HOLCF/ConvexPD.thy \ |
|
1651 |
HOLCF/Cpodef.thy \ |
|
1652 |
HOLCF/Cprod.thy \ |
|
1653 |
HOLCF/Discrete.thy \ |
|
1654 |
HOLCF/Deflation.thy \ |
|
1655 |
HOLCF/Domain.thy \ |
|
1656 |
HOLCF/Domain_Aux.thy \ |
|
1657 |
HOLCF/Fixrec.thy \ |
|
1658 |
HOLCF/Fix.thy \ |
|
1659 |
HOLCF/Fun_Cpo.thy \ |
|
1660 |
HOLCF/HOLCF.thy \ |
|
1661 |
HOLCF/Lift.thy \ |
|
1662 |
HOLCF/LowerPD.thy \ |
|
1663 |
HOLCF/Map_Functions.thy \ |
|
1664 |
HOLCF/One.thy \ |
|
1665 |
HOLCF/Pcpo.thy \ |
|
1666 |
HOLCF/Plain_HOLCF.thy \ |
|
1667 |
HOLCF/Porder.thy \ |
|
1668 |
HOLCF/Powerdomains.thy \ |
|
1669 |
HOLCF/Product_Cpo.thy \ |
|
| 41285 | 1670 |
HOLCF/Representable.thy \ |
| 40774 | 1671 |
HOLCF/Sfun.thy \ |
1672 |
HOLCF/Sprod.thy \ |
|
1673 |
HOLCF/Ssum.thy \ |
|
1674 |
HOLCF/Tr.thy \ |
|
1675 |
HOLCF/Universal.thy \ |
|
1676 |
HOLCF/UpperPD.thy \ |
|
1677 |
HOLCF/Up.thy \ |
|
1678 |
HOLCF/Tools/cont_consts.ML \ |
|
1679 |
HOLCF/Tools/cont_proc.ML \ |
|
1680 |
HOLCF/Tools/holcf_library.ML \ |
|
1681 |
HOLCF/Tools/Domain/domain.ML \ |
|
1682 |
HOLCF/Tools/Domain/domain_axioms.ML \ |
|
1683 |
HOLCF/Tools/Domain/domain_constructors.ML \ |
|
1684 |
HOLCF/Tools/Domain/domain_induction.ML \ |
|
1685 |
HOLCF/Tools/Domain/domain_isomorphism.ML \ |
|
1686 |
HOLCF/Tools/Domain/domain_take_proofs.ML \ |
|
1687 |
HOLCF/Tools/cpodef.ML \ |
|
1688 |
HOLCF/Tools/domaindef.ML \ |
|
1689 |
HOLCF/Tools/fixrec.ML \ |
|
1690 |
HOLCF/document/root.tex |
|
1691 |
@cd HOLCF; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOLCF |
|
1692 |
||
1693 |
||
1694 |
## HOLCF-Tutorial |
|
1695 |
||
1696 |
HOLCF-Tutorial: HOLCF $(LOG)/HOLCF-Tutorial.gz |
|
1697 |
||
1698 |
$(LOG)/HOLCF-Tutorial.gz: $(OUT)/HOLCF \ |
|
1699 |
HOLCF/Tutorial/Domain_ex.thy \ |
|
1700 |
HOLCF/Tutorial/Fixrec_ex.thy \ |
|
1701 |
HOLCF/Tutorial/New_Domain.thy \ |
|
1702 |
HOLCF/Tutorial/document/root.tex \ |
|
1703 |
HOLCF/Tutorial/ROOT.ML |
|
|
40777
4898bae6ef23
fix cut-and-paste errors for HOLCF entries in IsaMakefile
huffman
parents:
40774
diff
changeset
|
1704 |
@cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF Tutorial |
| 40774 | 1705 |
|
1706 |
||
1707 |
## HOLCF-Library |
|
1708 |
||
1709 |
HOLCF-Library: HOLCF $(LOG)/HOLCF-Library.gz |
|
1710 |
||
1711 |
$(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \ |
|
| 43919 | 1712 |
Library/Extended_Nat.thy \ |
| 40774 | 1713 |
HOLCF/Library/Defl_Bifinite.thy \ |
|
41112
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
41087
diff
changeset
|
1714 |
HOLCF/Library/Bool_Discrete.thy \ |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
41087
diff
changeset
|
1715 |
HOLCF/Library/Char_Discrete.thy \ |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
41087
diff
changeset
|
1716 |
HOLCF/Library/HOL_Cpo.thy \ |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
41087
diff
changeset
|
1717 |
HOLCF/Library/Int_Discrete.thy \ |
| 40774 | 1718 |
HOLCF/Library/List_Cpo.thy \ |
|
41112
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
41087
diff
changeset
|
1719 |
HOLCF/Library/List_Predomain.thy \ |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
41087
diff
changeset
|
1720 |
HOLCF/Library/Nat_Discrete.thy \ |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
41087
diff
changeset
|
1721 |
HOLCF/Library/Option_Cpo.thy \ |
| 40774 | 1722 |
HOLCF/Library/Stream.thy \ |
1723 |
HOLCF/Library/Sum_Cpo.thy \ |
|
1724 |
HOLCF/Library/HOLCF_Library.thy \ |
|
1725 |
HOLCF/Library/ROOT.ML |
|
|
44256
c478cd500dc4
IsaMakefile: target HOLCF-Library now compiles HOL/HOLCF/Library instead of HOL/Library
huffman
parents:
44236
diff
changeset
|
1726 |
@cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF Library |
| 40774 | 1727 |
|
1728 |
||
1729 |
## HOLCF-IMP |
|
1730 |
||
1731 |
HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz |
|
1732 |
||
|
40777
4898bae6ef23
fix cut-and-paste errors for HOLCF entries in IsaMakefile
huffman
parents:
40774
diff
changeset
|
1733 |
$(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF \ |
|
4898bae6ef23
fix cut-and-paste errors for HOLCF entries in IsaMakefile
huffman
parents:
40774
diff
changeset
|
1734 |
HOLCF/IMP/HoareEx.thy \ |
|
4898bae6ef23
fix cut-and-paste errors for HOLCF entries in IsaMakefile
huffman
parents:
40774
diff
changeset
|
1735 |
HOLCF/IMP/Denotational.thy \ |
|
4898bae6ef23
fix cut-and-paste errors for HOLCF entries in IsaMakefile
huffman
parents:
40774
diff
changeset
|
1736 |
HOLCF/IMP/ROOT.ML \ |
|
4898bae6ef23
fix cut-and-paste errors for HOLCF entries in IsaMakefile
huffman
parents:
40774
diff
changeset
|
1737 |
HOLCF/IMP/document/root.tex |
|
4898bae6ef23
fix cut-and-paste errors for HOLCF entries in IsaMakefile
huffman
parents:
40774
diff
changeset
|
1738 |
@cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF IMP |
| 40774 | 1739 |
|
1740 |
||
1741 |
## HOLCF-ex |
|
1742 |
||
1743 |
HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz |
|
1744 |
||
1745 |
$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF \ |
|
|
43524
d75e285fcf3e
add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
huffman
parents:
43438
diff
changeset
|
1746 |
HOLCF/ex/Concurrency_Monad.thy \ |
| 40774 | 1747 |
HOLCF/ex/Dagstuhl.thy \ |
1748 |
HOLCF/ex/Dnat.thy \ |
|
1749 |
HOLCF/ex/Domain_Proofs.thy \ |
|
1750 |
HOLCF/ex/Fix2.thy \ |
|
1751 |
HOLCF/ex/Focus_ex.thy \ |
|
1752 |
HOLCF/ex/Hoare.thy \ |
|
1753 |
HOLCF/ex/Letrec.thy \ |
|
1754 |
HOLCF/ex/Loop.thy \ |
|
1755 |
HOLCF/ex/Pattern_Match.thy \ |
|
1756 |
HOLCF/ex/Powerdomain_ex.thy \ |
|
1757 |
HOLCF/ex/ROOT.ML |
|
|
40777
4898bae6ef23
fix cut-and-paste errors for HOLCF entries in IsaMakefile
huffman
parents:
40774
diff
changeset
|
1758 |
@cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex |
| 40774 | 1759 |
|
1760 |
||
1761 |
## HOLCF-FOCUS |
|
1762 |
||
1763 |
HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz |
|
1764 |
||
|
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
41407
diff
changeset
|
1765 |
$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF HOLCF/FOCUS/ROOT.ML \ |
| 43919 | 1766 |
Library/Extended_Nat.thy \ |
| 40774 | 1767 |
HOLCF/Library/Stream.thy \ |
1768 |
HOLCF/FOCUS/Fstreams.thy \ |
|
|
40777
4898bae6ef23
fix cut-and-paste errors for HOLCF entries in IsaMakefile
huffman
parents:
40774
diff
changeset
|
1769 |
HOLCF/FOCUS/Fstream.thy \ |
|
4898bae6ef23
fix cut-and-paste errors for HOLCF entries in IsaMakefile
huffman
parents:
40774
diff
changeset
|
1770 |
HOLCF/FOCUS/FOCUS.thy \ |
|
4898bae6ef23
fix cut-and-paste errors for HOLCF entries in IsaMakefile
huffman
parents:
40774
diff
changeset
|
1771 |
HOLCF/FOCUS/Stream_adm.thy \ |
|
4898bae6ef23
fix cut-and-paste errors for HOLCF entries in IsaMakefile
huffman
parents:
40774
diff
changeset
|
1772 |
HOLCF/FOCUS/Buffer.thy \ |
|
4898bae6ef23
fix cut-and-paste errors for HOLCF entries in IsaMakefile
huffman
parents:
40774
diff
changeset
|
1773 |
HOLCF/FOCUS/Buffer_adm.thy \ |
|
4898bae6ef23
fix cut-and-paste errors for HOLCF entries in IsaMakefile
huffman
parents:
40774
diff
changeset
|
1774 |
Library/Continuity.thy |
|
4898bae6ef23
fix cut-and-paste errors for HOLCF entries in IsaMakefile
huffman
parents:
40774
diff
changeset
|
1775 |
@cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF FOCUS |
|
4898bae6ef23
fix cut-and-paste errors for HOLCF entries in IsaMakefile
huffman
parents:
40774
diff
changeset
|
1776 |
|
| 40774 | 1777 |
|
1778 |
## IOA |
|
1779 |
||
1780 |
IOA: HOLCF $(OUT)/IOA |
|
1781 |
||
1782 |
$(OUT)/IOA: $(OUT)/HOLCF \ |
|
1783 |
HOLCF/IOA/ROOT.ML \ |
|
1784 |
HOLCF/IOA/meta_theory/Traces.thy \ |
|
1785 |
HOLCF/IOA/meta_theory/Asig.thy \ |
|
1786 |
HOLCF/IOA/meta_theory/CompoScheds.thy \ |
|
1787 |
HOLCF/IOA/meta_theory/CompoTraces.thy \ |
|
1788 |
HOLCF/IOA/meta_theory/Seq.thy \ |
|
1789 |
HOLCF/IOA/meta_theory/RefCorrectness.thy \ |
|
1790 |
HOLCF/IOA/meta_theory/Automata.thy \ |
|
1791 |
HOLCF/IOA/meta_theory/ShortExecutions.thy \ |
|
1792 |
HOLCF/IOA/meta_theory/IOA.thy \ |
|
1793 |
HOLCF/IOA/meta_theory/Sequence.thy \ |
|
1794 |
HOLCF/IOA/meta_theory/CompoExecs.thy \ |
|
1795 |
HOLCF/IOA/meta_theory/RefMappings.thy \ |
|
1796 |
HOLCF/IOA/meta_theory/Compositionality.thy \ |
|
1797 |
HOLCF/IOA/meta_theory/TL.thy \ |
|
1798 |
HOLCF/IOA/meta_theory/TLS.thy \ |
|
1799 |
HOLCF/IOA/meta_theory/LiveIOA.thy \ |
|
1800 |
HOLCF/IOA/meta_theory/Pred.thy \ |
|
1801 |
HOLCF/IOA/meta_theory/Abstraction.thy \ |
|
1802 |
HOLCF/IOA/meta_theory/Simulations.thy \ |
|
1803 |
HOLCF/IOA/meta_theory/SimCorrectness.thy |
|
1804 |
@cd HOLCF/IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA |
|
1805 |
||
|
40777
4898bae6ef23
fix cut-and-paste errors for HOLCF entries in IsaMakefile
huffman
parents:
40774
diff
changeset
|
1806 |
|
| 40774 | 1807 |
## IOA-ABP |
1808 |
||
1809 |
IOA-ABP: IOA $(LOG)/IOA-ABP.gz |
|
1810 |
||
1811 |
$(LOG)/IOA-ABP.gz: $(OUT)/IOA \ |
|
1812 |
HOLCF/IOA/ABP/Abschannel.thy \ |
|
1813 |
HOLCF/IOA/ABP/Abschannel_finite.thy \ |
|
1814 |
HOLCF/IOA/ABP/Action.thy \ |
|
1815 |
HOLCF/IOA/ABP/Check.ML \ |
|
1816 |
HOLCF/IOA/ABP/Correctness.thy \ |
|
1817 |
HOLCF/IOA/ABP/Env.thy \ |
|
1818 |
HOLCF/IOA/ABP/Impl.thy \ |
|
1819 |
HOLCF/IOA/ABP/Impl_finite.thy \ |
|
1820 |
HOLCF/IOA/ABP/Lemmas.thy \ |
|
1821 |
HOLCF/IOA/ABP/Packet.thy \ |
|
1822 |
HOLCF/IOA/ABP/ROOT.ML \ |
|
1823 |
HOLCF/IOA/ABP/Receiver.thy \ |
|
1824 |
HOLCF/IOA/ABP/Sender.thy \ |
|
1825 |
HOLCF/IOA/ABP/Spec.thy |
|
1826 |
@cd HOLCF/IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ABP |
|
1827 |
||
|
40777
4898bae6ef23
fix cut-and-paste errors for HOLCF entries in IsaMakefile
huffman
parents:
40774
diff
changeset
|
1828 |
|
| 40774 | 1829 |
## IOA-NTP |
1830 |
||
1831 |
IOA-NTP: IOA $(LOG)/IOA-NTP.gz |
|
1832 |
||
1833 |
$(LOG)/IOA-NTP.gz: $(OUT)/IOA \ |
|
1834 |
HOLCF/IOA/NTP/Abschannel.thy \ |
|
1835 |
HOLCF/IOA/NTP/Action.thy \ |
|
1836 |
HOLCF/IOA/NTP/Correctness.thy \ |
|
1837 |
HOLCF/IOA/NTP/Impl.thy \ |
|
1838 |
HOLCF/IOA/NTP/Lemmas.thy \ |
|
1839 |
HOLCF/IOA/NTP/Multiset.thy \ |
|
1840 |
HOLCF/IOA/NTP/Packet.thy \ |
|
1841 |
HOLCF/IOA/NTP/ROOT.ML \ |
|
1842 |
HOLCF/IOA/NTP/Receiver.thy \ |
|
1843 |
HOLCF/IOA/NTP/Sender.thy \ |
|
1844 |
HOLCF/IOA/NTP/Spec.thy |
|
1845 |
@cd HOLCF/IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA NTP |
|
1846 |
||
1847 |
||
1848 |
## IOA-Storage |
|
1849 |
||
1850 |
IOA-Storage: IOA $(LOG)/IOA-Storage.gz |
|
1851 |
||
1852 |
$(LOG)/IOA-Storage.gz: $(OUT)/IOA \ |
|
1853 |
HOLCF/IOA/Storage/Action.thy \ |
|
1854 |
HOLCF/IOA/Storage/Correctness.thy \ |
|
1855 |
HOLCF/IOA/Storage/Impl.thy \ |
|
1856 |
HOLCF/IOA/Storage/ROOT.ML \ |
|
1857 |
HOLCF/IOA/Storage/Spec.thy |
|
1858 |
@cd HOLCF/IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA Storage |
|
1859 |
||
1860 |
||
1861 |
## IOA-ex |
|
1862 |
||
1863 |
IOA-ex: IOA $(LOG)/IOA-ex.gz |
|
1864 |
||
1865 |
$(LOG)/IOA-ex.gz: $(OUT)/IOA \ |
|
1866 |
HOLCF/IOA/ex/ROOT.ML \ |
|
1867 |
HOLCF/IOA/ex/TrivEx.thy \ |
|
1868 |
HOLCF/IOA/ex/TrivEx2.thy |
|
1869 |
@cd HOLCF/IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ex |
|
1870 |
||
1871 |
||
| 45860 | 1872 |
|
1873 |
## HOL-Datatype_Benchmark |
|
1874 |
||
1875 |
HOL-Datatype_Benchmark: HOL $(LOG)/HOL-Datatype_Benchmark.gz |
|
1876 |
||
1877 |
$(LOG)/HOL-Datatype_Benchmark.gz: $(OUT)/HOL \ |
|
1878 |
Datatype_Benchmark/ROOT.ML Datatype_Benchmark/Brackin.thy \ |
|
1879 |
Datatype_Benchmark/Instructions.thy Datatype_Benchmark/SML.thy \ |
|
1880 |
Datatype_Benchmark/Verilog.thy |
|
1881 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Datatype_Benchmark |
|
1882 |
||
1883 |
||
1884 |
## HOL-Record_Benchmark |
|
1885 |
||
1886 |
HOL-Record_Benchmark: HOL $(LOG)/HOL-Record_Benchmark.gz |
|
1887 |
||
1888 |
$(LOG)/HOL-Record_Benchmark.gz: $(OUT)/HOL Record_Benchmark/ROOT.ML \ |
|
1889 |
Record_Benchmark/Record_Benchmark.thy |
|
1890 |
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Record_Benchmark |
|
1891 |
||
1892 |
||
1893 |
||
| 4518 | 1894 |
## clean |
| 4447 | 1895 |
|
1896 |
clean: |
|
| 33450 | 1897 |
@rm -f $(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz \ |
1898 |
$(LOG)/HOL-Bali.gz $(LOG)/HOL-Base.gz \ |
|
1899 |
$(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
|
1900 |
$(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
|
1901 |
$(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
|
1902 |
$(LOG)/HOL-IMP.gz $(LOG)/HOL-IMPP.gz $(LOG)/HOL-IOA.gz \ |
| 33450 | 1903 |
$(LOG)/HOL-Imperative_HOL.gz $(LOG)/HOL-Import.gz \ |
1904 |
$(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
|
1905 |
$(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
|
1906 |
$(LOG)/HOL-Lex.gz $(LOG)/HOL-Library.gz \ |
| 46650 | 1907 |
$(LOG)/HOL-Library-Codegenerator_Test.gz \ |
|
46988
9f492f5b0cec
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset
|
1908 |
$(LOG)/HOL-Main.gz $(LOG)/HOL-Matrix_LP.gz \ |
|
9f492f5b0cec
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset
|
1909 |
$(LOG)/HOL-Metis_Examples.gz $(LOG)/HOL-MicroJava.gz \ |
|
9f492f5b0cec
renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;
wenzelm
parents:
46951
diff
changeset
|
1910 |
$(LOG)/HOL-Mirabelle.gz \ |
| 33450 | 1911 |
$(LOG)/HOL-Multivariate_Analysis.gz \ |
| 46650 | 1912 |
$(LOG)/HOL-Mutabelle.gz $(LOG)/HOL-NSA-Examples.gz \ |
1913 |
$(LOG)/HOL-NSA.gz $(LOG)/HOL-NanoJava.gz \ |
|
1914 |
$(LOG)/HOL-Nitpick_Examples.gz \ |
|
| 33450 | 1915 |
$(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-Nominal.gz \ |
1916 |
$(LOG)/HOL-Number_Theory.gz \ |
|
1917 |
$(LOG)/HOL-Old_Number_Theory.gz $(LOG)/HOL-Plain.gz \ |
|
| 35959 | 1918 |
$(LOG)/HOL-Predicate_Compile_Examples.gz \ |
| 33450 | 1919 |
$(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
|
1920 |
$(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
|
1921 |
$(LOG)/HOL-Proofs-Extraction.gz \ |
| 46650 | 1922 |
$(LOG)/HOL-Proofs-Lambda.gz \ |
1923 |
$(LOG)/HOL-Quickcheck_Examples.gz \ |
|
1924 |
$(LOG)/HOL-Quotient_Examples.gz \ |
|
1925 |
$(LOG)/HOL-SET_Protocol.gz \ |
|
| 45860 | 1926 |
$(LOG)/HOL-Word-SMT_Examples.gz $(LOG)/HOL-SPARK.gz \ |
1927 |
$(LOG)/HOL-SPARK-Examples.gz \ |
|
1928 |
$(LOG)/HOL-SPARK-Manual.gz $(LOG)/HOL-Statespace.gz \ |
|
| 46650 | 1929 |
$(LOG)/HOL-TPTP.gz $(LOG)/HOL-UNITY.gz \ |
1930 |
$(LOG)/HOL-Unix.gz $(LOG)/HOL-Word-Examples.gz \ |
|
1931 |
$(LOG)/HOL-Word.gz $(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz \ |
|
1932 |
$(LOG)/HOL.gz $(LOG)/HOL4.gz $(LOG)/TLA-Buffer.gz \ |
|
1933 |
$(LOG)/TLA-Inc.gz $(LOG)/TLA-Memory.gz $(LOG)/TLA.gz \ |
|
1934 |
$(OUT)/HOL $(OUT)/HOL-Algebra $(OUT)/HOL-Base \ |
|
1935 |
$(OUT)/HOL-Boogie $(OUT)/HOL-IMP $(OUT)/HOL-Library \ |
|
1936 |
$(OUT)/HOL-Main $(OUT)/HOL-Multivariate_Analysis \ |
|
1937 |
$(OUT)/HOL-NSA $(OUT)/HOL-Nominal $(OUT)/HOL-Plain \ |
|
| 35931 | 1938 |
$(OUT)/HOL-Probability $(OUT)/HOL-Proofs \ |
| 45860 | 1939 |
$(OUT)/HOL-SPARK $(OUT)/HOL-Word $(OUT)/HOL4 \ |
1940 |
$(OUT)/TLA $(OUT)/HOLCF $(LOG)/HOLCF.gz \ |
|
1941 |
$(LOG)/HOLCF-IMP.gz $(LOG)/HOLCF-ex.gz \ |
|
1942 |
$(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA $(LOG)/IOA.gz \ |
|
1943 |
$(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \ |
|
| 40774 | 1944 |
$(LOG)/IOA-Storage.gz $(LOG)/HOLCF-Library.gz \ |
| 45860 | 1945 |
$(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz \ |
1946 |
$(LOG)/HOL-Datatype_Benchmark.gz \ |
|
1947 |
$(LOG)/HOL-Record_Benchmark.gz |