isabelle: src/HOL/IsaMakefile@42330f25142c (annotated)

2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	1	#
61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	2	# IsaMakefile for HOL
61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	3	#
61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	4
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	5	## targets
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	6
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	7	default: HOL
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	8	generate: HOL-Generate-HOL HOL-Generate-HOLLight
33210 94ae82a4452f recovered sort indentation for "sort position", as documented in the file; wenzelm parents: 33204 diff changeset	9
94ae82a4452f recovered sort indentation for "sort position", as documented in the file; wenzelm parents: 33204 diff changeset	10	images: \
94ae82a4452f recovered sort indentation for "sort position", as documented in the file; wenzelm parents: 33204 diff changeset	11	HOL \
37691 4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test haftmann parents: 37672 diff changeset	12	HOL-Library \
33210 94ae82a4452f recovered sort indentation for "sort position", as documented in the file; wenzelm parents: 33204 diff changeset	13	HOL-Algebra \
33419 8ae45e87b992 added HOL-Boogie boehmes parents: 33356 diff changeset	14	HOL-Boogie \
33210 94ae82a4452f recovered sort indentation for "sort position", as documented in the file; wenzelm parents: 33204 diff changeset	15	HOL-Multivariate_Analysis \
94ae82a4452f recovered sort indentation for "sort position", as documented in the file; wenzelm parents: 33204 diff changeset	16	HOL-NSA \
94ae82a4452f recovered sort indentation for "sort position", as documented in the file; wenzelm parents: 33204 diff changeset	17	HOL-Nominal \
34205 f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.; wenzelm parents: 34126 diff changeset	18	HOL-Proofs \
41566 676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	19	HOL-SPARK \
33210 94ae82a4452f recovered sort indentation for "sort position", as documented in the file; wenzelm parents: 33204 diff changeset	20	HOL-Word \
94ae82a4452f recovered sort indentation for "sort position", as documented in the file; wenzelm parents: 33204 diff changeset	21	HOL4 \
40774 0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	22	HOLCF \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	23	IOA \
37691 4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test haftmann parents: 37672 diff changeset	24	TLA \
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test haftmann parents: 37672 diff changeset	25	HOL-Base \
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test haftmann parents: 37672 diff changeset	26	HOL-Main \
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test haftmann parents: 37672 diff changeset	27	HOL-Plain
10135 c2a4dccf6e67 reorganized AxClasses; wenzelm parents: 10094 diff changeset	28
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	29	#Note: keep targets sorted
10157 6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	30	test: \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	31	HOL-Auth \
14031 3240066af013 Added Bali to test schirmer parents: 14029 diff changeset	32	HOL-Bali \
33439 f5d95787224f more accurate dependencies; wenzelm parents: 33437 diff changeset	33	HOL-Boogie-Examples \
31795 be3e1cc5005c standard naming conventions for session and theories; wenzelm parents: 31771 diff changeset	34	HOL-Hahn_Banach \
10157 6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	35	HOL-Hoare \
32621 a073cb249a06 theory entry point for session Hoare_Parallel (now also with proper underscore) haftmann parents: 32618 diff changeset	36	HOL-Hoare_Parallel \
40774 0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	37	HOLCF-FOCUS \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	38	HOLCF-IMP \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	39	HOLCF-Library \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	40	HOLCF-Tutorial \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	41	HOLCF-ex \
10157 6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	42	HOL-IMP \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	43	HOL-IMPP \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	44	HOL-IOA \
40774 0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	45	IOA-ABP \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	46	IOA-NTP \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	47	IOA-Storage \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	48	IOA-ex \
29399 ebcd69a00872 split of Imperative_HOL theories from HOL-Library haftmann parents: 29197 diff changeset	49	HOL-Imperative_HOL \
33210 94ae82a4452f recovered sort indentation for "sort position", as documented in the file; wenzelm parents: 33204 diff changeset	50	HOL-Import \
10157 6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	51	HOL-Induct \
33026 8f35633c4922 modernized session Isar_Examples; wenzelm parents: 33024 diff changeset	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 3a699743bcba more accurate dependencies haftmann parents: 37742 diff changeset	54	HOL-Library-Codegenerator_Test \
28637 7aabaf1ba263 reactivated HOL-Matrix; wenzelm parents: 28612 diff changeset	55	HOL-Matrix \
33027 9cf389429f6d modernized session Metis_Examples; wenzelm parents: 33026 diff changeset	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 4ab00a2642c3 moved Mirabelle from HOL/Tools to HOL, boehmes parents: 32479 diff changeset	58	HOL-Mirabelle \
35536 1f980bbc6ad8 adding HOL-Mutabelle to tests bulwahn parents: 35502 diff changeset	59	HOL-Mutabelle \
11376 bf98ad1c22c6 added NanoJava oheimb parents: 11370 diff changeset	60	HOL-NanoJava \
33197 de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: 33192 diff changeset	61	HOL-Nitpick_Examples \
32479 521cc9bf2958 some reorganization of number theory haftmann parents: 32402 diff changeset	62	HOL-Number_Theory \
521cc9bf2958 some reorganization of number theory haftmann parents: 32402 diff changeset	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 9aa8bfb1649d modernized session SET_Protocol; wenzelm parents: 33027 diff changeset	69	HOL-SET_Protocol \
41569 98f59921c420 Also added SPARK to test and clean targets. berghofe parents: 41566 diff changeset	70	HOL-SPARK-Examples \
36933 705b58fde476 more precise dependencies for HOL-Word-SMT_Examples; wenzelm parents: 36916 diff changeset	71	HOL-Word-SMT_Examples \
25171 4a9c25bffc9b added Statespace library schirmer parents: 24994 diff changeset	72	HOL-Statespace \
10157 6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	73	HOL-Subst \
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 \
10157 6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	77	HOL-UNITY \
10966 8f2c27041a8e added HOL-Unix example; wenzelm parents: 10945 diff changeset	78	HOL-Unix \
24442 39e29972cb96 HOL-Word-Examples huffman parents: 24411 diff changeset	79	HOL-Word-Examples \
24325 5c29e8822f50 make HOL-ex earlier; wenzelm parents: 24288 diff changeset	80	HOL-ZF
10157 6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	81	# ^ this is the sort position
10614 d5c14e205c24 added Library/Rational_Numbers.thy; wenzelm parents: 10574 diff changeset	82
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	83	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	84	HOL-Probability
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	85
42138 e54a985daa61 added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj"; krauss parents: 42071 diff changeset	86	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	87	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	88	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	89	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	90	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	91
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	all: test-no-smlnj test images-no-smlnj images
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	smlnj: test images
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	94
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	95	## global settings
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	96
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	97	SRC = $(ISABELLE_HOME)/src
3118 24dae6222579 fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?); wenzelm parents: 3079 diff changeset	98	OUT = $(ISABELLE_OUTPUT)
4447 b7ee449eb345 log files; wenzelm parents: 4289 diff changeset	99	LOG = $(OUT)/log
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	100
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	101
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	102	## HOL
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	103
28393 30ba169e8c45 HOL no longer depends on HOL-Plain; wenzelm parents: 28376 diff changeset	104	HOL: Pure $(OUT)/HOL
27368 9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	105
29505 c6d2d23909d1 added HOL-Base image haftmann parents: 29463 diff changeset	106	HOL-Base: Pure $(OUT)/HOL-Base
c6d2d23909d1 added HOL-Base image haftmann parents: 29463 diff changeset	107
27368 9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	108	HOL-Plain: Pure $(OUT)/HOL-Plain
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	109
28401 d5f39173444c separate HOL-Main image haftmann parents: 28393 diff changeset	110	HOL-Main: Pure $(OUT)/HOL-Main
d5f39173444c separate HOL-Main image haftmann parents: 28393 diff changeset	111
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	112	Pure:
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	113	@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	114
27694 31a8e0908b9f corrected Pure dependency haftmann parents: 27679 diff changeset	115	$(OUT)/Pure: Pure
31a8e0908b9f corrected Pure dependency haftmann parents: 27679 diff changeset	116
36073 54a9f56fae7c slightly more standard dependencies; wenzelm parents: 36066 diff changeset	117	BASE_DEPENDENCIES = $(OUT)/Pure \
30160 5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete; wenzelm parents: 30101 diff changeset	118	$(SRC)/Provers/blast.ML \
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete; wenzelm parents: 30101 diff changeset	119	$(SRC)/Provers/clasimp.ML \
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete; wenzelm parents: 30101 diff changeset	120	$(SRC)/Provers/classical.ML \
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete; wenzelm parents: 30101 diff changeset	121	$(SRC)/Provers/hypsubst.ML \
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete; wenzelm parents: 30101 diff changeset	122	$(SRC)/Provers/quantifier1.ML \
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete; wenzelm parents: 30101 diff changeset	123	$(SRC)/Provers/splitter.ML \
37818 dd65033fed78 load cache_io before code generator; moved adhoc-overloading to generic tools haftmann parents: 37790 diff changeset	124	$(SRC)/Tools/cache_io.ML \
31771 1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	125	$(SRC)/Tools/Code/code_haskell.ML \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	126	$(SRC)/Tools/Code/code_ml.ML \
38970 53d1ee3d98b8 factored out generic part of Scala serializer into code_namespace.ML haftmann parents: 38965 diff changeset	127	$(SRC)/Tools/Code/code_namespace.ML \
31771 1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	128	$(SRC)/Tools/Code/code_preproc.ML \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	129	$(SRC)/Tools/Code/code_printer.ML \
39402 24d70f4e690d more accurate dependencies haftmann parents: 39394 diff changeset	130	$(SRC)/Tools/Code/code_runtime.ML \
34945 478f31081a78 more accurate dependencies haftmann parents: 34228 diff changeset	131	$(SRC)/Tools/Code/code_scala.ML \
37442 037ee7b712b2 added code_simp infrastructure haftmann parents: 37296 diff changeset	132	$(SRC)/Tools/Code/code_simp.ML \
31771 1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	133	$(SRC)/Tools/Code/code_target.ML \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	134	$(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	135	$(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	136	$(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	137	$(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	138	$(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	139	$(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	140	$(SRC)/Tools/atomize_elim.ML \
39323 ce5c6a8b0359 start renaming "Auto_Counterexample" to "Auto_Tools"; blanchet parents: 39271 diff changeset	141	$(SRC)/Tools/auto_tools.ML \
41827 98eda7ffde79 setup case_product attribute in HOL and FOL noschinl parents: 41655 diff changeset	142	$(SRC)/Tools/case_product.ML \
30160 5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete; wenzelm parents: 30101 diff changeset	143	$(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	144	$(SRC)/Tools/cong_tac.ML \
30160 5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete; wenzelm parents: 30101 diff changeset	145	$(SRC)/Tools/eqsubst.ML \
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete; wenzelm parents: 30101 diff changeset	146	$(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	147	$(SRC)/Tools/induct_tacs.ML \
30165 6ee87f67d9cd moved generic intuitionistic prover to src/Tools/intuitionistic.ML; wenzelm parents: 30160 diff changeset	148	$(SRC)/Tools/intuitionistic.ML \
37781 2fbbf0a48cef moved misc legacy stuff from OldGoals to Misc_Legacy; wenzelm parents: 37779 diff changeset	149	$(SRC)/Tools/misc_legacy.ML \
30160 5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete; wenzelm parents: 30101 diff changeset	150	$(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	151	$(SRC)/Tools/project_rule.ML \
30973 304ab57afa6e observe distinction between Pure/Tools and Tools more closely haftmann parents: 30954 diff changeset	152	$(SRC)/Tools/quickcheck.ML \
40116 9ed3711366c8 introduced manual version of "Auto Solve" as "solve_direct" blanchet parents: 40067 diff changeset	153	$(SRC)/Tools/solve_direct.ML \
30160 5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete; wenzelm parents: 30101 diff changeset	154	$(SRC)/Tools/value.ML \
29505 c6d2d23909d1 added HOL-Base image haftmann parents: 29463 diff changeset	155	HOL.thy \
c6d2d23909d1 added HOL-Base image haftmann parents: 29463 diff changeset	156	Tools/hologic.ML \
c6d2d23909d1 added HOL-Base image haftmann parents: 29463 diff changeset	157	Tools/recfun_codegen.ML \
36073 54a9f56fae7c slightly more standard dependencies; wenzelm parents: 36066 diff changeset	158	Tools/simpdata.ML
29505 c6d2d23909d1 added HOL-Base image haftmann parents: 29463 diff changeset	159
c6d2d23909d1 added HOL-Base image haftmann parents: 29463 diff changeset	160	$(OUT)/HOL-Base: base.ML $(BASE_DEPENDENCIES)
29523 f83dcdcee6b3 no document for HOL-Base haftmann parents: 29505 diff changeset	161	@$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base
29505 c6d2d23909d1 added HOL-Base image haftmann parents: 29463 diff changeset	162
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	163	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	164	$(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	165	$(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	166	$(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	167	$(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	168	$(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	169	$(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	170	$(SRC)/Tools/rat.ML \
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option; wenzelm parents: 40863 diff changeset	171	$(SRC)/Tools/subtyping.ML \
32139 e271a64f03ff moved complete_lattice &c. into separate theory haftmann parents: 31990 diff changeset	172	Complete_Lattice.thy \
40108 dbab949c2717 integrated partial_function into HOL-Plain krauss parents: 40104 diff changeset	173	Complete_Partial_Order.thy \
27368 9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	174	Datatype.thy \
9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	175	Extraction.thy \
35050 9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields haftmann parents: 35039 diff changeset	176	Fields.thy \
27368 9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	177	Finite_Set.thy \
9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	178	Fun.thy \
9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	179	FunDef.thy \
35050 9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields haftmann parents: 35039 diff changeset	180	Groups.thy \
27368 9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	181	Inductive.thy \
9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	182	Lattices.thy \
39945 277addece9b7 added "Meson" theory to Makefile blanchet parents: 39940 diff changeset	183	Meson.thy \
39946 78faa9b31202 move Metis into Plain blanchet parents: 39945 diff changeset	184	Metis.thy \
27368 9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	185	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	186	Option.thy \
27368 9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	187	Orderings.thy \
40108 dbab949c2717 integrated partial_function into HOL-Plain krauss parents: 40104 diff changeset	188	Partial_Function.thy \
27368 9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	189	Plain.thy \
9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	190	Power.thy \
9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	191	Predicate.thy \
9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	192	Product_Type.thy \
9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	193	Relation.thy \
35050 9f841f20dca6 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields haftmann parents: 35039 diff changeset	194	Rings.thy \
27368 9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	195	SAT.thy \
9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	196	Set.thy \
9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	197	Sum_Type.thy \
40939 2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option; wenzelm parents: 40863 diff changeset	198	Tools/Datatype/datatype.ML \
31771 1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	199	Tools/Datatype/datatype_abs_proofs.ML \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	200	Tools/Datatype/datatype_aux.ML \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	201	Tools/Datatype/datatype_case.ML \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	202	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	203	Tools/Datatype/datatype_data.ML \
31771 1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	204	Tools/Datatype/datatype_prop.ML \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	205	Tools/Datatype/datatype_realizer.ML \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	206	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	207	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	208	Tools/Function/function.ML \
33099 b8cdd3d73022 function package: more standard names for structures and files krauss parents: 33098 diff changeset	209	Tools/Function/function_common.ML \
b8cdd3d73022 function package: more standard names for structures and files krauss parents: 33098 diff changeset	210	Tools/Function/function_core.ML \
b8cdd3d73022 function package: more standard names for structures and files krauss parents: 33098 diff changeset	211	Tools/Function/function_lib.ML \
33471 5aef13872723 renamed method induct_scheme to induction_schema krauss parents: 33469 diff changeset	212	Tools/Function/induction_schema.ML \
31771 1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	213	Tools/Function/lexicographic_order.ML \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	214	Tools/Function/measure_functions.ML \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	215	Tools/Function/mutual.ML \
40108 dbab949c2717 integrated partial_function into HOL-Plain krauss parents: 40104 diff changeset	216	Tools/Function/partial_function.ML \
33083 1fad3160d873 pat_completeness gets its own file krauss parents: 33028 diff changeset	217	Tools/Function/pat_completeness.ML \
31771 1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	218	Tools/Function/pattern_split.ML \
33100 acc2bd3934ba renamed auto_term.ML -> relation.ML krauss parents: 33099 diff changeset	219	Tools/Function/relation.ML \
31771 1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	220	Tools/Function/scnp_reconstruct.ML \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	221	Tools/Function/scnp_solve.ML \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	222	Tools/Function/size.ML \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	223	Tools/Function/sum_tree.ML \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	224	Tools/Function/termination.ML \
39940 1f01c9b2b76b move MESON files together blanchet parents: 39889 diff changeset	225	Tools/Meson/meson.ML \
1f01c9b2b76b move MESON files together blanchet parents: 39889 diff changeset	226	Tools/Meson/meson_clausify.ML \
39948 317010af8972 factor out "Meson_Tactic" from "Meson_Clausify" blanchet parents: 39946 diff changeset	227	Tools/Meson/meson_tactic.ML \
39946 78faa9b31202 move Metis into Plain blanchet parents: 39945 diff changeset	228	Tools/Metis/metis_reconstruct.ML \
40939 2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option; wenzelm parents: 40863 diff changeset	229	Tools/Metis/metis_tactics.ML \
39946 78faa9b31202 move Metis into Plain blanchet parents: 39945 diff changeset	230	Tools/Metis/metis_translate.ML \
40939 2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option; wenzelm parents: 40863 diff changeset	231	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	232	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	233	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	234	Tools/dseq.ML \
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option; wenzelm parents: 40863 diff changeset	235	Tools/inductive.ML \
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option; wenzelm parents: 40863 diff changeset	236	Tools/inductive_codegen.ML \
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option; wenzelm parents: 40863 diff changeset	237	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	238	Tools/inductive_set.ML \
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option; wenzelm parents: 40863 diff changeset	239	Tools/lin_arith.ML \
30496 7cdcc9dd95cb vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement haftmann parents: 30457 diff changeset	240	Tools/nat_arith.ML \
31723 f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package" haftmann parents: 31706 diff changeset	241	Tools/primrec.ML \
27368 9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	242	Tools/prop_logic.ML \
9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	243	Tools/refute.ML \
9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	244	Tools/rewrite_hol_proof.ML \
9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	245	Tools/sat_funcs.ML \
9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	246	Tools/sat_solver.ML \
9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	247	Tools/split_rule.ML \
43016 42330f25142c renamed "try" "try_methods" blanchet parents: 42861 diff changeset	248	Tools/try_methods.ML \
31723 f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package" haftmann parents: 31706 diff changeset	249	Tools/typedef.ML \
41505 6d19301074cf "enriched_type" replaces less specific "type_lifting" haftmann parents: 41496 diff changeset	250	Tools/enriched_type.ML \
27368 9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	251	Transitive_Closure.thy \
9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	252	Typedef.thy \
40939 2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option; wenzelm parents: 40863 diff changeset	253	Wellfounded.thy
28312 f0838044f034 different session branches for HOL-Plain vs. Plain haftmann parents: 28243 diff changeset	254
f0838044f034 different session branches for HOL-Plain vs. Plain haftmann parents: 28243 diff changeset	255	$(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES)
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	256	@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
27368 9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	257
28401 d5f39173444c separate HOL-Main image haftmann parents: 28393 diff changeset	258	MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
40178 00152d17855b reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers blanchet parents: 40162 diff changeset	259	ATP.thy \
35725 4d7e3cc9c52c Big_Operators now in Main rather than Plain src/HOL/Wellfounded.thy haftmann parents: 35719 diff changeset	260	Big_Operators.thy \
32657 5f13912245ff Code_Eval(uation) haftmann parents: 32636 diff changeset	261	Code_Evaluation.thy \
31205 98370b26c2ce String.literal replaces message_string, code_numeral replaces (code_)index haftmann parents: 31203 diff changeset	262	Code_Numeral.thy \
33296 a3924d1069e5 moved theory Divides after theory Nat_Numeral; tuned some proof texts haftmann parents: 33272 diff changeset	263	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	264	DSequence.thy \
27368 9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	265	Equiv_Relations.thy \
40650 d40b347d5b0b adding Enum to HOL-Main image and removing it from HOL-Library bulwahn parents: 40634 diff changeset	266	Enum.thy \
27368 9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	267	Groebner_Basis.thy \
9f90ac19e32b established Plain theory and image haftmann parents: 27326 diff changeset	268	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	269	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	270	Lazy_Sequence.thy \
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	271	List.thy \
7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	272	Main.thy \
7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	273	Map.thy \
30925 c38cbc0ac8d1 theory NatBin now named Nat_Numeral haftmann parents: 30689 diff changeset	274	Nat_Numeral.thy \
33318 ddd97d9dfbfb moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly haftmann parents: 33298 diff changeset	275	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	276	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	277	New_Random_Sequence.thy \
36915 7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong blanchet parents: 36901 diff changeset	278	Nitpick.thy \
33356 9157d0f9f00e moved Commutative_Ring into session Decision_Procs haftmann parents: 33348 diff changeset	279	Numeral_Simprocs.thy \
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	280	Presburger.thy \
33250 5c2af18a3237 including the predicate compiler in HOL-Main; added RandomPredicate monad to Quickcheck bulwahn parents: 33210 diff changeset	281	Predicate_Compile.thy \
31203 5c8fb4fd67e0 moved Code_Index, Random and Quickcheck before Main haftmann parents: 31186 diff changeset	282	Quickcheck.thy \
41919 e180c2a9873b correcting dependencies after renaming bulwahn parents: 41911 diff changeset	283	Quickcheck_Exhaustive.thy \
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35151 diff changeset	284	Quotient.thy \
31203 5c8fb4fd67e0 moved Code_Index, Random and Quickcheck before Main haftmann parents: 31186 diff changeset	285	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	286	Random_Sequence.thy \
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	287	Recdef.thy \
39271 436554f1beaa more correct dependencies haftmann parents: 39223 diff changeset	288	Record.thy \
36916 279074271b8e move Refute dependency from Plain to Main blanchet parents: 36915 diff changeset	289	Refute.thy \
36751 7f1da69cacb3 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces haftmann parents: 36700 diff changeset	290	Semiring_Normalization.thy \
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	291	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	292	Sledgehammer.thy \
36898 8e55aa1306c5 integrated SMT into the HOL image boehmes parents: 36895 diff changeset	293	SMT.thy \
31048 ac146fc38b51 refined HOL string theories and corresponding ML fragments haftmann parents: 31036 diff changeset	294	String.thy \
31203 5c8fb4fd67e0 moved Code_Index, Random and Quickcheck before Main haftmann parents: 31186 diff changeset	295	Typerep.thy \
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	296	$(SRC)/Provers/Arith/assoc_fold.ML \
7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	297	$(SRC)/Provers/Arith/cancel_numeral_factor.ML \
7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	298	$(SRC)/Provers/Arith/cancel_numerals.ML \
7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	299	$(SRC)/Provers/Arith/combine_numerals.ML \
7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	300	$(SRC)/Provers/Arith/extract_common_term.ML \
38047 9033c03cc214 consequence of directory renaming blanchet parents: 38021 diff changeset	301	Tools/ATP/atp_problem.ML \
39452 70a57e40f795 factored out TSTP/SPASS/Vampire proof parsing; blanchet parents: 39432 diff changeset	302	Tools/ATP/atp_proof.ML \
38047 9033c03cc214 consequence of directory renaming blanchet parents: 38021 diff changeset	303	Tools/ATP/atp_systems.ML \
33318 ddd97d9dfbfb moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly haftmann parents: 33298 diff changeset	304	Tools/choice_specification.ML \
39564 acfd10e38e80 Factored out ML into separate file haftmann parents: 39505 diff changeset	305	Tools/code_evaluation.ML \
41919 e180c2a9873b correcting dependencies after renaming bulwahn parents: 41911 diff changeset	306	Tools/groebner.ML \
31068 f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs haftmann parents: 31060 diff changeset	307	Tools/int_arith.ML \
31055 2cf6efca6c71 proper structures for list and string code generation stuff haftmann parents: 31048 diff changeset	308	Tools/list_code.ML \
41463 edbf0a86fb1c adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs bulwahn parents: 41426 diff changeset	309	Tools/list_to_set_comprehension.ML \
31068 f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs haftmann parents: 31060 diff changeset	310	Tools/nat_numeral_simprocs.ML \
36915 7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong blanchet parents: 36901 diff changeset	311	Tools/Nitpick/kodkod.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong blanchet parents: 36901 diff changeset	312	Tools/Nitpick/kodkod_sat.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong blanchet parents: 36901 diff changeset	313	Tools/Nitpick/nitpick.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong blanchet parents: 36901 diff changeset	314	Tools/Nitpick/nitpick_hol.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong blanchet parents: 36901 diff changeset	315	Tools/Nitpick/nitpick_isar.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong blanchet parents: 36901 diff changeset	316	Tools/Nitpick/nitpick_kodkod.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong blanchet parents: 36901 diff changeset	317	Tools/Nitpick/nitpick_model.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong blanchet parents: 36901 diff changeset	318	Tools/Nitpick/nitpick_mono.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong blanchet parents: 36901 diff changeset	319	Tools/Nitpick/nitpick_nut.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong blanchet parents: 36901 diff changeset	320	Tools/Nitpick/nitpick_peephole.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong blanchet parents: 36901 diff changeset	321	Tools/Nitpick/nitpick_preproc.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong blanchet parents: 36901 diff changeset	322	Tools/Nitpick/nitpick_rep.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong blanchet parents: 36901 diff changeset	323	Tools/Nitpick/nitpick_scope.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong blanchet parents: 36901 diff changeset	324	Tools/Nitpick/nitpick_tests.ML \
7c429a484c74 move Nitpick files from "PLAIN_DEPENDENCIES" to "MAIN_DEPENDENCIES", where they belong blanchet parents: 36901 diff changeset	325	Tools/Nitpick/nitpick_util.ML \
42064 f4e53c8630c0 added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter blanchet parents: 42063 diff changeset	326	Tools/Nitpick/nitrox.ML \
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	327	Tools/numeral.ML \
31068 f591144b0f17 modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs haftmann parents: 31060 diff changeset	328	Tools/numeral_simprocs.ML \
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	329	Tools/numeral_syntax.ML \
40141 0e8a4e27a685 adding new predicate compiler files to the IsaMakefile bulwahn parents: 40123 diff changeset	330	Tools/Predicate_Compile/core_data.ML \
0e8a4e27a685 adding new predicate compiler files to the IsaMakefile bulwahn parents: 40123 diff changeset	331	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	332	Tools/Predicate_Compile/predicate_compile_aux.ML \
36046 c3946372f556 putting compilation setup of predicate compiler in a separate file bulwahn parents: 36032 diff changeset	333	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	334	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	335	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	336	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	337	Tools/Predicate_Compile/predicate_compile.ML \
40141 0e8a4e27a685 adding new predicate compiler files to the IsaMakefile bulwahn parents: 40123 diff changeset	338	Tools/Predicate_Compile/predicate_compile_proof.ML \
36032 dfd30b5b4e73 adding specialisation of predicates to the predicate compiler bulwahn parents: 35972 diff changeset	339	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	340	Tools/Predicate_Compile/predicate_compile_pred.ML \
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	341	Tools/Qelim/cooper.ML \
36803 2cad8904c4ff updated references to ML files haftmann parents: 36798 diff changeset	342	Tools/Qelim/cooper_procedure.ML \
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	343	Tools/Qelim/qelim.ML \
41920 d4fb7a418152 moving exhaustive_generators.ML to Quickcheck directory bulwahn parents: 41919 diff changeset	344	Tools/Quickcheck/exhaustive_generators.ML \
41924 107bf5c959d3 correcting dependencies in IsaMakefile bulwahn parents: 41920 diff changeset	345	Tools/Quickcheck/random_generators.ML \
41928 05abcee548a1 adaptions in generators using the common functions bulwahn parents: 41927 diff changeset	346	Tools/Quickcheck/quickcheck_common.ML \
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35151 diff changeset	347	Tools/Quotient/quotient_def.ML \
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35151 diff changeset	348	Tools/Quotient/quotient_info.ML \
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35151 diff changeset	349	Tools/Quotient/quotient_tacs.ML \
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35151 diff changeset	350	Tools/Quotient/quotient_term.ML \
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35151 diff changeset	351	Tools/Quotient/quotient_typ.ML \
31723 f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package" haftmann parents: 31706 diff changeset	352	Tools/recdef.ML \
38394 3142c1e21a0e moved Record.thy from session Plain to Main; avoid variable name acc haftmann parents: 38282 diff changeset	353	Tools/record.ML \
36753 5cf4e9128f22 renamed Normalizer to the more specific Semiring_Normalizer haftmann parents: 36751 diff changeset	354	Tools/semiring_normalizer.ML \
41042 8275f52ac991 load "try" after "Metis" and move "Async_Manager" back to Sledgehammer blanchet parents: 41023 diff changeset	355	Tools/Sledgehammer/async_manager.ML \
41087 d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems blanchet parents: 41065 diff changeset	356	Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML \
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems blanchet parents: 41065 diff changeset	357	Tools/Sledgehammer/sledgehammer_atp_translate.ML \
38986 e34c1b09bb5e shorten a few file names blanchet parents: 38942 diff changeset	358	Tools/Sledgehammer/sledgehammer_filter.ML \
e34c1b09bb5e shorten a few file names blanchet parents: 38942 diff changeset	359	Tools/Sledgehammer/sledgehammer_minimize.ML \
35866 513074557e06 move the Sledgehammer Isar commands together into one file; blanchet parents: 35865 diff changeset	360	Tools/Sledgehammer/sledgehammer_isar.ML \
41087 d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems blanchet parents: 41065 diff changeset	361	Tools/Sledgehammer/sledgehammer_provers.ML \
d7b5fd465198 split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems blanchet parents: 41065 diff changeset	362	Tools/Sledgehammer/sledgehammer_run.ML \
35967 b9659daa5b4b add new file "sledgehammer_util.ML" to setup blanchet parents: 35892 diff changeset	363	Tools/Sledgehammer/sledgehammer_util.ML \
36898 8e55aa1306c5 integrated SMT into the HOL image boehmes parents: 36895 diff changeset	364	Tools/SMT/smtlib_interface.ML \
40277 4e3a3461c1a6 added crafted list of SMT built-in constants boehmes parents: 40239 diff changeset	365	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	366	Tools/SMT/smt_config.ML \
41426 09615ed31f04 re-implemented support for datatypes (including records and typedefs); boehmes parents: 41413 diff changeset	367	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	368	Tools/SMT/smt_failure.ML \
36898 8e55aa1306c5 integrated SMT into the HOL image boehmes parents: 36895 diff changeset	369	Tools/SMT/smt_monomorph.ML \
8e55aa1306c5 integrated SMT into the HOL image boehmes parents: 36895 diff changeset	370	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	371	Tools/SMT/smt_setup_solvers.ML \
36898 8e55aa1306c5 integrated SMT into the HOL image boehmes parents: 36895 diff changeset	372	Tools/SMT/smt_solver.ML \
8e55aa1306c5 integrated SMT into the HOL image boehmes parents: 36895 diff changeset	373	Tools/SMT/smt_translate.ML \
40662 798aad2229c0 added prove reconstruction for injective functions; boehmes parents: 40650 diff changeset	374	Tools/SMT/smt_utils.ML \
36898 8e55aa1306c5 integrated SMT into the HOL image boehmes parents: 36895 diff changeset	375	Tools/SMT/z3_interface.ML \
8e55aa1306c5 integrated SMT into the HOL image boehmes parents: 36895 diff changeset	376	Tools/SMT/z3_model.ML \
8e55aa1306c5 integrated SMT into the HOL image boehmes parents: 36895 diff changeset	377	Tools/SMT/z3_proof_literals.ML \
40662 798aad2229c0 added prove reconstruction for injective functions; boehmes parents: 40650 diff changeset	378	Tools/SMT/z3_proof_methods.ML \
36898 8e55aa1306c5 integrated SMT into the HOL image boehmes parents: 36895 diff changeset	379	Tools/SMT/z3_proof_parser.ML \
8e55aa1306c5 integrated SMT into the HOL image boehmes parents: 36895 diff changeset	380	Tools/SMT/z3_proof_reconstruction.ML \
8e55aa1306c5 integrated SMT into the HOL image boehmes parents: 36895 diff changeset	381	Tools/SMT/z3_proof_tools.ML \
31055 2cf6efca6c71 proper structures for list and string code generation stuff haftmann parents: 31048 diff changeset	382	Tools/string_code.ML \
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	383	Tools/string_syntax.ML \
33318 ddd97d9dfbfb moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly haftmann parents: 33298 diff changeset	384	Tools/transfer.ML \
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	385	Tools/TFL/casesplit.ML \
7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	386	Tools/TFL/dcterm.ML \
7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	387	Tools/TFL/post.ML \
7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	388	Tools/TFL/rules.ML \
7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	389	Tools/TFL/tfl.ML \
7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	390	Tools/TFL/thms.ML \
7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	391	Tools/TFL/thry.ML \
7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	392	Tools/TFL/usyntax.ML \
28477 9339d4dcec8b version of sledgehammer using threads instead of processes, misc cleanup; wenzelm parents: 28476 diff changeset	393	Tools/TFL/utils.ML
28401 d5f39173444c separate HOL-Main image haftmann parents: 28393 diff changeset	394
d5f39173444c separate HOL-Main image haftmann parents: 28393 diff changeset	395	$(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES)
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	396	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
28401 d5f39173444c separate HOL-Main image haftmann parents: 28393 diff changeset	397
34205 f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.; wenzelm parents: 34126 diff changeset	398	HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \
30096 c5497842ee35 new theory of Archimedean fields huffman parents: 30049 diff changeset	399	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	400	Complex.thy \
28952 15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s haftmann parents: 28905 diff changeset	401	Complex_Main.thy \
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s haftmann parents: 28905 diff changeset	402	Deriv.thy \
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s haftmann parents: 28905 diff changeset	403	Fact.thy \
32479 521cc9bf2958 some reorganization of number theory haftmann parents: 32402 diff changeset	404	GCD.thy \
28952 15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s haftmann parents: 28905 diff changeset	405	Lim.thy \
31352 b3b534f06c2d add dependency on Limits.thy huffman parents: 31283 diff changeset	406	Limits.thy \
28952 15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s haftmann parents: 28905 diff changeset	407	Ln.thy \
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s haftmann parents: 28905 diff changeset	408	Log.thy \
32479 521cc9bf2958 some reorganization of number theory haftmann parents: 32402 diff changeset	409	Lubs.thy \
28952 15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s haftmann parents: 28905 diff changeset	410	MacLaurin.thy \
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s haftmann parents: 28905 diff changeset	411	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	412	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	413	RComplete.thy \
35372 ca158c7b1144 renamed theory Rational to Rat haftmann parents: 35329 diff changeset	414	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	415	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	416	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	417	RealVector.thy \
29197 6d4cb27ed19c adapted HOL source structure to distribution layout haftmann parents: 29181 diff changeset	418	SEQ.thy \
28952 15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s haftmann parents: 28905 diff changeset	419	Series.thy \
33269 3b7e2dbbd684 New theory SupInf of the supremum and infimum operators for sets of reals. paulson parents: 33083 diff changeset	420	SupInf.thy \
28952 15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s haftmann parents: 28905 diff changeset	421	Taylor.thy \
40839 48e01d16dd17 activate subtyping/coercions in theory Complex_Main; wenzelm parents: 40837 diff changeset	422	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	423	Tools/float_syntax.ML \
40839 48e01d16dd17 activate subtyping/coercions in theory Complex_Main; wenzelm parents: 40837 diff changeset	424	Transcendental.thy
34205 f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.; wenzelm parents: 34126 diff changeset	425
f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.; wenzelm parents: 34126 diff changeset	426	$(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	427	@$(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	428
7535 599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar) wenzelm parents: 7513 diff changeset	429
10255 bb66874b4750 added HOL/Library, rearranged several files; wenzelm parents: 10214 diff changeset	430	## HOL-Library
bb66874b4750 added HOL/Library, rearranged several files; wenzelm parents: 10214 diff changeset	431
37691 4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test haftmann parents: 37672 diff changeset	432	HOL-Library: HOL $(OUT)/HOL-Library
10255 bb66874b4750 added HOL/Library, rearranged several files; wenzelm parents: 10214 diff changeset	433
38137 6fda94059baa renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1); wenzelm parents: 38119 diff changeset	434	$(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	435	$(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	436	Library/Abstract_Rat.thy $(SRC)/Tools/Adhoc_Overloading.thy \
38137 6fda94059baa renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1); wenzelm parents: 38119 diff changeset	437	Library/AssocList.thy Library/BigO.thy Library/Binomial.thy \
37968 52fdcb76c0af added Code_Natural.thy haftmann parents: 37921 diff changeset	438	Library/Bit.thy Library/Boolean_Algebra.thy Library/Cardinality.thy \
37662 35c060043a5a repaired line ending haftmann parents: 37660 diff changeset	439	Library/Char_nat.thy Library/Code_Char.thy Library/Code_Char_chr.thy \
42841 9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages bulwahn parents: 42602 diff changeset	440	Library/Code_Char_ord.thy Library/Code_Integer.thy Library/Code_Natural.thy \
38119 e00f970425e9 adding Code_Prolog theory to IsaMakefile and HOL-Library root file bulwahn parents: 38074 diff changeset	441	Library/Code_Prolog.thy Tools/Predicate_Compile/code_prolog.ML \
37968 52fdcb76c0af added Code_Natural.thy haftmann parents: 37921 diff changeset	442	Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy \
38137 6fda94059baa renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1); wenzelm parents: 38119 diff changeset	443	Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy \
40650 d40b347d5b0b adding Enum to HOL-Main image and removing it from HOL-Library bulwahn parents: 40634 diff changeset	444	Library/Efficient_Nat.thy Library/Eval_Witness.thy \
41973 15927c040731 add Extended_Reals from AFP/Lower_Semicontinuous hoelzl parents: 41960 diff changeset	445	Library/Executable_Set.thy Library/Extended_Reals.thy \
15927c040731 add Extended_Reals from AFP/Lower_Semicontinuous hoelzl parents: 41960 diff changeset	446	Library/Float.thy Library/Formal_Power_Series.thy \
15927c040731 add Extended_Reals from AFP/Lower_Semicontinuous hoelzl parents: 41960 diff changeset	447	Library/Fraction_Field.thy Library/FrechetDeriv.thy Library/Cset.thy \
15927c040731 add Extended_Reals from AFP/Lower_Semicontinuous hoelzl parents: 41960 diff changeset	448	Library/FuncSet.thy Library/Function_Algebras.thy \
37968 52fdcb76c0af added Code_Natural.thy haftmann parents: 37921 diff changeset	449	Library/Fundamental_Theorem_Algebra.thy Library/Glbs.thy \
52fdcb76c0af added Code_Natural.thy haftmann parents: 37921 diff changeset	450	Library/Indicator_Function.thy Library/Infinite_Set.thy \
52fdcb76c0af added Code_Natural.thy haftmann parents: 37921 diff changeset	451	Library/Inner_Product.thy Library/Kleene_Algebra.thy \
37118 ccae4ecd67f4 eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML; wenzelm parents: 37024 diff changeset	452	Library/LaTeXsugar.thy Library/Lattice_Algebras.thy \
ccae4ecd67f4 eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML; wenzelm parents: 37024 diff changeset	453	Library/Lattice_Syntax.thy Library/Library.thy \
ccae4ecd67f4 eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML; wenzelm parents: 37024 diff changeset	454	Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy \
37790 7fea92005066 uniform do notation for monads krauss parents: 37789 diff changeset	455	Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy \
37818 dd65033fed78 load cache_io before code generator; moved adhoc-overloading to generic tools haftmann parents: 37790 diff changeset	456	Library/Multiset.thy Library/Nat_Bijection.thy \
38137 6fda94059baa renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1); wenzelm parents: 38119 diff changeset	457	Library/Nat_Infinity.thy Library/Nested_Environment.thy \
6fda94059baa renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1); wenzelm parents: 38119 diff changeset	458	Library/Numeral_Type.thy Library/OptionalSugar.thy \
6fda94059baa renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1); wenzelm parents: 38119 diff changeset	459	Library/Order_Relation.thy Library/Permutation.thy \
6fda94059baa renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1); wenzelm parents: 38119 diff changeset	460	Library/Permutations.thy Library/Poly_Deriv.thy \
6fda94059baa renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1); wenzelm parents: 38119 diff changeset	461	Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy \
6fda94059baa renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1); wenzelm parents: 38119 diff changeset	462	Library/Preorder.thy Library/Product_Vector.thy \
6fda94059baa renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1); wenzelm parents: 38119 diff changeset	463	Library/Product_ord.thy Library/Product_plus.thy \
40349 131cf8790a1c moved theory Quicksort from Library/ to ex/ haftmann parents: 40281 diff changeset	464	Library/Quickcheck_Types.thy \
37118 ccae4ecd67f4 eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML; wenzelm parents: 37024 diff changeset	465	Library/Quotient_List.thy Library/Quotient_Option.thy \
ccae4ecd67f4 eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML; wenzelm parents: 37024 diff changeset	466	Library/Quotient_Product.thy Library/Quotient_Sum.thy \
ccae4ecd67f4 eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML; wenzelm parents: 37024 diff changeset	467	Library/Quotient_Syntax.thy Library/Quotient_Type.thy \
ccae4ecd67f4 eliminated slightly odd Library/Library session setup (cf. d7711be8c3a9) which is obsolete due to usedir -f HOL_Library_ROOT.ML; wenzelm parents: 37024 diff changeset	468	Library/RBT.thy Library/RBT_Impl.thy Library/README.html \
38622 86fc906dcd86 split and enriched theory SetsAndFunctions haftmann parents: 38539 diff changeset	469	Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy \
86fc906dcd86 split and enriched theory SetsAndFunctions haftmann parents: 38539 diff changeset	470	Library/Reflection.thy Library/SML_Quickcheck.thy \
41474 60d091240485 renamed Sum_Of_Squares to Sum_of_Squares; wenzelm parents: 41465 diff changeset	471	Library/Sublist_Order.thy Library/Sum_of_Squares.thy \
60d091240485 renamed Sum_Of_Squares to Sum_of_Squares; wenzelm parents: 41465 diff changeset	472	Library/Sum_of_Squares/sos_wrapper.ML \
60d091240485 renamed Sum_Of_Squares to Sum_of_Squares; wenzelm parents: 41465 diff changeset	473	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	474	Library/Transitive_Closure_Table.thy Library/Univ_Poly.thy \
04577a7e0c51 move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex" blanchet parents: 42064 diff changeset	475	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	476	$(SRC)/Tools/adhoc_overloading.ML Library/positivstellensatz.ML \
37789 93f6dcf9ec02 generic ad-hoc overloading via check/uncheck krauss parents: 37781 diff changeset	477	Library/reflection.ML Library/reify_data.ML \
41927 8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators bulwahn parents: 41924 diff changeset	478	Library/Quickcheck_Narrowing.thy \
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators bulwahn parents: 41924 diff changeset	479	Tools/Quickcheck/narrowing_generators.ML \
8759e9d043f9 adding file quickcheck_common to carry common functions of all quickcheck generators bulwahn parents: 41924 diff changeset	480	Tools/Quickcheck/Narrowing_Engine.hs \
37691 4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test haftmann parents: 37672 diff changeset	481	Library/document/root.bib Library/document/root.tex
38137 6fda94059baa renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1); wenzelm parents: 38119 diff changeset	482	@cd Library; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL-Library
10255 bb66874b4750 added HOL/Library, rearranged several files; wenzelm parents: 10214 diff changeset	483
bb66874b4750 added HOL/Library, rearranged several files; wenzelm parents: 10214 diff changeset	484
31795 be3e1cc5005c standard naming conventions for session and theories; wenzelm parents: 31771 diff changeset	485	## HOL-Hahn_Banach
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	486
31795 be3e1cc5005c standard naming conventions for session and theories; wenzelm parents: 31771 diff changeset	487	HOL-Hahn_Banach: HOL $(LOG)/HOL-Hahn_Banach.gz
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	488
31795 be3e1cc5005c standard naming conventions for session and theories; wenzelm parents: 31771 diff changeset	489	$(LOG)/HOL-Hahn_Banach.gz: $(OUT)/HOL Hahn_Banach/Bounds.thy \
be3e1cc5005c standard naming conventions for session and theories; wenzelm parents: 31771 diff changeset	490	Hahn_Banach/Function_Norm.thy Hahn_Banach/Function_Order.thy \
be3e1cc5005c standard naming conventions for session and theories; wenzelm parents: 31771 diff changeset	491	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	492	Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Hahn_Banach/Linearform.thy \
be3e1cc5005c standard naming conventions for session and theories; wenzelm parents: 31771 diff changeset	493	Hahn_Banach/Normed_Space.thy Hahn_Banach/README.html \
be3e1cc5005c standard naming conventions for session and theories; wenzelm parents: 31771 diff changeset	494	Hahn_Banach/ROOT.ML Hahn_Banach/Subspace.thy \
be3e1cc5005c standard naming conventions for session and theories; wenzelm parents: 31771 diff changeset	495	Hahn_Banach/Vector_Space.thy Hahn_Banach/Zorn_Lemma.thy \
be3e1cc5005c standard naming conventions for session and theories; wenzelm parents: 31771 diff changeset	496	Hahn_Banach/document/root.bib Hahn_Banach/document/root.tex
be3e1cc5005c standard naming conventions for session and theories; wenzelm parents: 31771 diff changeset	497	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hahn_Banach
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	498
7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	499
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	500	## HOL-Subst
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	501
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	502	HOL-Subst: HOL $(LOG)/HOL-Subst.gz
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	503
27164 81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	504	$(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.thy Subst/ROOT.ML \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	505	Subst/Subst.thy Subst/UTerm.thy Subst/Unifier.thy Subst/Unify.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	506	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Subst
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	507
61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	508
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	509	## HOL-Induct
2473 3eb12c85846c minor tuning; wenzelm parents: 2448 diff changeset	510
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	511	HOL-Induct: HOL $(LOG)/HOL-Induct.gz
3125 3f0ab2c306f7 Moved induction examples to directory Induct paulson parents: 3118 diff changeset	512
33688 1a97dcd8dc6a moved old SList, LList, LFilter to AFP/Lazy-Lists-II; wenzelm parents: 33649 diff changeset	513	$(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	514	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	515	Induct/QuoDataType.thy Induct/ROOT.ML Induct/Sexp.thy \
35249 7024a8a8f36a more precise dependencies; wenzelm parents: 35222 diff changeset	516	Induct/Sigma_Algebra.thy Induct/ABexp.thy Induct/SList.thy \
7024a8a8f36a more precise dependencies; wenzelm parents: 35222 diff changeset	517	Induct/Term.thy Induct/Tree.thy Induct/document/root.tex
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	518	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Induct
3125 3f0ab2c306f7 Moved induction examples to directory Induct paulson parents: 3118 diff changeset	519
3f0ab2c306f7 Moved induction examples to directory Induct paulson parents: 3118 diff changeset	520
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	521	## HOL-IMP
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	522
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	523	HOL-IMP: HOL $(LOG)/HOL-IMP.gz
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	524
27164 81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	525	$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Compiler0.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	526	IMP/Compiler.thy IMP/Denotation.thy IMP/Expr.thy IMP/Hoare.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	527	IMP/Natural.thy IMP/Examples.thy IMP/Transition.thy IMP/VC.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	528	IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	529	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL IMP
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	530
61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	531
8179 6a0b1037bab3 added forgotten rules to make IMPP oheimb parents: 8177 diff changeset	532	## HOL-IMPP
6a0b1037bab3 added forgotten rules to make IMPP oheimb parents: 8177 diff changeset	533
6a0b1037bab3 added forgotten rules to make IMPP oheimb parents: 8177 diff changeset	534	HOL-IMPP: HOL $(LOG)/HOL-IMPP.gz
6a0b1037bab3 added forgotten rules to make IMPP oheimb parents: 8177 diff changeset	535
27164 81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	536	$(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy \
19803 aa2581752afb removed obsolete ML files; wenzelm parents: 19802 diff changeset	537	IMPP/Natural.thy IMPP/Hoare.thy IMPP/Misc.thy IMPP/EvenOdd.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	538	@$(ISABELLE_TOOL) usedir $(OUT)/HOL IMPP
8179 6a0b1037bab3 added forgotten rules to make IMPP oheimb parents: 8177 diff changeset	539
6a0b1037bab3 added forgotten rules to make IMPP oheimb parents: 8177 diff changeset	540
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	541	## HOL-Import
14516 a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	542
19097 2fc1a6da9366 removed Import/lazy_scan.ML; wenzelm parents: 19085 diff changeset	543	IMPORTER_FILES = Import/lazy_seq.ML Import/proof_kernel.ML Import/replay.ML \
20610 09ef37366a31 moved Import/susp.ML to Pure/General; wenzelm parents: 20598 diff changeset	544	Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \
14516 a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	545	Import/HOL4Syntax.thy Import/HOL4Compat.thy Import/import_syntax.ML \
31723 f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package" haftmann parents: 31706 diff changeset	546	Import/hol4rews.ML Import/import.ML Import/ROOT.ML
14516 a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	547
17323 2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight obua parents: 17308 diff changeset	548	IMPORTER_HOLLIGHT_FILES = Import/proof_kernel.ML Import/replay.ML \
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight obua parents: 17308 diff changeset	549	Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight obua parents: 17308 diff changeset	550	Import/HOL4Syntax.thy Import/HOLLightCompat.thy Import/import_syntax.ML \
31771 1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	551	Import/hol4rews.ML Import/import.ML Import/ROOT.ML
17323 2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight obua parents: 17308 diff changeset	552
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	553	HOL-Import: HOL $(LOG)/HOL-Import.gz
14516 a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	554
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	555	$(LOG)/HOL-Import.gz: $(OUT)/HOL $(IMPORTER_FILES)
37296 1fad5b94c0ae replaced ML pokes by explicit usedir -p; wenzelm parents: 37292 diff changeset	556	@$(ISABELLE_TOOL) usedir -p 0 $(OUT)/HOL Import
14516 a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	557
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	558
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	559	## HOL-Generate-HOL
14516 a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	560
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	561	HOL-Generate-HOL: HOL $(LOG)/HOL-Generate-HOL.gz
14516 a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	562
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	563	$(LOG)/HOL-Generate-HOL.gz: $(OUT)/HOL \
27164 81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	564	$(IMPORTER_FILES) Import/Generate-HOL/GenHOL4Base.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	565	Import/Generate-HOL/GenHOL4Prob.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	566	Import/Generate-HOL/GenHOL4Real.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	567	Import/Generate-HOL/GenHOL4Vec.thy \
14516 a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	568	Import/Generate-HOL/GenHOL4Word32.thy Import/Generate-HOL/ROOT.ML
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	569	@cd Import; $(ISABELLE_TOOL) usedir $(OUT)/HOL Generate-HOL
14516 a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	570
17460 7780d953598c generate: added HOL-Complex-Generate-HOLLight; wenzelm parents: 17430 diff changeset	571
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	572	## HOL-Generate-HOLLight
17460 7780d953598c generate: added HOL-Complex-Generate-HOLLight; wenzelm parents: 17430 diff changeset	573
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	574	HOL-Generate-HOLLight: HOL $(LOG)/HOL-Generate-HOLLight.gz
17323 2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight obua parents: 17308 diff changeset	575
37742 d8e7f473c3a1 tuned tabs haftmann parents: 37691 diff changeset	576	$(LOG)/HOL-Generate-HOLLight.gz: $(OUT)/HOL \
27164 81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	577	$(IMPORTER_HOLLIGHT_FILES) Import/Generate-HOLLight/GenHOLLight.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	578	Import/Generate-HOLLight/ROOT.ML
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	579	@cd Import; $(ISABELLE_TOOL) usedir $(OUT)/HOL Generate-HOLLight
14516 a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	580
17460 7780d953598c generate: added HOL-Complex-Generate-HOLLight; wenzelm parents: 17430 diff changeset	581
14516 a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	582	## HOL-Import-HOL
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	583
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	584	HOL4: HOL $(LOG)/HOL4.gz
14516 a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	585
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	586	HOL_IMPORT_FILES = arithmetic.imp bits.imp boolean_sequence.imp bool.imp \
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	587	bword_arith.imp bword_bitop.imp bword_num.imp combin.imp divides.imp \
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	588	hrat.imp hreal.imp ind_type.imp lim.imp list.imp marker.imp nets.imp \
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	589	numeral.imp num.imp one.imp operator.imp option.imp pair.imp poly.imp \
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	590	powser.imp pred_set.imp prime.imp prim_rec.imp prob_algebra.imp \
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	591	prob_canon.imp prob_extra.imp prob.imp prob_indep.imp prob_pseudo.imp \
23194 085fa3def13b tuned webertj parents: 23193 diff changeset	592	prob_uniform.imp realax.imp real.imp relation.imp res_quan.imp \
085fa3def13b tuned webertj parents: 23193 diff changeset	593	rich_list.imp \
14516 a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	594	seq.imp state_transformer.imp sum.imp topology.imp transc.imp word32.imp \
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	595	word_base.imp word_bitop.imp word_num.imp
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	596
37742 d8e7f473c3a1 tuned tabs haftmann parents: 37691 diff changeset	597	$(LOG)/HOL4.gz: $(OUT)/HOL $(IMPORTER_FILES) \
27164 81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	598	$(HOL_IMPORT_FILES:%=Import/HOL/%) Import/HOL/HOL4Base.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	599	Import/HOL/HOL4Prob.thy Import/HOL/HOL4Real.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	600	Import/HOL/HOL4Vec.thy Import/HOL/HOL4Word32.thy Import/HOL/HOL4.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	601	Import/HOL/ROOT.ML
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	602	@cd Import/HOL; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL4
14516 a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	603
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	604	HOLLight: HOL $(LOG)/HOLLight.gz
17645 940371ea0ff3 added entry for running HOLLight obua parents: 17637 diff changeset	605
37742 d8e7f473c3a1 tuned tabs haftmann parents: 37691 diff changeset	606	$(LOG)/HOLLight.gz: $(OUT)/HOL $(IMPORTER_HOLLIGHT_FILES) \
27164 81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	607	Import/HOLLight/hollight.imp Import/HOLLight/HOLLight.thy \
17645 940371ea0ff3 added entry for running HOLLight obua parents: 17637 diff changeset	608	Import/HOLLight/ROOT.ML
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	609	@cd Import/HOLLight; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOLLight
17645 940371ea0ff3 added entry for running HOLLight obua parents: 17637 diff changeset	610
14516 a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	611
32479 521cc9bf2958 some reorganization of number theory haftmann parents: 32402 diff changeset	612	## HOL-Number_Theory
31719 29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad nipkow parents: 31706 diff changeset	613
32479 521cc9bf2958 some reorganization of number theory haftmann parents: 32402 diff changeset	614	HOL-Number_Theory: HOL $(LOG)/HOL-Number_Theory.gz
31719 29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad nipkow parents: 31706 diff changeset	615
32479 521cc9bf2958 some reorganization of number theory haftmann parents: 32402 diff changeset	616	$(LOG)/HOL-Number_Theory.gz: $(OUT)/HOL $(ALGEBRA_DEPENDENCIES) \
31771 1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	617	Library/Multiset.thy \
32479 521cc9bf2958 some reorganization of number theory haftmann parents: 32402 diff changeset	618	Number_Theory/Binomial.thy \
521cc9bf2958 some reorganization of number theory haftmann parents: 32402 diff changeset	619	Number_Theory/Cong.thy \
521cc9bf2958 some reorganization of number theory haftmann parents: 32402 diff changeset	620	Number_Theory/Fib.thy \
521cc9bf2958 some reorganization of number theory haftmann parents: 32402 diff changeset	621	Number_Theory/MiscAlgebra.thy \
521cc9bf2958 some reorganization of number theory haftmann parents: 32402 diff changeset	622	Number_Theory/Number_Theory.thy \
521cc9bf2958 some reorganization of number theory haftmann parents: 32402 diff changeset	623	Number_Theory/Residues.thy \
521cc9bf2958 some reorganization of number theory haftmann parents: 32402 diff changeset	624	Number_Theory/UniqueFactorization.thy \
521cc9bf2958 some reorganization of number theory haftmann parents: 32402 diff changeset	625	Number_Theory/ROOT.ML
521cc9bf2958 some reorganization of number theory haftmann parents: 32402 diff changeset	626	@$(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	627
31719 29f5b20e8ee8 Added NewNumberTheory by Jeremy Avigad nipkow parents: 31706 diff changeset	628
32479 521cc9bf2958 some reorganization of number theory haftmann parents: 32402 diff changeset	629	## HOL-Old_Number_Theory
9510 dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied paulson parents: 9481 diff changeset	630
32479 521cc9bf2958 some reorganization of number theory haftmann parents: 32402 diff changeset	631	HOL-Old_Number_Theory: HOL $(LOG)/HOL-Old_Number_Theory.gz
9510 dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied paulson parents: 9481 diff changeset	632
37021 87c696bfe839 adjusted haftmann parents: 36962 diff changeset	633	$(LOG)/HOL-Old_Number_Theory.gz: $(OUT)/HOL Library/Permutation.thy \
87c696bfe839 adjusted haftmann parents: 36962 diff changeset	634	Old_Number_Theory/Primes.thy Old_Number_Theory/Fib.thy \
87c696bfe839 adjusted haftmann parents: 36962 diff changeset	635	Old_Number_Theory/Factorization.thy Old_Number_Theory/BijectionRel.thy\
87c696bfe839 adjusted haftmann parents: 36962 diff changeset	636	Old_Number_Theory/Chinese.thy Old_Number_Theory/EulerFermat.thy \
87c696bfe839 adjusted haftmann parents: 36962 diff changeset	637	Old_Number_Theory/IntFact.thy Old_Number_Theory/IntPrimes.thy \
87c696bfe839 adjusted haftmann parents: 36962 diff changeset	638	Old_Number_Theory/WilsonBij.thy Old_Number_Theory/WilsonRuss.thy \
87c696bfe839 adjusted haftmann parents: 36962 diff changeset	639	Old_Number_Theory/Finite2.thy Old_Number_Theory/Int2.thy \
87c696bfe839 adjusted haftmann parents: 36962 diff changeset	640	Old_Number_Theory/EvenOdd.thy Old_Number_Theory/Residues.thy \
87c696bfe839 adjusted haftmann parents: 36962 diff changeset	641	Old_Number_Theory/Euler.thy Old_Number_Theory/Gauss.thy \
32479 521cc9bf2958 some reorganization of number theory haftmann parents: 32402 diff changeset	642	Old_Number_Theory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy \
37021 87c696bfe839 adjusted haftmann parents: 36962 diff changeset	643	Old_Number_Theory/Legacy_GCD.thy Old_Number_Theory/Pocklington.thy \
87c696bfe839 adjusted haftmann parents: 36962 diff changeset	644	Old_Number_Theory/ROOT.ML
32479 521cc9bf2958 some reorganization of number theory haftmann parents: 32402 diff changeset	645	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Old_Number_Theory
9510 dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied paulson parents: 9481 diff changeset	646
dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied paulson parents: 9481 diff changeset	647
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	648	## HOL-Hoare
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	649
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	650	HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	651
27164 81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	652	$(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.thy Hoare/Examples.thy \
42153 fa108629d132 use shared copy of hoare_syntax.ML; wenzelm parents: 42148 diff changeset	653	Hoare/Hoare.thy Hoare/hoare_syntax.ML Hoare/hoare_tac.ML \
fa108629d132 use shared copy of hoare_syntax.ML; wenzelm parents: 42148 diff changeset	654	Hoare/Heap.thy Hoare/Hoare_Logic.thy Hoare/Hoare_Logic_Abort.thy \
27164 81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	655	Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy Hoare/ROOT.ML \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	656	Hoare/ExamplesAbort.thy Hoare/HeapSyntaxAbort.thy \
42153 fa108629d132 use shared copy of hoare_syntax.ML; wenzelm parents: 42148 diff changeset	657	Hoare/SchorrWaite.thy Hoare/Separation.thy Hoare/SepLogHeap.thy \
fa108629d132 use shared copy of hoare_syntax.ML; wenzelm parents: 42148 diff changeset	658	Hoare/document/root.tex Hoare/document/root.bib
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	659	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Hoare
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	660
61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	661
32621 a073cb249a06 theory entry point for session Hoare_Parallel (now also with proper underscore) haftmann parents: 32618 diff changeset	662	## HOL-Hoare_Parallel
12996 7ac0a7e306db Completed annonce of HoareParallel prensani parents: 12951 diff changeset	663
32621 a073cb249a06 theory entry point for session Hoare_Parallel (now also with proper underscore) haftmann parents: 32618 diff changeset	664	HOL-Hoare_Parallel: HOL $(LOG)/HOL-Hoare_Parallel.gz
12996 7ac0a7e306db Completed annonce of HoareParallel prensani parents: 12951 diff changeset	665
32621 a073cb249a06 theory entry point for session Hoare_Parallel (now also with proper underscore) haftmann parents: 32618 diff changeset	666	$(LOG)/HOL-Hoare_Parallel.gz: $(OUT)/HOL Hoare_Parallel/Gar_Coll.thy \
33439 f5d95787224f more accurate dependencies; wenzelm parents: 33437 diff changeset	667	Hoare_Parallel/Graph.thy Hoare_Parallel/Hoare_Parallel.thy \
f5d95787224f more accurate dependencies; wenzelm parents: 33437 diff changeset	668	Hoare_Parallel/Mul_Gar_Coll.thy Hoare_Parallel/OG_Com.thy \
f5d95787224f more accurate dependencies; wenzelm parents: 33437 diff changeset	669	Hoare_Parallel/OG_Examples.thy Hoare_Parallel/OG_Hoare.thy \
f5d95787224f more accurate dependencies; wenzelm parents: 33437 diff changeset	670	Hoare_Parallel/OG_Syntax.thy Hoare_Parallel/OG_Tactics.thy \
f5d95787224f more accurate dependencies; wenzelm parents: 33437 diff changeset	671	Hoare_Parallel/OG_Tran.thy Hoare_Parallel/Quote_Antiquote.thy \
f5d95787224f more accurate dependencies; wenzelm parents: 33437 diff changeset	672	Hoare_Parallel/RG_Com.thy Hoare_Parallel/RG_Examples.thy \
f5d95787224f more accurate dependencies; wenzelm parents: 33437 diff changeset	673	Hoare_Parallel/RG_Hoare.thy Hoare_Parallel/RG_Syntax.thy \
f5d95787224f more accurate dependencies; wenzelm parents: 33437 diff changeset	674	Hoare_Parallel/RG_Tran.thy Hoare_Parallel/ROOT.ML \
f5d95787224f more accurate dependencies; wenzelm parents: 33437 diff changeset	675	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	676	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hoare_Parallel
12996 7ac0a7e306db Completed annonce of HoareParallel prensani parents: 12951 diff changeset	677
7ac0a7e306db Completed annonce of HoareParallel prensani parents: 12951 diff changeset	678
37747 3a699743bcba more accurate dependencies haftmann parents: 37742 diff changeset	679	## HOL-Library-Codegenerator_Test
37691 4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test haftmann parents: 37672 diff changeset	680
37747 3a699743bcba more accurate dependencies haftmann parents: 37742 diff changeset	681	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	682
37747 3a699743bcba more accurate dependencies haftmann parents: 37742 diff changeset	683	$(LOG)/HOL-Library-Codegenerator_Test.gz: $(OUT)/HOL-Library \
37742 d8e7f473c3a1 tuned tabs haftmann parents: 37691 diff changeset	684	Codegenerator_Test/ROOT.ML \
d8e7f473c3a1 tuned tabs haftmann parents: 37691 diff changeset	685	Codegenerator_Test/Candidates.thy \
37691 4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test haftmann parents: 37672 diff changeset	686	Codegenerator_Test/Candidates_Pretty.thy \
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test haftmann parents: 37672 diff changeset	687	Codegenerator_Test/Generate.thy \
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test haftmann parents: 37672 diff changeset	688	Codegenerator_Test/Generate_Pretty.thy
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test haftmann parents: 37672 diff changeset	689	@$(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	690
4915de09b4d3 build image for session HOL-Library; introduced distinct session HOL-Codegenerator_Test haftmann parents: 37672 diff changeset	691
33027 9cf389429f6d modernized session Metis_Examples; wenzelm parents: 33026 diff changeset	692	## HOL-Metis_Examples
23449 dd874e6a3282 integration of Metis prover paulson parents: 23445 diff changeset	693
33027 9cf389429f6d modernized session Metis_Examples; wenzelm parents: 33026 diff changeset	694	HOL-Metis_Examples: HOL $(LOG)/HOL-Metis_Examples.gz
23449 dd874e6a3282 integration of Metis prover paulson parents: 23445 diff changeset	695
41144 509e51b7509a example tuning blanchet parents: 41112 diff changeset	696	$(LOG)/HOL-Metis_Examples.gz: $(OUT)/HOL Metis_Examples/ROOT.ML \
509e51b7509a example tuning blanchet parents: 41112 diff changeset	697	Metis_Examples/Abstraction.thy Metis_Examples/BigO.thy \
42343 118cc349de35 compile blanchet parents: 42338 diff changeset	698	Metis_Examples/BT.thy Metis_Examples/Clausify.thy \
42338 802f2fe7a0c9 started clausifier examples blanchet parents: 42161 diff changeset	699	Metis_Examples/HO_Reas.thy Metis_Examples/Message.thy \
802f2fe7a0c9 started clausifier examples blanchet parents: 42161 diff changeset	700	Metis_Examples/Tarski.thy Metis_Examples/TransClosure.thy \
802f2fe7a0c9 started clausifier examples blanchet parents: 42161 diff changeset	701	Metis_Examples/set.thy
33027 9cf389429f6d modernized session Metis_Examples; wenzelm parents: 33026 diff changeset	702	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples
23449 dd874e6a3282 integration of Metis prover paulson parents: 23445 diff changeset	703
dd874e6a3282 integration of Metis prover paulson parents: 23445 diff changeset	704
33197 de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: 33192 diff changeset	705	## HOL-Nitpick_Examples
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: 33192 diff changeset	706
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: 33192 diff changeset	707	HOL-Nitpick_Examples: HOL $(LOG)/HOL-Nitpick_Examples.gz
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: 33192 diff changeset	708
34126 8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: 34069 diff changeset	709	$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \
8a2c5d7aff51 polished Nitpick's binary integer support etc.; blanchet parents: 34069 diff changeset	710	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	711	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	712	Nitpick_Examples/Integer_Nits.thy Nitpick_Examples/Manual_Nits.thy \
39221 70fd4a3c41ed remove "minipick" (the toy version of Nitpick) and some tests; blanchet parents: 39048 diff changeset	713	Nitpick_Examples/Mono_Nits.thy Nitpick_Examples/Nitpick_Examples.thy \
70fd4a3c41ed remove "minipick" (the toy version of Nitpick) and some tests; blanchet parents: 39048 diff changeset	714	Nitpick_Examples/Pattern_Nits.thy Nitpick_Examples/Record_Nits.thy \
70fd4a3c41ed remove "minipick" (the toy version of Nitpick) and some tests; blanchet parents: 39048 diff changeset	715	Nitpick_Examples/Refute_Nits.thy Nitpick_Examples/Special_Nits.thy \
70fd4a3c41ed remove "minipick" (the toy version of Nitpick) and some tests; blanchet parents: 39048 diff changeset	716	Nitpick_Examples/Tests_Nits.thy Nitpick_Examples/Typedef_Nits.thy
33197 de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: 33192 diff changeset	717	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: 33192 diff changeset	718
de6285ebcc05 continuation of Nitpick's integration into Isabelle; blanchet parents: 33192 diff changeset	719
7999 7acf6eb8eec1 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: 7985 diff changeset	720	## HOL-Algebra
7acf6eb8eec1 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: 7985 diff changeset	721
33439 f5d95787224f more accurate dependencies; wenzelm parents: 33437 diff changeset	722	HOL-Algebra: HOL $(OUT)/HOL-Algebra
7999 7acf6eb8eec1 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: 7985 diff changeset	723
31771 1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	724	ALGEBRA_DEPENDENCIES = $(OUT)/HOL \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	725	Algebra/ROOT.ML \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	726	Library/Binomial.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	727	Library/FuncSet.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	728	Library/Multiset.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	729	Library/Permutation.thy \
32479 521cc9bf2958 some reorganization of number theory haftmann parents: 32402 diff changeset	730	Number_Theory/Primes.thy \
31771 1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	731	Algebra/AbelCoset.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	732	Algebra/Bij.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	733	Algebra/Congruence.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	734	Algebra/Coset.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	735	Algebra/Divisibility.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	736	Algebra/Exponent.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	737	Algebra/FiniteProduct.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	738	Algebra/Group.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	739	Algebra/Ideal.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	740	Algebra/IntRing.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	741	Algebra/Lattice.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	742	Algebra/Module.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	743	Algebra/QuotRing.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	744	Algebra/Ring.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	745	Algebra/RingHom.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	746	Algebra/Sylow.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	747	Algebra/UnivPoly.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	748	Algebra/abstract/Abstract.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	749	Algebra/abstract/Factor.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	750	Algebra/abstract/Field.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	751	Algebra/abstract/Ideal2.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	752	Algebra/abstract/PID.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	753	Algebra/abstract/Ring2.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	754	Algebra/abstract/RingHomo.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	755	Algebra/document/root.tex \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	756	Algebra/document/root.tex \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	757	Algebra/poly/LongDiv.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	758	Algebra/poly/PolyHomo.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	759	Algebra/poly/Polynomial.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	760	Algebra/poly/UnivPoly2.thy \
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	761	Algebra/ringsimp.ML
1a92eb45060f NewNumberTheory depends on Algebra haftmann parents: 31761 diff changeset	762
33448 7f716a975ada more accurate dependencies; wenzelm parents: 33439 diff changeset	763	$(OUT)/HOL-Algebra: $(ALGEBRA_DEPENDENCIES)
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	764	@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	765
27477 c64736fe2a1f more precise dependencies for HOL-Word and HOL-NSA; wenzelm parents: 27470 diff changeset	766
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	767	## HOL-Auth
3819 5a6a6f18b109 added TLA stuff; wenzelm parents: 3616 diff changeset	768
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	769	HOL-Auth: HOL $(LOG)/HOL-Auth.gz
3819 5a6a6f18b109 added TLA stuff; wenzelm parents: 3616 diff changeset	770
28098 c92850d2d16c Replaced Library/NatPair by Nat_Int_Bij. nipkow parents: 28054 diff changeset	771	$(LOG)/HOL-Auth.gz: $(OUT)/HOL \
37021 87c696bfe839 adjusted haftmann parents: 36962 diff changeset	772	Auth/Auth_Shared.thy Auth/Auth_Public.thy Auth/All_Symmetric.thy \
87c696bfe839 adjusted haftmann parents: 36962 diff changeset	773	Auth/Guard/Auth_Guard_Shared.thy \
87c696bfe839 adjusted haftmann parents: 36962 diff changeset	774	Auth/Guard/Auth_Guard_Public.thy \
32632 8ae912371831 added session entry point theories haftmann parents: 32624 diff changeset	775	Auth/Smartcard/Auth_Smartcard.thy Auth/All_Symmetric.thy \
27164 81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	776	Auth/CertifiedEmail.thy Auth/Event.thy Auth/Message.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	777	Auth/NS_Public.thy Auth/NS_Public_Bad.thy Auth/NS_Shared.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	778	Auth/OtwayRees.thy Auth/OtwayReesBella.thy Auth/OtwayRees_AN.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	779	Auth/OtwayRees_Bad.thy Auth/Public.thy Auth/ROOT.ML Auth/Recur.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	780	Auth/Shared.thy Auth/TLS.thy Auth/WooLam.thy Auth/Kerberos_BAN.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	781	Auth/Kerberos_BAN_Gets.thy Auth/KerberosIV.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	782	Auth/KerberosIV_Gets.thy Auth/KerberosV.thy Auth/Yahalom.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	783	Auth/Yahalom2.thy Auth/Yahalom_Bad.thy Auth/ZhouGollmann.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	784	Auth/Guard/Analz.thy Auth/Guard/Extensions.thy Auth/Guard/GuardK.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	785	Auth/Guard/Guard_Public.thy Auth/Guard/Guard_Shared.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	786	Auth/Guard/Guard.thy Auth/Guard/List_Msg.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	787	Auth/Guard/Guard_NS_Public.thy Auth/Guard/Guard_OtwayRees.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	788	Auth/Guard/P1.thy Auth/Guard/P2.thy Auth/Guard/Proto.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	789	Auth/Guard/Guard_Yahalom.thy Auth/Smartcard/EventSC.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	790	Auth/Smartcard/ShoupRubinBella.thy Auth/Smartcard/ShoupRubin.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	791	Auth/Smartcard/Smartcard.thy Auth/document/root.tex
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	792	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Auth
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	793
61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	794
4777 379f32b0ae40 New target HOL-UNITY paulson parents: 4729 diff changeset	795	## HOL-UNITY
379f32b0ae40 New target HOL-UNITY paulson parents: 4729 diff changeset	796
379f32b0ae40 New target HOL-UNITY paulson parents: 4729 diff changeset	797	HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz
379f32b0ae40 New target HOL-UNITY paulson parents: 4729 diff changeset	798
27164 81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	799	$(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	800	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	801	UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy \
27164 81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	802	UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy UNITY/Guar.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	803	UNITY/Lift_prog.thy UNITY/ListOrder.thy UNITY/ProgressSets.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	804	UNITY/PPROD.thy UNITY/Project.thy UNITY/Rename.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	805	UNITY/Transformers.thy UNITY/SubstAx.thy UNITY/UNITY.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	806	UNITY/Union.thy UNITY/WFair.thy UNITY/Simple/Channel.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	807	UNITY/Simple/Common.thy UNITY/Simple/Deadlock.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	808	UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	809	UNITY/Simple/NSP_Bad.thy UNITY/Simple/Network.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	810	UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	811	UNITY/Simple/Token.thy UNITY/Comp/Alloc.thy UNITY/Comp/AllocBase.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	812	UNITY/Comp/AllocImpl.thy UNITY/Comp/Client.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	813	UNITY/Comp/Counter.thy UNITY/Comp/Counterc.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	814	UNITY/Comp/Handshake.thy UNITY/Comp/PriorityAux.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	815	UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	816	UNITY/Comp/TimerArray.thy UNITY/document/root.tex
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	817	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL UNITY
4777 379f32b0ae40 New target HOL-UNITY paulson parents: 4729 diff changeset	818
379f32b0ae40 New target HOL-UNITY paulson parents: 4729 diff changeset	819
10966 8f2c27041a8e added HOL-Unix example; wenzelm parents: 10945 diff changeset	820	## HOL-Unix
8f2c27041a8e added HOL-Unix example; wenzelm parents: 10945 diff changeset	821
8f2c27041a8e added HOL-Unix example; wenzelm parents: 10945 diff changeset	822	HOL-Unix: HOL $(LOG)/HOL-Unix.gz
8f2c27041a8e added HOL-Unix example; wenzelm parents: 10945 diff changeset	823
37742 d8e7f473c3a1 tuned tabs haftmann parents: 37691 diff changeset	824	$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy \
d8e7f473c3a1 tuned tabs haftmann parents: 37691 diff changeset	825	Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy \
10966 8f2c27041a8e added HOL-Unix example; wenzelm parents: 10945 diff changeset	826	Unix/document/root.bib Unix/document/root.tex
39156 b4f18ac786fa modernized session ROOT setup; wenzelm parents: 39048 diff changeset	827	@$(ISABELLE_TOOL) usedir -m no_brackets -m no_type_brackets $(OUT)/HOL Unix
10966 8f2c27041a8e added HOL-Unix example; wenzelm parents: 10945 diff changeset	828
27477 c64736fe2a1f more precise dependencies for HOL-Word and HOL-NSA; wenzelm parents: 27470 diff changeset	829
19203 778507520684 Added HOL-ZF to Isabelle. obua parents: 19192 diff changeset	830	## HOL-ZF
778507520684 Added HOL-ZF to Isabelle. obua parents: 19192 diff changeset	831
778507520684 Added HOL-ZF to Isabelle. obua parents: 19192 diff changeset	832	HOL-ZF: HOL $(LOG)/HOL-ZF.gz
778507520684 Added HOL-ZF to Isabelle. obua parents: 19192 diff changeset	833
39306 c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies haftmann parents: 39271 diff changeset	834	$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/LProd.thy \
27164 81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	835	ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	836	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF
10966 8f2c27041a8e added HOL-Unix example; wenzelm parents: 10945 diff changeset	837
27477 c64736fe2a1f more precise dependencies for HOL-Word and HOL-NSA; wenzelm parents: 27470 diff changeset	838
29399 ebcd69a00872 split of Imperative_HOL theories from HOL-Library haftmann parents: 29197 diff changeset	839	## HOL-Imperative_HOL
ebcd69a00872 split of Imperative_HOL theories from HOL-Library haftmann parents: 29197 diff changeset	840
ebcd69a00872 split of Imperative_HOL theories from HOL-Library haftmann parents: 29197 diff changeset	841	HOL-Imperative_HOL: HOL $(LOG)/HOL-Imperative_HOL.gz
ebcd69a00872 split of Imperative_HOL theories from HOL-Library haftmann parents: 29197 diff changeset	842
39306 c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies haftmann parents: 39271 diff changeset	843	$(LOG)/HOL-Imperative_HOL.gz: $(OUT)/HOL \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies haftmann parents: 39271 diff changeset	844	Imperative_HOL/Array.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies haftmann parents: 39271 diff changeset	845	Imperative_HOL/Heap.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies haftmann parents: 39271 diff changeset	846	Imperative_HOL/Heap_Monad.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies haftmann parents: 39271 diff changeset	847	Imperative_HOL/Imperative_HOL.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies haftmann parents: 39271 diff changeset	848	Imperative_HOL/Imperative_HOL_ex.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies haftmann parents: 39271 diff changeset	849	Imperative_HOL/Mrec.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies haftmann parents: 39271 diff changeset	850	Imperative_HOL/Ref.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies haftmann parents: 39271 diff changeset	851	Imperative_HOL/ROOT.ML \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies haftmann parents: 39271 diff changeset	852	Imperative_HOL/ex/Imperative_Quicksort.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies haftmann parents: 39271 diff changeset	853	Imperative_HOL/ex/Imperative_Reverse.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies haftmann parents: 39271 diff changeset	854	Imperative_HOL/ex/Linked_Lists.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies haftmann parents: 39271 diff changeset	855	Imperative_HOL/ex/SatChecker.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies haftmann parents: 39271 diff changeset	856	Imperative_HOL/ex/Sorted_List.thy \
c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies haftmann parents: 39271 diff changeset	857	Imperative_HOL/ex/Subarray.thy \
30689 b14b2cc4e25e moved Imperative_HOL examples to Imperative_HOL/ex haftmann parents: 30654 diff changeset	858	Imperative_HOL/ex/Sublist.thy
39306 c1f3992c9097 print mode for Imperative HOL overview; tuned and more accurate dependencies haftmann parents: 39271 diff changeset	859	@$(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	860
ebcd69a00872 split of Imperative_HOL theories from HOL-Library haftmann parents: 29197 diff changeset	861
29823 0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there haftmann parents: 29813 diff changeset	862	## HOL-Decision_Procs
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there haftmann parents: 29813 diff changeset	863
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there haftmann parents: 29813 diff changeset	864	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	865
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there haftmann parents: 29813 diff changeset	866	$(LOG)/HOL-Decision_Procs.gz: $(OUT)/HOL \
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there haftmann parents: 29813 diff changeset	867	Decision_Procs/Approximation.thy \
33356 9157d0f9f00e moved Commutative_Ring into session Decision_Procs haftmann parents: 33348 diff changeset	868	Decision_Procs/Commutative_Ring.thy \
9157d0f9f00e moved Commutative_Ring into session Decision_Procs haftmann parents: 33348 diff changeset	869	Decision_Procs/Commutative_Ring_Complete.thy \
29823 0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there haftmann parents: 29813 diff changeset	870	Decision_Procs/Cooper.thy \
35053 43175817d83b more precise dependencies; wenzelm parents: 35050 diff changeset	871	Decision_Procs/Decision_Procs.thy \
29823 0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there haftmann parents: 29813 diff changeset	872	Decision_Procs/Dense_Linear_Order.thy \
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there haftmann parents: 29813 diff changeset	873	Decision_Procs/Ferrack.thy \
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there haftmann parents: 29813 diff changeset	874	Decision_Procs/MIR.thy \
35053 43175817d83b more precise dependencies; wenzelm parents: 35050 diff changeset	875	Decision_Procs/Parametric_Ferrante_Rackoff.thy \
43175817d83b more precise dependencies; wenzelm parents: 35050 diff changeset	876	Decision_Procs/Polynomial_List.thy \
37120 5df087c6ce94 moved ML files where they are actually used; wenzelm parents: 37118 diff changeset	877	Decision_Procs/ROOT.ML \
35053 43175817d83b more precise dependencies; wenzelm parents: 35050 diff changeset	878	Decision_Procs/Reflected_Multivariate_Polynomial.thy \
43175817d83b more precise dependencies; wenzelm parents: 35050 diff changeset	879	Decision_Procs/commutative_ring_tac.ML \
43175817d83b more precise dependencies; wenzelm parents: 35050 diff changeset	880	Decision_Procs/cooper_tac.ML \
30429 39acdf031548 moved Decision_Procs examples to Decision_Procs/ex haftmann parents: 30400 diff changeset	881	Decision_Procs/ex/Approximation_Ex.thy \
33356 9157d0f9f00e moved Commutative_Ring into session Decision_Procs haftmann parents: 33348 diff changeset	882	Decision_Procs/ex/Commutative_Ring_Ex.thy \
35053 43175817d83b more precise dependencies; wenzelm parents: 35050 diff changeset	883	Decision_Procs/ex/Dense_Linear_Order_Ex.thy \
43175817d83b more precise dependencies; wenzelm parents: 35050 diff changeset	884	Decision_Procs/ferrack_tac.ML \
37120 5df087c6ce94 moved ML files where they are actually used; wenzelm parents: 37118 diff changeset	885	Decision_Procs/ferrante_rackoff.ML \
5df087c6ce94 moved ML files where they are actually used; wenzelm parents: 37118 diff changeset	886	Decision_Procs/ferrante_rackoff_data.ML \
5df087c6ce94 moved ML files where they are actually used; wenzelm parents: 37118 diff changeset	887	Decision_Procs/langford.ML \
5df087c6ce94 moved ML files where they are actually used; wenzelm parents: 37118 diff changeset	888	Decision_Procs/langford_data.ML \
5df087c6ce94 moved ML files where they are actually used; wenzelm parents: 37118 diff changeset	889	Decision_Procs/mir_tac.ML
29823 0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there haftmann parents: 29813 diff changeset	890	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Decision_Procs
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there haftmann parents: 29813 diff changeset	891
0ab754d13ccd session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there haftmann parents: 29813 diff changeset	892
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	893	## 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	894
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical); wenzelm parents: 39156 diff changeset	895	HOL-Proofs: 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	896
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical); wenzelm parents: 39156 diff changeset	897	$(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	898	@$(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	899
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical); wenzelm parents: 39156 diff changeset	900
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical); wenzelm parents: 39156 diff changeset	901	## 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	902
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical); wenzelm parents: 39156 diff changeset	903	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	904
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical); wenzelm parents: 39156 diff changeset	905	$(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	906	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	907	@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	908
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical); wenzelm parents: 39156 diff changeset	909
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical); wenzelm parents: 39156 diff changeset	910	## 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	911
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical); wenzelm parents: 39156 diff changeset	912	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	913
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical); wenzelm parents: 39156 diff changeset	914	$(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	915	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	916	Proofs/Extraction/Greatest_Common_Divisor.thy \
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical); wenzelm parents: 39156 diff changeset	917	Proofs/Extraction/Higman.thy Proofs/Extraction/Pigeonhole.thy \
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical); wenzelm parents: 39156 diff changeset	918	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	919	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	920	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	921	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	922	@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	923
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	924
34205 f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.; wenzelm parents: 34126 diff changeset	925	## HOL-Proofs-Lambda
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	926
34205 f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.; wenzelm parents: 34126 diff changeset	927	HOL-Proofs-Lambda: HOL-Proofs $(LOG)/HOL-Proofs-Lambda.gz
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	928
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	929	$(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	930	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	931	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	932	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	933	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	934	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	935	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	936	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	937	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	938	@cd Proofs; $(ISABELLE_TOOL) usedir -g true -m no_brackets -p 2 -q 0 $(OUT)/HOL-Proofs Lambda
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	939
61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	940
9015 8006e9009621 added HOL/Prolog oheimb parents: 8958 diff changeset	941	## HOL-Prolog
8006e9009621 added HOL/Prolog oheimb parents: 8958 diff changeset	942
8006e9009621 added HOL/Prolog oheimb parents: 8958 diff changeset	943	HOL-Prolog: HOL $(LOG)/HOL-Prolog.gz
8006e9009621 added HOL/Prolog oheimb parents: 8958 diff changeset	944
27164 81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	945	$(LOG)/HOL-Prolog.gz: $(OUT)/HOL Prolog/ROOT.ML Prolog/prolog.ML \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	946	Prolog/HOHH.thy Prolog/Test.thy Prolog/Func.thy Prolog/Type.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	947	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Prolog
9015 8006e9009621 added HOL/Prolog oheimb parents: 8958 diff changeset	948
8006e9009621 added HOL/Prolog oheimb parents: 8958 diff changeset	949
8012 bbdf3c51c3b8 Added MicroJava nipkow parents: 8008 diff changeset	950	## HOL-MicroJava
bbdf3c51c3b8 Added MicroJava nipkow parents: 8008 diff changeset	951
bbdf3c51c3b8 Added MicroJava nipkow parents: 8008 diff changeset	952	HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
bbdf3c51c3b8 Added MicroJava nipkow parents: 8008 diff changeset	953
27164 81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	954	$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL Library/Executable_Set.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	955	MicroJava/ROOT.ML MicroJava/Comp/AuxLemmas.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	956	MicroJava/Comp/CorrComp.thy MicroJava/Comp/CorrCompTp.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	957	MicroJava/Comp/DefsComp.thy MicroJava/Comp/Index.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	958	MicroJava/Comp/LemmasComp.thy MicroJava/Comp/NatCanonify.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	959	MicroJava/Comp/TranslComp.thy MicroJava/Comp/TranslCompTp.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	960	MicroJava/Comp/TypeInf.thy MicroJava/J/Conform.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	961	MicroJava/J/Eval.thy MicroJava/J/JBasis.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	962	MicroJava/J/JTypeSafe.thy MicroJava/J/Decl.thy MicroJava/J/State.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	963	MicroJava/J/Term.thy MicroJava/J/Type.thy MicroJava/J/TypeRel.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	964	MicroJava/J/WellForm.thy MicroJava/J/Value.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	965	MicroJava/J/WellType.thy MicroJava/J/Example.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	966	MicroJava/J/JListExample.thy MicroJava/JVM/JVMExec.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	967	MicroJava/JVM/JVMInstructions.thy MicroJava/JVM/JVMState.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	968	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	969	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	970	MicroJava/DFA/Err.thy MicroJava/DFA/Kildall.thy \
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: 33820 diff changeset	971	MicroJava/DFA/LBVComplete.thy MicroJava/DFA/LBVCorrect.thy \
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: 33820 diff changeset	972	MicroJava/DFA/LBVSpec.thy MicroJava/DFA/Listn.thy \
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: 33820 diff changeset	973	MicroJava/DFA/Opt.thy MicroJava/DFA/Product.thy \
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: 33820 diff changeset	974	MicroJava/DFA/SemilatAlg.thy MicroJava/DFA/Semilat.thy \
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: 33820 diff changeset	975	MicroJava/DFA/Semilattices.thy MicroJava/DFA/Typing_Framework_err.thy \
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: 33820 diff changeset	976	MicroJava/DFA/Typing_Framework.thy MicroJava/BV/BVSpec.thy \
27164 81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	977	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	978	MicroJava/BV/JType.thy MicroJava/BV/JVM.thy MicroJava/BV/JVMType.thy \
27164 81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	979	MicroJava/BV/Effect.thy MicroJava/BV/EffectMono.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	980	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	981	MicroJava/BV/LBVJVM.thy MicroJava/document/root.bib \
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: 33820 diff changeset	982	MicroJava/document/root.tex MicroJava/document/introduction.tex
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	983	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL MicroJava
11850 cdfc3fce577e document graphs for several sessions; wenzelm parents: 11837 diff changeset	984
8012 bbdf3c51c3b8 Added MicroJava nipkow parents: 8008 diff changeset	985
11376 bf98ad1c22c6 added NanoJava oheimb parents: 11370 diff changeset	986	## HOL-NanoJava
bf98ad1c22c6 added NanoJava oheimb parents: 11370 diff changeset	987
bf98ad1c22c6 added NanoJava oheimb parents: 11370 diff changeset	988	HOL-NanoJava: HOL $(LOG)/HOL-NanoJava.gz
bf98ad1c22c6 added NanoJava oheimb parents: 11370 diff changeset	989
27164 81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	990	$(LOG)/HOL-NanoJava.gz: $(OUT)/HOL NanoJava/ROOT.ML NanoJava/Term.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	991	NanoJava/Decl.thy NanoJava/TypeRel.thy NanoJava/State.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	992	NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy \
11376 bf98ad1c22c6 added NanoJava oheimb parents: 11370 diff changeset	993	NanoJava/document/root.bib NanoJava/document/root.tex
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	994	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NanoJava
11850 cdfc3fce577e document graphs for several sessions; wenzelm parents: 11837 diff changeset	995
8193 33e4ec7a2daa added MicroJava/document; wenzelm parents: 8179 diff changeset	996
12855 21225338f8db Bali added schirmer parents: 12816 diff changeset	997	## HOL-Bali
21225338f8db Bali added schirmer parents: 12816 diff changeset	998
21225338f8db Bali added schirmer parents: 12816 diff changeset	999	HOL-Bali: HOL $(LOG)/HOL-Bali.gz
21225338f8db Bali added schirmer parents: 12816 diff changeset	1000
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	1001	$(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	1002	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	1003	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	1004	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	1005	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	1006	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	1007	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	1008	Bali/WellType.thy Bali/document/root.tex
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	1009	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Bali
12855 21225338f8db Bali added schirmer parents: 12816 diff changeset	1010
21225338f8db Bali added schirmer parents: 12816 diff changeset	1011
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1012	## HOL-IOA
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1013
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1014	HOL-IOA: HOL $(LOG)/HOL-IOA.gz
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	1015
27164 81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	1016	$(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.thy IOA/IOA.thy IOA/ROOT.ML \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	1017	IOA/Solve.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	1018	@$(ISABELLE_TOOL) usedir $(OUT)/HOL IOA
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1019
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1020
10157 6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	1021	## HOL-Lattice
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	1022
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	1023	HOL-Lattice: HOL $(LOG)/HOL-Lattice.gz
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	1024
27164 81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	1025	$(LOG)/HOL-Lattice.gz: $(OUT)/HOL Lattice/Bounds.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	1026	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	1027	Lattice/ROOT.ML Lattice/document/root.tex
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	1028	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Lattice
10157 6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	1029
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	1030
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1031	## HOL-ex
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	1032
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1033	HOL-ex: HOL $(LOG)/HOL-ex.gz
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	1034
33439 f5d95787224f more accurate dependencies; wenzelm parents: 33437 diff changeset	1035	$(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	1036	Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \
b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical); wenzelm parents: 39156 diff changeset	1037	ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy ex/BT.thy \
42601 cddab94eeb14 renamed theory to make its purpose clearer blanchet parents: 42343 diff changeset	1038	ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradoxon.thy \
cddab94eeb14 renamed theory to make its purpose clearer blanchet parents: 42343 diff changeset	1039	ex/CASC_Setup.thy ex/CTL.thy ex/Case_Product.thy \
40837 dedb893dc692 more precise dependencies; wenzelm parents: 40777 diff changeset	1040	ex/Chinese.thy ex/Classical.thy ex/CodegenSML_Test.thy \
dedb893dc692 more precise dependencies; wenzelm parents: 40777 diff changeset	1041	ex/Coercion_Examples.thy ex/Coherent.thy ex/Dedekind_Real.thy \
dedb893dc692 more precise dependencies; wenzelm parents: 40777 diff changeset	1042	ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy \
dedb893dc692 more precise dependencies; wenzelm parents: 40777 diff changeset	1043	ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy \
dedb893dc692 more precise dependencies; wenzelm parents: 40777 diff changeset	1044	ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy \
dedb893dc692 more precise dependencies; wenzelm parents: 40777 diff changeset	1045	ex/Higher_Order_Logic.thy ex/Iff_Oracle.thy ex/Induction_Schema.thy \
dedb893dc692 more precise dependencies; wenzelm parents: 40777 diff changeset	1046	ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \
41582 c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example haftmann parents: 41569 diff changeset	1047	ex/Interpretation_with_Defs.thy ex/Intuitionistic.thy ex/Lagrange.thy \
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example haftmann parents: 41569 diff changeset	1048	ex/List_to_Set_Comprehension_Examples.thy ex/LocaleTest2.thy \
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example haftmann parents: 41569 diff changeset	1049	ex/MT.thy ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \
40837 dedb893dc692 more precise dependencies; wenzelm parents: 40777 diff changeset	1050	ex/Multiquote.thy ex/NatSum.thy ex/Normalization_by_Evaluation.thy \
dedb893dc692 more precise dependencies; wenzelm parents: 40777 diff changeset	1051	ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
dedb893dc692 more precise dependencies; wenzelm parents: 40777 diff changeset	1052	ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \
42161 d1b39536e1fb adding a regression test for SML_Quickcheck; putting SML_Quickcheck back in shape bulwahn parents: 42153 diff changeset	1053	ex/Quickcheck_Narrowing_Examples.thy ex/SML_Quickcheck_Examples.thy \
40837 dedb893dc692 more precise dependencies; wenzelm parents: 40777 diff changeset	1054	ex/Quicksort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
dedb893dc692 more precise dependencies; wenzelm parents: 40777 diff changeset	1055	ex/ReflectionEx.thy ex/Refute_Examples.thy ex/SAT_Examples.thy \
42071 04577a7e0c51 move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex" blanchet parents: 42064 diff changeset	1056	ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy \
04577a7e0c51 move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex" blanchet parents: 42064 diff changeset	1057	ex/sledgehammer_tactics.ML ex/Sqrt.thy \
41582 c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example haftmann parents: 41569 diff changeset	1058	ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy \
42602 a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning blanchet parents: 42601 diff changeset	1059	ex/TPTP_Export.thy ex/Transfer_Ex.thy ex/Tree23.thy \
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning blanchet parents: 42601 diff changeset	1060	ex/Unification.thy ex/While_Combinator_Example.thy \
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning blanchet parents: 42601 diff changeset	1061	ex/document/root.bib ex/document/root.tex ex/set.thy ex/svc_funcs.ML \
a2db47fa015e added TPTP exporter facility -- useful to do experiments with machine learning blanchet parents: 42601 diff changeset	1062	ex/svc_test.thy \
41582 c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example haftmann parents: 41569 diff changeset	1063	../Tools/interpretation_with_defs.ML
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	1064	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	1065
61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	1066
33026 8f35633c4922 modernized session Isar_Examples; wenzelm parents: 33024 diff changeset	1067	## HOL-Isar_Examples
6445 931fc1daa8b1 added Isar_examples; wenzelm parents: 6440 diff changeset	1068
33026 8f35633c4922 modernized session Isar_Examples; wenzelm parents: 33024 diff changeset	1069	HOL-Isar_Examples: HOL $(LOG)/HOL-Isar_Examples.gz
6445 931fc1daa8b1 added Isar_examples; wenzelm parents: 6440 diff changeset	1070
33026 8f35633c4922 modernized session Isar_Examples; wenzelm parents: 33024 diff changeset	1071	$(LOG)/HOL-Isar_Examples.gz: $(OUT)/HOL Isar_Examples/Basic_Logic.thy \
8f35633c4922 modernized session Isar_Examples; wenzelm parents: 33024 diff changeset	1072	Isar_Examples/Cantor.thy Isar_Examples/Drinker.thy \
8f35633c4922 modernized session Isar_Examples; wenzelm parents: 33024 diff changeset	1073	Isar_Examples/Expr_Compiler.thy Isar_Examples/Fibonacci.thy \
8f35633c4922 modernized session Isar_Examples; wenzelm parents: 33024 diff changeset	1074	Isar_Examples/Group.thy Isar_Examples/Hoare.thy \
8f35633c4922 modernized session Isar_Examples; wenzelm parents: 33024 diff changeset	1075	Isar_Examples/Hoare_Ex.thy Isar_Examples/Knaster_Tarski.thy \
8f35633c4922 modernized session Isar_Examples; wenzelm parents: 33024 diff changeset	1076	Isar_Examples/Mutilated_Checkerboard.thy \
8f35633c4922 modernized session Isar_Examples; wenzelm parents: 33024 diff changeset	1077	Isar_Examples/Nested_Datatype.thy Isar_Examples/Peirce.thy \
8f35633c4922 modernized session Isar_Examples; wenzelm parents: 33024 diff changeset	1078	Isar_Examples/Puzzle.thy Isar_Examples/Summation.thy \
8f35633c4922 modernized session Isar_Examples; wenzelm parents: 33024 diff changeset	1079	Isar_Examples/ROOT.ML Isar_Examples/document/proof.sty \
8f35633c4922 modernized session Isar_Examples; wenzelm parents: 33024 diff changeset	1080	Isar_Examples/document/root.bib Isar_Examples/document/root.tex \
37672 645eb9fec794 avoid Old_Number_Theory; wenzelm parents: 37665 diff changeset	1081	Isar_Examples/document/style.tex Hoare/hoare_tac.ML \
645eb9fec794 avoid Old_Number_Theory; wenzelm parents: 37665 diff changeset	1082	Number_Theory/Primes.thy
33026 8f35633c4922 modernized session Isar_Examples; wenzelm parents: 33024 diff changeset	1083	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Isar_Examples
6445 931fc1daa8b1 added Isar_examples; wenzelm parents: 6440 diff changeset	1084
931fc1daa8b1 added Isar_examples; wenzelm parents: 6440 diff changeset	1085
33028 9aa8bfb1649d modernized session SET_Protocol; wenzelm parents: 33027 diff changeset	1086	## HOL-SET_Protocol
14199 d3b8d972a488 new session HOL-SET-Protocol paulson parents: 14182 diff changeset	1087
33028 9aa8bfb1649d modernized session SET_Protocol; wenzelm parents: 33027 diff changeset	1088	HOL-SET_Protocol: HOL $(LOG)/HOL-SET_Protocol.gz
14199 d3b8d972a488 new session HOL-SET-Protocol paulson parents: 14182 diff changeset	1089
33028 9aa8bfb1649d modernized session SET_Protocol; wenzelm parents: 33027 diff changeset	1090	$(LOG)/HOL-SET_Protocol.gz: $(OUT)/HOL SET_Protocol/ROOT.ML \
9aa8bfb1649d modernized session SET_Protocol; wenzelm parents: 33027 diff changeset	1091	SET_Protocol/Message_SET.thy SET_Protocol/Event_SET.thy \
9aa8bfb1649d modernized session SET_Protocol; wenzelm parents: 33027 diff changeset	1092	SET_Protocol/Public_SET.thy SET_Protocol/Cardholder_Registration.thy \
9aa8bfb1649d modernized session SET_Protocol; wenzelm parents: 33027 diff changeset	1093	SET_Protocol/Merchant_Registration.thy SET_Protocol/Purchase.thy \
39757 21423597a80d modernized session haftmann parents: 39720 diff changeset	1094	SET_Protocol/SET_Protocol.thy SET_Protocol/document/root.tex
33028 9aa8bfb1649d modernized session SET_Protocol; wenzelm parents: 33027 diff changeset	1095	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL SET_Protocol
14199 d3b8d972a488 new session HOL-SET-Protocol paulson parents: 14182 diff changeset	1096
d3b8d972a488 new session HOL-SET-Protocol paulson parents: 14182 diff changeset	1097
27421 7e458bd56860 HOL += HOL-Complex haftmann parents: 27396 diff changeset	1098	## HOL-Matrix
14610 9c2e31e483b2 added HOL-Matrix, added HOL/Matrix/ROOT.ML kleing parents: 14603 diff changeset	1099
28637 7aabaf1ba263 reactivated HOL-Matrix; wenzelm parents: 28612 diff changeset	1100	HOL-Matrix: HOL $(LOG)/HOL-Matrix.gz
17323 2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight obua parents: 17308 diff changeset	1101
37872 d83659570337 moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway; wenzelm parents: 37818 diff changeset	1102	$(LOG)/HOL-Matrix.gz: $(OUT)/HOL Matrix/ComputeFloat.thy \
d83659570337 moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway; wenzelm parents: 37818 diff changeset	1103	Matrix/ComputeHOL.thy Matrix/ComputeNumeral.thy \
d83659570337 moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway; wenzelm parents: 37818 diff changeset	1104	Matrix/Compute_Oracle/Compute_Oracle.thy Matrix/Compute_Oracle/am.ML \
d83659570337 moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway; wenzelm parents: 37818 diff changeset	1105	Matrix/Compute_Oracle/am_compiler.ML Matrix/Compute_Oracle/am_ghc.ML \
d83659570337 moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway; wenzelm parents: 37818 diff changeset	1106	Matrix/Compute_Oracle/am_interpreter.ML \
d83659570337 moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway; wenzelm parents: 37818 diff changeset	1107	Matrix/Compute_Oracle/am_sml.ML Matrix/Compute_Oracle/compute.ML \
d83659570337 moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway; wenzelm parents: 37818 diff changeset	1108	Matrix/Compute_Oracle/linker.ML Matrix/Cplex.thy \
37764 3489daf839d5 more regular session structure haftmann parents: 37747 diff changeset	1109	Matrix/CplexMatrixConverter.ML Matrix/Cplex_tools.ML \
37872 d83659570337 moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway; wenzelm parents: 37818 diff changeset	1110	Matrix/FloatSparseMatrixBuilder.ML Matrix/LP.thy Matrix/Matrix.thy \
d83659570337 moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway; wenzelm parents: 37818 diff changeset	1111	Matrix/ROOT.ML Matrix/SparseMatrix.thy Matrix/document/root.tex \
d83659570337 moved src/Tools/Compute_Oracle to src/HOL/Matrix/Compute_Oracle -- it actually depends on HOL anyway; wenzelm parents: 37818 diff changeset	1112	Matrix/fspmlp.ML Matrix/matrixlp.ML Tools/float_arith.ML
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	1113	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Matrix
16873 9ed940a1bebb proving bounds for real linear programs obua parents: 16784 diff changeset	1114
14199 d3b8d972a488 new session HOL-SET-Protocol paulson parents: 14182 diff changeset	1115
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1116	## TLA
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1117
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1118	TLA: HOL $(OUT)/TLA
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1119
27164 81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	1120	$(OUT)/TLA: $(OUT)/HOL TLA/Action.thy TLA/Init.thy TLA/Intensional.thy \
21624 6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 21542 diff changeset	1121	TLA/ROOT.ML TLA/Stfun.thy TLA/TLA.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	1122	@cd TLA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL TLA
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1123
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1124
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1125	## TLA-Inc
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1126
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1127	TLA-Inc: TLA $(LOG)/TLA-Inc.gz
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1128
21624 6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 21542 diff changeset	1129	$(LOG)/TLA-Inc.gz: $(OUT)/TLA TLA/Inc/Inc.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	1130	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Inc
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1131
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1132
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1133	## TLA-Buffer
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1134
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1135	TLA-Buffer: TLA $(LOG)/TLA-Buffer.gz
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	1136
33024 60a098883d81 more accurate dependencies for HOL-SMT, which is a session with image; wenzelm parents: 33010 diff changeset	1137	$(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	1138	TLA/Buffer/DBuffer.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	1139	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Buffer
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1140
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1141
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1142	## TLA-Memory
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1143
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1144	TLA-Memory: TLA $(LOG)/TLA-Memory.gz
4447 b7ee449eb345 log files; wenzelm parents: 4289 diff changeset	1145
27164 81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	1146	$(LOG)/TLA-Memory.gz: $(OUT)/TLA TLA/Memory/MemClerk.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	1147	TLA/Memory/MemClerkParameters.thy TLA/Memory/Memory.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	1148	TLA/Memory/MemoryImplementation.thy TLA/Memory/MemoryParameters.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	1149	TLA/Memory/ProcedureInterface.thy TLA/Memory/RPC.thy \
21624 6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 21542 diff changeset	1150	TLA/Memory/RPCMemoryParams.thy TLA/Memory/RPCParameters.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	1151	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Memory
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1152
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1153
33175 2083bde13ce1 distinguished session for multivariate analysis himmelma parents: 33083 diff changeset	1154	## HOL-Multivariate_Analysis
2083bde13ce1 distinguished session for multivariate analysis himmelma parents: 33083 diff changeset	1155
36898 8e55aa1306c5 integrated SMT into the HOL image boehmes parents: 36895 diff changeset	1156	HOL-Multivariate_Analysis: HOL $(OUT)/HOL-Multivariate_Analysis
33175 2083bde13ce1 distinguished session for multivariate analysis himmelma parents: 33083 diff changeset	1157
36937 a30e50d4aeeb moved normarith.ML where it is actually used; wenzelm parents: 36936 diff changeset	1158	$(OUT)/HOL-Multivariate_Analysis: $(OUT)/HOL \
a30e50d4aeeb moved normarith.ML where it is actually used; wenzelm parents: 36936 diff changeset	1159	Multivariate_Analysis/Brouwer_Fixpoint.thy \
37522 0246a314b57d more accurate dependencies; wenzelm parents: 37509 diff changeset	1160	Multivariate_Analysis/Cartesian_Euclidean_Space.thy \
36937 a30e50d4aeeb moved normarith.ML where it is actually used; wenzelm parents: 36936 diff changeset	1161	Multivariate_Analysis/Convex_Euclidean_Space.thy \
a30e50d4aeeb moved normarith.ML where it is actually used; wenzelm parents: 36936 diff changeset	1162	Multivariate_Analysis/Derivative.thy \
a30e50d4aeeb moved normarith.ML where it is actually used; wenzelm parents: 36936 diff changeset	1163	Multivariate_Analysis/Determinants.thy \
a30e50d4aeeb moved normarith.ML where it is actually used; wenzelm parents: 36936 diff changeset	1164	Multivariate_Analysis/Euclidean_Space.thy \
41980 28b51effc5ed split Extended_Reals into parts for Library and Multivariate_Analysis hoelzl parents: 41973 diff changeset	1165	Multivariate_Analysis/Extended_Real_Limits.thy \
36937 a30e50d4aeeb moved normarith.ML where it is actually used; wenzelm parents: 36936 diff changeset	1166	Multivariate_Analysis/Fashoda.thy \
a30e50d4aeeb moved normarith.ML where it is actually used; wenzelm parents: 36936 diff changeset	1167	Multivariate_Analysis/Finite_Cartesian_Product.thy \
a30e50d4aeeb moved normarith.ML where it is actually used; wenzelm parents: 36936 diff changeset	1168	Multivariate_Analysis/Integration.certs \
a30e50d4aeeb moved normarith.ML where it is actually used; wenzelm parents: 36936 diff changeset	1169	Multivariate_Analysis/Integration.thy \
a30e50d4aeeb moved normarith.ML where it is actually used; wenzelm parents: 36936 diff changeset	1170	Multivariate_Analysis/L2_Norm.thy \
a30e50d4aeeb moved normarith.ML where it is actually used; wenzelm parents: 36936 diff changeset	1171	Multivariate_Analysis/Multivariate_Analysis.thy \
a30e50d4aeeb moved normarith.ML where it is actually used; wenzelm parents: 36936 diff changeset	1172	Multivariate_Analysis/Operator_Norm.thy \
a30e50d4aeeb moved normarith.ML where it is actually used; wenzelm parents: 36936 diff changeset	1173	Multivariate_Analysis/Path_Connected.thy \
a30e50d4aeeb moved normarith.ML where it is actually used; wenzelm parents: 36936 diff changeset	1174	Multivariate_Analysis/ROOT.ML \
a30e50d4aeeb moved normarith.ML where it is actually used; wenzelm parents: 36936 diff changeset	1175	Multivariate_Analysis/Real_Integration.thy \
a30e50d4aeeb moved normarith.ML where it is actually used; wenzelm parents: 36936 diff changeset	1176	Multivariate_Analysis/Topology_Euclidean_Space.thy \
a30e50d4aeeb moved normarith.ML where it is actually used; wenzelm parents: 36936 diff changeset	1177	Multivariate_Analysis/document/root.tex \
37742 d8e7f473c3a1 tuned tabs haftmann parents: 37691 diff changeset	1178	Multivariate_Analysis/normarith.ML Library/Glbs.thy \
41981 cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41980 diff changeset	1179	Library/Extended_Reals.thy Library/Indicator_Function.thy \
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41980 diff changeset	1180	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	1181	Library/FrechetDeriv.thy Library/Product_Vector.thy \
cdf7693bbe08 reworked Probability theory: measures are not type restricted to positive extended reals hoelzl parents: 41980 diff changeset	1182	Library/Product_plus.thy
36898 8e55aa1306c5 integrated SMT into the HOL image boehmes parents: 36895 diff changeset	1183	@cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Multivariate_Analysis
33175 2083bde13ce1 distinguished session for multivariate analysis himmelma parents: 33083 diff changeset	1184
33285 a0de1d5c7b3d tuned; wenzelm parents: 33272 diff changeset	1185
33271 7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: 33270 diff changeset	1186	## HOL-Probability
7be66dee1a5a New theory Probability, which contains a development of measure theory paulson parents: 33270 diff changeset	1187
38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 38622 diff changeset	1188	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	1189
40863 ab83ba2cd5d1 Corrected IsaMakefile hoelzl parents: 40862 diff changeset	1190	$(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	1191	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	1192	Probability/Caratheodory.thy Probability/Complete_Measure.thy \
40860 a6df324752da More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability. hoelzl parents: 40839 diff changeset	1193	Probability/ex/Dining_Cryptographers.thy \
a6df324752da More correct make dependencies for HOL-Multivariate_Analysis and HOL-Probability. hoelzl parents: 40839 diff changeset	1194	Probability/ex/Koepf_Duermuth_Countermeasure.thy \
42147 61d5d50ca74c add infinite product measure hoelzl parents: 42146 diff changeset	1195	Probability/Finite_Product_Measure.thy \
42861 16375b493b64 Add formalization of probabilistic independence for families of sets hoelzl parents: 42841 diff changeset	1196	Probability/Independent_Family.thy \
42147 61d5d50ca74c add infinite product measure hoelzl parents: 42146 diff changeset	1197	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	1198	Probability/Lebesgue_Integration.thy Probability/Lebesgue_Measure.thy \
42148 d596e7bb251f rename Probability_Space to Probability_Measure hoelzl parents: 42147 diff changeset	1199	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	1200	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	1201	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	1202	Library/Countable.thy Library/FuncSet.thy Library/Nat_Bijection.thy
38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 38622 diff changeset	1203	@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	1204
39157 b98909faaea8 more explicit HOL-Proofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical); wenzelm parents: 39156 diff changeset	1205
19497 630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	1206	## HOL-Nominal
630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	1207
630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	1208	HOL-Nominal: HOL $(OUT)/HOL-Nominal
630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	1209
22245 1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls urbanc parents: 22167 diff changeset	1210	$(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	1211	Nominal/Nominal.thy \
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls urbanc parents: 22167 diff changeset	1212	Nominal/nominal_atoms.ML \
31936 9466169dc8e0 nominal.ML is nominal_datatype.ML haftmann parents: 31849 diff changeset	1213	Nominal/nominal_datatype.ML \
22784 4637b69de71b Added datatype_case.ML and nominal_fresh_fun.ML. berghofe parents: 22657 diff changeset	1214	Nominal/nominal_fresh_fun.ML \
22247 5bad0d429694 corrected typo introduced by me urbanc parents: 22245 diff changeset	1215	Nominal/nominal_induct.ML \
22314 d541f13756a2 Added new file Nominal/nominal_inductive.ML berghofe parents: 22260 diff changeset	1216	Nominal/nominal_inductive.ML \
28652 659d64d59f16 Added nominal_inductive2.ML berghofe parents: 28637 diff changeset	1217	Nominal/nominal_inductive2.ML \
22245 1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls urbanc parents: 22167 diff changeset	1218	Nominal/nominal_permeq.ML \
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls urbanc parents: 22167 diff changeset	1219	Nominal/nominal_primrec.ML \
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls urbanc parents: 22167 diff changeset	1220	Nominal/nominal_thmdecls.ML \
21542 4462ee172ef0 Added nominal_primrec.ML berghofe parents: 21425 diff changeset	1221	Library/Infinite_Set.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	1222	@cd Nominal; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Nominal
19497 630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	1223
630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	1224
630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	1225	## HOL-Nominal-Examples
630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	1226
630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	1227	HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz
630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	1228
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	1229	$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal \
32636 55a0be42327c added session theory for Bali and Nominal_Examples haftmann parents: 32632 diff changeset	1230	Nominal/Examples/Nominal_Examples.thy \
27163 587ad1fba128 added CK_Machine to the nominal section urbanc parents: 27127 diff changeset	1231	Nominal/Examples/CK_Machine.thy \
22073 c170dcbe6c9d formalisation of Crary's chapter on logical relations urbanc parents: 22067 diff changeset	1232	Nominal/Examples/CR.thy \
22821 15b2e7ec1f3b alternative and much simpler proof for Church-Rosser of Beta-Reduction urbanc parents: 22819 diff changeset	1233	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	1234	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	1235	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	1236	Nominal/Examples/Class3.thy \
22073 c170dcbe6c9d formalisation of Crary's chapter on logical relations urbanc parents: 22067 diff changeset	1237	Nominal/Examples/Compile.thy \
25725 18bc59fb01b5 updated HOL-Nominal-Examples deps; wenzelm parents: 25600 diff changeset	1238	Nominal/Examples/Contexts.thy \
18bc59fb01b5 updated HOL-Nominal-Examples deps; wenzelm parents: 25600 diff changeset	1239	Nominal/Examples/Crary.thy \
22073 c170dcbe6c9d formalisation of Crary's chapter on logical relations urbanc parents: 22067 diff changeset	1240	Nominal/Examples/Fsub.thy \
25725 18bc59fb01b5 updated HOL-Nominal-Examples deps; wenzelm parents: 25600 diff changeset	1241	Nominal/Examples/Height.thy \
18bc59fb01b5 updated HOL-Nominal-Examples deps; wenzelm parents: 25600 diff changeset	1242	Nominal/Examples/Lam_Funs.thy \
22073 c170dcbe6c9d formalisation of Crary's chapter on logical relations urbanc parents: 22067 diff changeset	1243	Nominal/Examples/Lambda_mu.thy \
25725 18bc59fb01b5 updated HOL-Nominal-Examples deps; wenzelm parents: 25600 diff changeset	1244	Nominal/Examples/LocalWeakening.thy \
33189 82a40677c1f8 Added Pattern.thy to Nominal/Examples. berghofe parents: 33176 diff changeset	1245	Nominal/Examples/Pattern.thy \
25725 18bc59fb01b5 updated HOL-Nominal-Examples deps; wenzelm parents: 25600 diff changeset	1246	Nominal/Examples/ROOT.ML \
22073 c170dcbe6c9d formalisation of Crary's chapter on logical relations urbanc parents: 22067 diff changeset	1247	Nominal/Examples/SN.thy \
23144 4a9c9e260abf included new example in the compiling process urbanc parents: 23100 diff changeset	1248	Nominal/Examples/SOS.thy \
27624 a925aa66e17a Added Standardization theory to nominal examples. berghofe parents: 27484 diff changeset	1249	Nominal/Examples/Standardization.thy \
24896 70f238757695 added the two new examples from Nominal to the build process urbanc parents: 24830 diff changeset	1250	Nominal/Examples/Support.thy \
27032 6fd85edc403d new example urbanc parents: 26878 diff changeset	1251	Nominal/Examples/Type_Preservation.thy \
25725 18bc59fb01b5 updated HOL-Nominal-Examples deps; wenzelm parents: 25600 diff changeset	1252	Nominal/Examples/VC_Condition.thy \
26195 8292f8723e99 added new example urbanc parents: 26192 diff changeset	1253	Nominal/Examples/W.thy \
25725 18bc59fb01b5 updated HOL-Nominal-Examples deps; wenzelm parents: 25600 diff changeset	1254	Nominal/Examples/Weakening.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	1255	@cd Nominal; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Nominal Examples
19497 630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	1256
630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	1257
24333 e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	1258	## HOL-Word
e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	1259
e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	1260	HOL-Word: HOL $(OUT)/HOL-Word
e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	1261
33024 60a098883d81 more accurate dependencies for HOL-SMT, which is a session with image; wenzelm parents: 33010 diff changeset	1262	$(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML Library/Boolean_Algebra.thy \
37655 f4d616d41a59 more speaking theory names haftmann parents: 37583 diff changeset	1263	Library/Numeral_Type.thy Word/Misc_Numeric.thy Word/Misc_Typedef.thy \
37659 14cabf5fa710 more speaking names haftmann parents: 37655 diff changeset	1264	Word/Type_Length.thy Word/Bit_Representation.thy Word/Bit_Int.thy \
14cabf5fa710 more speaking names haftmann parents: 37655 diff changeset	1265	Word/Bool_List_Representation.thy Word/Bit_Operations.thy \
37660 56e3520b68b2 one unified Word theory haftmann parents: 37659 diff changeset	1266	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	1267	Word/document/root.bib Word/Tools/smt_word.ML
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	1268	@cd Word; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Word
24333 e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	1269
e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	1270
24442 39e29972cb96 HOL-Word-Examples huffman parents: 24411 diff changeset	1271	## HOL-Word-Examples
39e29972cb96 HOL-Word-Examples huffman parents: 24411 diff changeset	1272
39e29972cb96 HOL-Word-Examples huffman parents: 24411 diff changeset	1273	HOL-Word-Examples: HOL-Word $(LOG)/HOL-Word-Examples.gz
39e29972cb96 HOL-Word-Examples huffman parents: 24411 diff changeset	1274
27164 81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	1275	$(LOG)/HOL-Word-Examples.gz: $(OUT)/HOL-Word Word/Examples/ROOT.ML \
24442 39e29972cb96 HOL-Word-Examples huffman parents: 24411 diff changeset	1276	Word/Examples/WordExamples.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	1277	@cd Word; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Word Examples
24442 39e29972cb96 HOL-Word-Examples huffman parents: 24411 diff changeset	1278
27477 c64736fe2a1f more precise dependencies for HOL-Word and HOL-NSA; wenzelm parents: 27470 diff changeset	1279
25171 4a9c25bffc9b added Statespace library schirmer parents: 24994 diff changeset	1280	## HOL-Statespace
4a9c25bffc9b added Statespace library schirmer parents: 24994 diff changeset	1281
4a9c25bffc9b added Statespace library schirmer parents: 24994 diff changeset	1282	HOL-Statespace: HOL $(LOG)/HOL-Statespace.gz
4a9c25bffc9b added Statespace library schirmer parents: 24994 diff changeset	1283
27164 81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	1284	$(LOG)/HOL-Statespace.gz: $(OUT)/HOL Statespace/DistinctTreeProver.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	1285	Statespace/StateFun.thy Statespace/StateSpaceLocale.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	1286	Statespace/StateSpaceSyntax.thy Statespace/StateSpaceEx.thy \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	1287	Statespace/distinct_tree_prover.ML Statespace/state_space.ML \
81632fd4ff61 some reformatting; wenzelm parents: 27163 diff changeset	1288	Statespace/state_fun.ML Statespace/document/root.tex
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	1289	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Statespace
24442 39e29972cb96 HOL-Word-Examples huffman parents: 24411 diff changeset	1290
27477 c64736fe2a1f more precise dependencies for HOL-Word and HOL-NSA; wenzelm parents: 27470 diff changeset	1291
27470 84526c368a58 add HOL-NSA huffman parents: 27456 diff changeset	1292	## HOL-NSA
84526c368a58 add HOL-NSA huffman parents: 27456 diff changeset	1293
27477 c64736fe2a1f more precise dependencies for HOL-Word and HOL-NSA; wenzelm parents: 27470 diff changeset	1294	HOL-NSA: HOL $(OUT)/HOL-NSA
27470 84526c368a58 add HOL-NSA huffman parents: 27456 diff changeset	1295
33024 60a098883d81 more accurate dependencies for HOL-SMT, which is a session with image; wenzelm parents: 33010 diff changeset	1296	$(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	1297	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	1298	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	1299	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	1300	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	1301	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	1302	Library/Infinite_Set.thy Library/Zorn.thy NSA/ROOT.ML
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	1303	@cd NSA; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-NSA
27470 84526c368a58 add HOL-NSA huffman parents: 27456 diff changeset	1304
27477 c64736fe2a1f more precise dependencies for HOL-Word and HOL-NSA; wenzelm parents: 27470 diff changeset	1305
27470 84526c368a58 add HOL-NSA huffman parents: 27456 diff changeset	1306	## HOL-NSA-Examples
84526c368a58 add HOL-NSA huffman parents: 27456 diff changeset	1307
84526c368a58 add HOL-NSA huffman parents: 27456 diff changeset	1308	HOL-NSA-Examples: HOL-NSA $(LOG)/HOL-NSA-Examples.gz
84526c368a58 add HOL-NSA huffman parents: 27456 diff changeset	1309
37742 d8e7f473c3a1 tuned tabs haftmann parents: 37691 diff changeset	1310	$(LOG)/HOL-NSA-Examples.gz: $(OUT)/HOL-NSA NSA/Examples/ROOT.ML \
27470 84526c368a58 add HOL-NSA huffman parents: 27456 diff changeset	1311	NSA/Examples/NSPrimes.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 28477 diff changeset	1312	@cd NSA; $(ISABELLE_TOOL) usedir $(OUT)/HOL-NSA Examples
27470 84526c368a58 add HOL-NSA huffman parents: 27456 diff changeset	1313
27477 c64736fe2a1f more precise dependencies for HOL-Word and HOL-NSA; wenzelm parents: 27470 diff changeset	1314
32496 4ab00a2642c3 moved Mirabelle from HOL/Tools to HOL, boehmes parents: 32479 diff changeset	1315	## HOL-Mirabelle
4ab00a2642c3 moved Mirabelle from HOL/Tools to HOL, boehmes parents: 32479 diff changeset	1316
4ab00a2642c3 moved Mirabelle from HOL/Tools to HOL, boehmes parents: 32479 diff changeset	1317	HOL-Mirabelle: HOL $(LOG)/HOL-Mirabelle.gz
4ab00a2642c3 moved Mirabelle from HOL/Tools to HOL, boehmes parents: 32479 diff changeset	1318
33024 60a098883d81 more accurate dependencies for HOL-SMT, which is a session with image; wenzelm parents: 33010 diff changeset	1319	$(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	1320	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	1321	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	1322	Mirabelle/Tools/mirabelle_metis.ML \
60a098883d81 more accurate dependencies for HOL-SMT, which is a session with image; wenzelm parents: 33010 diff changeset	1323	Mirabelle/Tools/mirabelle_quickcheck.ML \
60a098883d81 more accurate dependencies for HOL-SMT, which is a session with image; wenzelm parents: 33010 diff changeset	1324	Mirabelle/Tools/mirabelle_refute.ML \
40634 dc124a486f94 adding dependencies to IsaMakefile; adding sledgehammer_tactic in Mirabelle_Test bulwahn parents: 40632 diff changeset	1325	Mirabelle/Tools/mirabelle_sledgehammer.ML \
41407 2878845bc549 made SML/NJ happy; wenzelm parents: 41358 diff changeset	1326	Mirabelle/Tools/mirabelle_sledgehammer_filter.ML \
42071 04577a7e0c51 move "TPTP" wrapper and "Sledgehammer as a tactic" to "HOL/ex" blanchet parents: 42064 diff changeset	1327	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	1328	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	1329	Library/Inner_Product.thy
32496 4ab00a2642c3 moved Mirabelle from HOL/Tools to HOL, boehmes parents: 32479 diff changeset	1330	@$(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	1331	@cd Library; $(ISABELLE_TOOL) mirabelle -q arith Inner_Product.thy # some arbitrary small test case
32496 4ab00a2642c3 moved Mirabelle from HOL/Tools to HOL, boehmes parents: 32479 diff changeset	1332
4ab00a2642c3 moved Mirabelle from HOL/Tools to HOL, boehmes parents: 32479 diff changeset	1333
36933 705b58fde476 more precise dependencies for HOL-Word-SMT_Examples; wenzelm parents: 36916 diff changeset	1334	## HOL-Word-SMT_Examples
32618 42865636d006 added new method "smt": an oracle-based connection to external SMT solvers boehmes parents: 32558 diff changeset	1335
36933 705b58fde476 more precise dependencies for HOL-Word-SMT_Examples; wenzelm parents: 36916 diff changeset	1336	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	1337
36933 705b58fde476 more precise dependencies for HOL-Word-SMT_Examples; wenzelm parents: 36916 diff changeset	1338	$(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	1339	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	1340	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	1341	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	1342	@$(ISABELLE_TOOL) usedir $(OUT)/HOL-Word SMT_Examples
33010 39f73a59e855 added proof reconstructon for Z3, boehmes parents: 32812 diff changeset	1343
39f73a59e855 added proof reconstructon for Z3, boehmes parents: 32812 diff changeset	1344
33419 8ae45e87b992 added HOL-Boogie boehmes parents: 33356 diff changeset	1345	## HOL-Boogie
8ae45e87b992 added HOL-Boogie boehmes parents: 33356 diff changeset	1346
36899 bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable boehmes parents: 36898 diff changeset	1347	HOL-Boogie: HOL-Word $(OUT)/HOL-Boogie
33419 8ae45e87b992 added HOL-Boogie boehmes parents: 33356 diff changeset	1348
36901 a20c5484dc9c more precise dependencies boehmes parents: 36900 diff changeset	1349	$(OUT)/HOL-Boogie: $(OUT)/HOL-Word Boogie/ROOT.ML Boogie/Boogie.thy \
33439 f5d95787224f more accurate dependencies; wenzelm parents: 33437 diff changeset	1350	Boogie/Tools/boogie_vcs.ML Boogie/Tools/boogie_loader.ML \
34069 c1fd26512f6d updated dependencies boehmes parents: 34067 diff changeset	1351	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	1352	@cd Boogie; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-Boogie
33419 8ae45e87b992 added HOL-Boogie boehmes parents: 33356 diff changeset	1353
8ae45e87b992 added HOL-Boogie boehmes parents: 33356 diff changeset	1354
8ae45e87b992 added HOL-Boogie boehmes parents: 33356 diff changeset	1355	## HOL-Boogie_Examples
8ae45e87b992 added HOL-Boogie boehmes parents: 33356 diff changeset	1356
33439 f5d95787224f more accurate dependencies; wenzelm parents: 33437 diff changeset	1357	HOL-Boogie-Examples: HOL-Boogie $(LOG)/HOL-Boogie-Examples.gz
33419 8ae45e87b992 added HOL-Boogie boehmes parents: 33356 diff changeset	1358
33439 f5d95787224f more accurate dependencies; wenzelm parents: 33437 diff changeset	1359	$(LOG)/HOL-Boogie-Examples.gz: $(OUT)/HOL-Boogie \
f5d95787224f more accurate dependencies; wenzelm parents: 33437 diff changeset	1360	Boogie/Examples/ROOT.ML Boogie/Examples/Boogie_Max.thy \
f5d95787224f more accurate dependencies; wenzelm parents: 33437 diff changeset	1361	Boogie/Examples/Boogie_Max.b2i Boogie/Examples/Boogie_Dijkstra.thy \
f5d95787224f more accurate dependencies; wenzelm parents: 33437 diff changeset	1362	Boogie/Examples/VCC_Max.thy Boogie/Examples/Boogie_Dijkstra.b2i \
34996 51c93ab92c3e updated dependencies boehmes parents: 34974 diff changeset	1363	Boogie/Examples/VCC_Max.b2i Boogie/Examples/Boogie_Max.certs \
51c93ab92c3e updated dependencies boehmes parents: 34974 diff changeset	1364	Boogie/Examples/Boogie_Dijkstra.certs Boogie/Examples/VCC_Max.certs
33419 8ae45e87b992 added HOL-Boogie boehmes parents: 33356 diff changeset	1365	@cd Boogie; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Boogie Examples
8ae45e87b992 added HOL-Boogie boehmes parents: 33356 diff changeset	1366
8ae45e87b992 added HOL-Boogie boehmes parents: 33356 diff changeset	1367
41566 676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1368	## HOL-SPARK
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1369
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1370	HOL-SPARK: HOL-Word $(OUT)/HOL-SPARK
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1371
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1372	$(OUT)/HOL-SPARK: $(OUT)/HOL-Word SPARK/ROOT.ML \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1373	SPARK/SPARK.thy SPARK/SPARK_Setup.thy \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1374	SPARK/Tools/fdl_lexer.ML SPARK/Tools/fdl_parser.ML \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1375	SPARK/Tools/spark_commands.ML SPARK/Tools/spark_vcs.ML
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1376	@cd SPARK; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SPARK
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1377
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1378
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1379	## HOL-SPARK-Examples
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1380
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1381	HOL-SPARK-Examples: HOL-SPARK $(LOG)/HOL-SPARK-Examples.gz
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1382
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1383	$(LOG)/HOL-SPARK-Examples.gz: $(OUT)/HOL-SPARK \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1384	SPARK/Examples/ROOT.ML \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1385	SPARK/Examples/Gcd/Greatest_Common_Divisor.thy \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1386	SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.fdl \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1387	SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.rls \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1388	SPARK/Examples/Gcd/greatest_common_divisor/g_c_d.siv \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1389	SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1390	SPARK/Examples/Liseq/liseq/liseq_length.fdl \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1391	SPARK/Examples/Liseq/liseq/liseq_length.rls \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1392	SPARK/Examples/Liseq/liseq/liseq_length.siv \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1393	SPARK/Examples/RIPEMD-160/F.thy SPARK/Examples/RIPEMD-160/Hash.thy \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1394	SPARK/Examples/RIPEMD-160/K_L.thy SPARK/Examples/RIPEMD-160/K_R.thy \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1395	SPARK/Examples/RIPEMD-160/R_L.thy \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1396	SPARK/Examples/RIPEMD-160/RMD_Lemmas.thy \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1397	SPARK/Examples/RIPEMD-160/RMD_Specification.thy \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1398	SPARK/Examples/RIPEMD-160/RMD.thy SPARK/Examples/RIPEMD-160/Round.thy \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1399	SPARK/Examples/RIPEMD-160/R_R.thy SPARK/Examples/RIPEMD-160/S_L.thy \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1400	SPARK/Examples/RIPEMD-160/S_R.thy \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1401	SPARK/Examples/RIPEMD-160/rmd/f.fdl \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1402	SPARK/Examples/RIPEMD-160/rmd/f.rls \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1403	SPARK/Examples/RIPEMD-160/rmd/f.siv \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1404	SPARK/Examples/RIPEMD-160/rmd/hash.fdl \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1405	SPARK/Examples/RIPEMD-160/rmd/hash.rls \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1406	SPARK/Examples/RIPEMD-160/rmd/hash.siv \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1407	SPARK/Examples/RIPEMD-160/rmd/k_l.fdl \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1408	SPARK/Examples/RIPEMD-160/rmd/k_l.rls \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1409	SPARK/Examples/RIPEMD-160/rmd/k_l.siv \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1410	SPARK/Examples/RIPEMD-160/rmd/k_r.fdl \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1411	SPARK/Examples/RIPEMD-160/rmd/k_r.rls \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1412	SPARK/Examples/RIPEMD-160/rmd/k_r.siv \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1413	SPARK/Examples/RIPEMD-160/rmd/r_l.fdl \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1414	SPARK/Examples/RIPEMD-160/rmd/r_l.rls \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1415	SPARK/Examples/RIPEMD-160/rmd/r_l.siv \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1416	SPARK/Examples/RIPEMD-160/rmd/round.fdl \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1417	SPARK/Examples/RIPEMD-160/rmd/round.rls \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1418	SPARK/Examples/RIPEMD-160/rmd/round.siv \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1419	SPARK/Examples/RIPEMD-160/rmd/r_r.fdl \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1420	SPARK/Examples/RIPEMD-160/rmd/r_r.rls \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1421	SPARK/Examples/RIPEMD-160/rmd/r_r.siv \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1422	SPARK/Examples/RIPEMD-160/rmd/s_l.fdl \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1423	SPARK/Examples/RIPEMD-160/rmd/s_l.rls \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1424	SPARK/Examples/RIPEMD-160/rmd/s_l.siv \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1425	SPARK/Examples/RIPEMD-160/rmd/s_r.fdl \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1426	SPARK/Examples/RIPEMD-160/rmd/s_r.rls \
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1427	SPARK/Examples/RIPEMD-160/rmd/s_r.siv
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1428	@cd SPARK; $(ISABELLE_TOOL) usedir $(OUT)/HOL-SPARK Examples
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1429
676b32bea254 Added HOL-SPARK and removed old_primrec.ML berghofe parents: 41505 diff changeset	1430
34965 3b4762c1052c adding Mutabelle to repository bulwahn parents: 34958 diff changeset	1431	## HOL-Mutabelle
3b4762c1052c adding Mutabelle to repository bulwahn parents: 34958 diff changeset	1432
3b4762c1052c adding Mutabelle to repository bulwahn parents: 34958 diff changeset	1433	HOL-Mutabelle: HOL $(LOG)/HOL-Mutabelle.gz
3b4762c1052c adding Mutabelle to repository bulwahn parents: 34958 diff changeset	1434
3b4762c1052c adding Mutabelle to repository bulwahn parents: 34958 diff changeset	1435	$(LOG)/HOL-Mutabelle.gz: $(OUT)/HOL Mutabelle/MutabelleExtra.thy \
35959 b88e061754a1 more precise dependencies; wenzelm parents: 35957 diff changeset	1436	Mutabelle/ROOT.ML Mutabelle/mutabelle.ML \
34965 3b4762c1052c adding Mutabelle to repository bulwahn parents: 34958 diff changeset	1437	Mutabelle/mutabelle_extra.ML
3b4762c1052c adding Mutabelle to repository bulwahn parents: 34958 diff changeset	1438	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mutabelle
3b4762c1052c adding Mutabelle to repository bulwahn parents: 34958 diff changeset	1439
3b4762c1052c adding Mutabelle to repository bulwahn parents: 34958 diff changeset	1440
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35151 diff changeset	1441	## HOL-Quotient_Examples
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35151 diff changeset	1442
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35151 diff changeset	1443	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	1444
35959 b88e061754a1 more precise dependencies; wenzelm parents: 35957 diff changeset	1445	$(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL \
37742 d8e7f473c3a1 tuned tabs haftmann parents: 37691 diff changeset	1446	Quotient_Examples/FSet.thy Quotient_Examples/Quotient_Int.thy \
36524 3909002beca5 Tuning the quotient examples Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 36403 diff changeset	1447	Quotient_Examples/Quotient_Message.thy
35222 4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35151 diff changeset	1448	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35151 diff changeset	1449
4f1fba00f66d Initial version of HOL quotient package. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 35151 diff changeset	1450
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	1451	## 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	1452
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	1453	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	1454
35959 b88e061754a1 more precise dependencies; wenzelm parents: 35957 diff changeset	1455	$(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	1456	Predicate_Compile_Examples/ROOT.ML \
39655 8ad7fe9d6f0b splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests bulwahn parents: 39564 diff changeset	1457	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	1458	Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy \
38730 5bbdd9a9df62 adding hotel keycard example for prolog generation bulwahn parents: 38656 diff changeset	1459	Predicate_Compile_Examples/Code_Prolog_Examples.thy \
39655 8ad7fe9d6f0b splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests bulwahn parents: 39564 diff changeset	1460	Predicate_Compile_Examples/Examples.thy \
39185 c035d01a7e77 adding the CFG example to the build process bulwahn parents: 39184 diff changeset	1461	Predicate_Compile_Examples/Context_Free_Grammar_Example.thy \
38948 c4e6afaa8dcd adding Lambda example theory; tuned bulwahn parents: 38730 diff changeset	1462	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	1463	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	1464	Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy \
39186 475856793715 adding IMP quickcheck examples bulwahn parents: 39185 diff changeset	1465	Predicate_Compile_Examples/IMP_1.thy \
475856793715 adding IMP quickcheck examples bulwahn parents: 39185 diff changeset	1466	Predicate_Compile_Examples/IMP_2.thy \
475856793715 adding IMP quickcheck examples bulwahn parents: 39185 diff changeset	1467	Predicate_Compile_Examples/IMP_3.thy \
475856793715 adding IMP quickcheck examples bulwahn parents: 39185 diff changeset	1468	Predicate_Compile_Examples/IMP_4.thy \
39184 71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: 39183 diff changeset	1469	Predicate_Compile_Examples/Lambda_Example.thy \
39188 cd6558ed65d7 adding the Reg_Exp example bulwahn parents: 39186 diff changeset	1470	Predicate_Compile_Examples/List_Examples.thy \
cd6558ed65d7 adding the Reg_Exp example bulwahn parents: 39186 diff changeset	1471	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	1472	@$(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	1473
35959 b88e061754a1 more precise dependencies; wenzelm parents: 35957 diff changeset	1474
40774 0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1475	## HOLCF
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1476
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1477	HOLCF: HOL $(OUT)/HOLCF
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1478
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1479	$(OUT)/HOLCF: $(OUT)/HOL \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1480	HOLCF/ROOT.ML \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1481	HOLCF/Adm.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1482	HOLCF/Algebraic.thy \
41286 3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9) huffman parents: 41285 diff changeset	1483	HOLCF/Bifinite.thy \
40774 0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1484	HOLCF/Cfun.thy \
41284 6d66975b711f renamed CompactBasis.thy to Compact_Basis.thy huffman parents: 41144 diff changeset	1485	HOLCF/Compact_Basis.thy \
40774 0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1486	HOLCF/Completion.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1487	HOLCF/Cont.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1488	HOLCF/ConvexPD.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1489	HOLCF/Cpodef.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1490	HOLCF/Cprod.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1491	HOLCF/Discrete.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1492	HOLCF/Deflation.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1493	HOLCF/Domain.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1494	HOLCF/Domain_Aux.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1495	HOLCF/Fixrec.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1496	HOLCF/Fix.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1497	HOLCF/Fun_Cpo.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1498	HOLCF/HOLCF.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1499	HOLCF/Lift.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1500	HOLCF/LowerPD.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1501	HOLCF/Map_Functions.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1502	HOLCF/One.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1503	HOLCF/Pcpo.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1504	HOLCF/Plain_HOLCF.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1505	HOLCF/Porder.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1506	HOLCF/Powerdomains.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1507	HOLCF/Product_Cpo.thy \
41285 efd23c1d9886 renamed Bifinite.thy to Representable.thy huffman parents: 41284 diff changeset	1508	HOLCF/Representable.thy \
40774 0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1509	HOLCF/Sfun.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1510	HOLCF/Sprod.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1511	HOLCF/Ssum.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1512	HOLCF/Tr.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1513	HOLCF/Universal.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1514	HOLCF/UpperPD.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1515	HOLCF/Up.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1516	HOLCF/Tools/cont_consts.ML \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1517	HOLCF/Tools/cont_proc.ML \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1518	HOLCF/Tools/holcf_library.ML \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1519	HOLCF/Tools/Domain/domain.ML \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1520	HOLCF/Tools/Domain/domain_axioms.ML \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1521	HOLCF/Tools/Domain/domain_constructors.ML \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1522	HOLCF/Tools/Domain/domain_induction.ML \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1523	HOLCF/Tools/Domain/domain_isomorphism.ML \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1524	HOLCF/Tools/Domain/domain_take_proofs.ML \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1525	HOLCF/Tools/cpodef.ML \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1526	HOLCF/Tools/domaindef.ML \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1527	HOLCF/Tools/fixrec.ML \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1528	HOLCF/document/root.tex
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1529	@cd HOLCF; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOLCF
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1530
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1531
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1532	## HOLCF-Tutorial
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1533
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1534	HOLCF-Tutorial: HOLCF $(LOG)/HOLCF-Tutorial.gz
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1535
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1536	$(LOG)/HOLCF-Tutorial.gz: $(OUT)/HOLCF \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1537	HOLCF/Tutorial/Domain_ex.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1538	HOLCF/Tutorial/Fixrec_ex.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1539	HOLCF/Tutorial/New_Domain.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1540	HOLCF/Tutorial/document/root.tex \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1541	HOLCF/Tutorial/ROOT.ML
40777 4898bae6ef23 fix cut-and-paste errors for HOLCF entries in IsaMakefile huffman parents: 40774 diff changeset	1542	@cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF Tutorial
40774 0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1543
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1544
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1545	## HOLCF-Library
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1546
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1547	HOLCF-Library: HOLCF $(LOG)/HOLCF-Library.gz
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1548
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1549	$(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \
41852 9aae2eed4696 corrected HOLCF dependency on Nat_Infinity nipkow parents: 41827 diff changeset	1550	Library/Nat_Infinity.thy \
40774 0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1551	HOLCF/Library/Defl_Bifinite.thy \
41112 866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types huffman parents: 41087 diff changeset	1552	HOLCF/Library/Bool_Discrete.thy \
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types huffman parents: 41087 diff changeset	1553	HOLCF/Library/Char_Discrete.thy \
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types huffman parents: 41087 diff changeset	1554	HOLCF/Library/HOL_Cpo.thy \
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types huffman parents: 41087 diff changeset	1555	HOLCF/Library/Int_Discrete.thy \
40774 0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1556	HOLCF/Library/List_Cpo.thy \
41112 866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types huffman parents: 41087 diff changeset	1557	HOLCF/Library/List_Predomain.thy \
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types huffman parents: 41087 diff changeset	1558	HOLCF/Library/Nat_Discrete.thy \
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types huffman parents: 41087 diff changeset	1559	HOLCF/Library/Option_Cpo.thy \
40774 0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1560	HOLCF/Library/Stream.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1561	HOLCF/Library/Sum_Cpo.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1562	HOLCF/Library/HOLCF_Library.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1563	HOLCF/Library/ROOT.ML
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1564	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Library
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1565
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1566
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1567	## HOLCF-IMP
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1568
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1569	HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1570
40777 4898bae6ef23 fix cut-and-paste errors for HOLCF entries in IsaMakefile huffman parents: 40774 diff changeset	1571	$(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF \
4898bae6ef23 fix cut-and-paste errors for HOLCF entries in IsaMakefile huffman parents: 40774 diff changeset	1572	HOLCF/IMP/HoareEx.thy \
4898bae6ef23 fix cut-and-paste errors for HOLCF entries in IsaMakefile huffman parents: 40774 diff changeset	1573	HOLCF/IMP/Denotational.thy \
4898bae6ef23 fix cut-and-paste errors for HOLCF entries in IsaMakefile huffman parents: 40774 diff changeset	1574	HOLCF/IMP/ROOT.ML \
4898bae6ef23 fix cut-and-paste errors for HOLCF entries in IsaMakefile huffman parents: 40774 diff changeset	1575	HOLCF/IMP/document/root.tex
4898bae6ef23 fix cut-and-paste errors for HOLCF entries in IsaMakefile huffman parents: 40774 diff changeset	1576	@cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF IMP
40774 0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1577
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1578
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1579	## HOLCF-ex
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1580
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1581	HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1582
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1583	$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1584	HOLCF/ex/Dagstuhl.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1585	HOLCF/ex/Dnat.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1586	HOLCF/ex/Domain_Proofs.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1587	HOLCF/ex/Fix2.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1588	HOLCF/ex/Focus_ex.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1589	HOLCF/ex/Hoare.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1590	HOLCF/ex/Letrec.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1591	HOLCF/ex/Loop.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1592	HOLCF/ex/Pattern_Match.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1593	HOLCF/ex/Powerdomain_ex.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1594	HOLCF/ex/ROOT.ML
40777 4898bae6ef23 fix cut-and-paste errors for HOLCF entries in IsaMakefile huffman parents: 40774 diff changeset	1595	@cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex
40774 0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1596
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1597
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1598	## HOLCF-FOCUS
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1599
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1600	HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1601
41413 64cd30d6b0b8 explicit file specifications -- avoid secondary load path; wenzelm parents: 41407 diff changeset	1602	$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF HOLCF/FOCUS/ROOT.ML \
41854 b2b5b965b59c Corrected HOLCF/FOCUS dependency nipkow parents: 41852 diff changeset	1603	Library/Nat_Infinity.thy \
40774 0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1604	HOLCF/Library/Stream.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1605	HOLCF/FOCUS/Fstreams.thy \
40777 4898bae6ef23 fix cut-and-paste errors for HOLCF entries in IsaMakefile huffman parents: 40774 diff changeset	1606	HOLCF/FOCUS/Fstream.thy \
4898bae6ef23 fix cut-and-paste errors for HOLCF entries in IsaMakefile huffman parents: 40774 diff changeset	1607	HOLCF/FOCUS/FOCUS.thy \
4898bae6ef23 fix cut-and-paste errors for HOLCF entries in IsaMakefile huffman parents: 40774 diff changeset	1608	HOLCF/FOCUS/Stream_adm.thy \
4898bae6ef23 fix cut-and-paste errors for HOLCF entries in IsaMakefile huffman parents: 40774 diff changeset	1609	HOLCF/FOCUS/Buffer.thy \
4898bae6ef23 fix cut-and-paste errors for HOLCF entries in IsaMakefile huffman parents: 40774 diff changeset	1610	HOLCF/FOCUS/Buffer_adm.thy \
4898bae6ef23 fix cut-and-paste errors for HOLCF entries in IsaMakefile huffman parents: 40774 diff changeset	1611	Library/Continuity.thy
4898bae6ef23 fix cut-and-paste errors for HOLCF entries in IsaMakefile huffman parents: 40774 diff changeset	1612	@cd HOLCF; $(ISABELLE_TOOL) usedir $(OUT)/HOLCF FOCUS
4898bae6ef23 fix cut-and-paste errors for HOLCF entries in IsaMakefile huffman parents: 40774 diff changeset	1613
40774 0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1614
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1615	## IOA
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1616
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1617	IOA: HOLCF $(OUT)/IOA
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1618
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1619	$(OUT)/IOA: $(OUT)/HOLCF \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1620	HOLCF/IOA/ROOT.ML \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1621	HOLCF/IOA/meta_theory/Traces.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1622	HOLCF/IOA/meta_theory/Asig.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1623	HOLCF/IOA/meta_theory/CompoScheds.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1624	HOLCF/IOA/meta_theory/CompoTraces.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1625	HOLCF/IOA/meta_theory/Seq.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1626	HOLCF/IOA/meta_theory/RefCorrectness.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1627	HOLCF/IOA/meta_theory/Automata.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1628	HOLCF/IOA/meta_theory/ShortExecutions.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1629	HOLCF/IOA/meta_theory/IOA.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1630	HOLCF/IOA/meta_theory/Sequence.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1631	HOLCF/IOA/meta_theory/CompoExecs.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1632	HOLCF/IOA/meta_theory/RefMappings.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1633	HOLCF/IOA/meta_theory/Compositionality.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1634	HOLCF/IOA/meta_theory/TL.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1635	HOLCF/IOA/meta_theory/TLS.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1636	HOLCF/IOA/meta_theory/LiveIOA.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1637	HOLCF/IOA/meta_theory/Pred.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1638	HOLCF/IOA/meta_theory/Abstraction.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1639	HOLCF/IOA/meta_theory/Simulations.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1640	HOLCF/IOA/meta_theory/SimCorrectness.thy
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1641	@cd HOLCF/IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1642
40777 4898bae6ef23 fix cut-and-paste errors for HOLCF entries in IsaMakefile huffman parents: 40774 diff changeset	1643
40774 0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1644	## IOA-ABP
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1645
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1646	IOA-ABP: IOA $(LOG)/IOA-ABP.gz
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1647
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1648	$(LOG)/IOA-ABP.gz: $(OUT)/IOA \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1649	HOLCF/IOA/ABP/Abschannel.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1650	HOLCF/IOA/ABP/Abschannel_finite.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1651	HOLCF/IOA/ABP/Action.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1652	HOLCF/IOA/ABP/Check.ML \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1653	HOLCF/IOA/ABP/Correctness.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1654	HOLCF/IOA/ABP/Env.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1655	HOLCF/IOA/ABP/Impl.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1656	HOLCF/IOA/ABP/Impl_finite.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1657	HOLCF/IOA/ABP/Lemmas.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1658	HOLCF/IOA/ABP/Packet.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1659	HOLCF/IOA/ABP/ROOT.ML \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1660	HOLCF/IOA/ABP/Receiver.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1661	HOLCF/IOA/ABP/Sender.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1662	HOLCF/IOA/ABP/Spec.thy
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1663	@cd HOLCF/IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ABP
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1664
40777 4898bae6ef23 fix cut-and-paste errors for HOLCF entries in IsaMakefile huffman parents: 40774 diff changeset	1665
40774 0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1666	## IOA-NTP
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1667
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1668	IOA-NTP: IOA $(LOG)/IOA-NTP.gz
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1669
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1670	$(LOG)/IOA-NTP.gz: $(OUT)/IOA \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1671	HOLCF/IOA/NTP/Abschannel.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1672	HOLCF/IOA/NTP/Action.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1673	HOLCF/IOA/NTP/Correctness.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1674	HOLCF/IOA/NTP/Impl.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1675	HOLCF/IOA/NTP/Lemmas.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1676	HOLCF/IOA/NTP/Multiset.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1677	HOLCF/IOA/NTP/Packet.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1678	HOLCF/IOA/NTP/ROOT.ML \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1679	HOLCF/IOA/NTP/Receiver.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1680	HOLCF/IOA/NTP/Sender.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1681	HOLCF/IOA/NTP/Spec.thy
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1682	@cd HOLCF/IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA NTP
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1683
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1684
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1685	## IOA-Storage
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1686
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1687	IOA-Storage: IOA $(LOG)/IOA-Storage.gz
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1688
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1689	$(LOG)/IOA-Storage.gz: $(OUT)/IOA \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1690	HOLCF/IOA/Storage/Action.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1691	HOLCF/IOA/Storage/Correctness.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1692	HOLCF/IOA/Storage/Impl.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1693	HOLCF/IOA/Storage/ROOT.ML \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1694	HOLCF/IOA/Storage/Spec.thy
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1695	@cd HOLCF/IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA Storage
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1696
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1697
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1698	## IOA-ex
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1699
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1700	IOA-ex: IOA $(LOG)/IOA-ex.gz
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1701
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1702	$(LOG)/IOA-ex.gz: $(OUT)/IOA \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1703	HOLCF/IOA/ex/ROOT.ML \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1704	HOLCF/IOA/ex/TrivEx.thy \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1705	HOLCF/IOA/ex/TrivEx2.thy
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1706	@cd HOLCF/IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ex
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1707
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1708
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	1709	## clean
4447 b7ee449eb345 log files; wenzelm parents: 4289 diff changeset	1710
b7ee449eb345 log files; wenzelm parents: 4289 diff changeset	1711	clean:
33450 4389ec600ba7 more accurate cleanup; wenzelm parents: 33449 diff changeset	1712	@rm -f $(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz \
4389ec600ba7 more accurate cleanup; wenzelm parents: 33449 diff changeset	1713	$(LOG)/HOL-Bali.gz $(LOG)/HOL-Base.gz \
4389ec600ba7 more accurate cleanup; wenzelm parents: 33449 diff changeset	1714	$(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	1715	$(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	1716	$(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	1717	$(LOG)/HOL-IMP.gz $(LOG)/HOL-IMPP.gz $(LOG)/HOL-IOA.gz \
33450 4389ec600ba7 more accurate cleanup; wenzelm parents: 33449 diff changeset	1718	$(LOG)/HOL-Imperative_HOL.gz $(LOG)/HOL-Import.gz \
4389ec600ba7 more accurate cleanup; wenzelm parents: 33449 diff changeset	1719	$(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	1720	$(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	1721	$(LOG)/HOL-Lex.gz $(LOG)/HOL-Library.gz \
f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.; wenzelm parents: 34126 diff changeset	1722	$(LOG)/HOL-Main.gz $(LOG)/HOL-Matrix \
f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.; wenzelm parents: 34126 diff changeset	1723	$(LOG)/HOL-Matrix.gz $(LOG)/HOL-Metis_Examples.gz \
f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.; wenzelm parents: 34126 diff changeset	1724	$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-Mirabelle.gz \
33450 4389ec600ba7 more accurate cleanup; wenzelm parents: 33449 diff changeset	1725	$(LOG)/HOL-Multivariate_Analysis.gz \
4389ec600ba7 more accurate cleanup; wenzelm parents: 33449 diff changeset	1726	$(LOG)/HOL-NSA-Examples.gz $(LOG)/HOL-NSA.gz \
4389ec600ba7 more accurate cleanup; wenzelm parents: 33449 diff changeset	1727	$(LOG)/HOL-NanoJava.gz $(LOG)/HOL-Nitpick_Examples.gz \
4389ec600ba7 more accurate cleanup; wenzelm parents: 33449 diff changeset	1728	$(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-Nominal.gz \
4389ec600ba7 more accurate cleanup; wenzelm parents: 33449 diff changeset	1729	$(LOG)/HOL-Number_Theory.gz \
4389ec600ba7 more accurate cleanup; wenzelm parents: 33449 diff changeset	1730	$(LOG)/HOL-Old_Number_Theory.gz $(LOG)/HOL-Plain.gz \
35959 b88e061754a1 more precise dependencies; wenzelm parents: 35957 diff changeset	1731	$(LOG)/HOL-Predicate_Compile_Examples.gz \
33450 4389ec600ba7 more accurate cleanup; wenzelm parents: 33449 diff changeset	1732	$(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	1733	$(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	1734	$(LOG)/HOL-Proofs-Extraction.gz \
34205 f69cd974bc4e explicit session HOL-Proofs -- avoid statefulness of main HOL image wrt. HOL_proofs etc.; wenzelm parents: 34126 diff changeset	1735	$(LOG)/HOL-Proofs-Lambda.gz $(LOG)/HOL-SET_Protocol.gz \
36933 705b58fde476 more precise dependencies for HOL-Word-SMT_Examples; wenzelm parents: 36916 diff changeset	1736	$(LOG)/HOL-Word-SMT_Examples.gz \
41569 98f59921c420 Also added SPARK to test and clean targets. berghofe parents: 41566 diff changeset	1737	$(LOG)/HOL-SPARK.gz $(LOG)/HOL-SPARK-Examples.gz \
36933 705b58fde476 more precise dependencies for HOL-Word-SMT_Examples; wenzelm parents: 36916 diff changeset	1738	$(LOG)/HOL-Statespace.gz $(LOG)/HOL-Subst.gz \
705b58fde476 more precise dependencies for HOL-Word-SMT_Examples; wenzelm parents: 36916 diff changeset	1739	$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz \
705b58fde476 more precise dependencies for HOL-Word-SMT_Examples; wenzelm parents: 36916 diff changeset	1740	$(LOG)/HOL-Word-Examples.gz $(LOG)/HOL-Word.gz \
705b58fde476 more precise dependencies for HOL-Word-SMT_Examples; wenzelm parents: 36916 diff changeset	1741	$(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz $(LOG)/HOL.gz \
705b58fde476 more precise dependencies for HOL-Word-SMT_Examples; wenzelm parents: 36916 diff changeset	1742	$(LOG)/HOL4.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Inc.gz \
705b58fde476 more precise dependencies for HOL-Word-SMT_Examples; wenzelm parents: 36916 diff changeset	1743	$(LOG)/TLA-Memory.gz $(LOG)/TLA.gz $(OUT)/HOL \
705b58fde476 more precise dependencies for HOL-Word-SMT_Examples; wenzelm parents: 36916 diff changeset	1744	$(OUT)/HOL-Algebra $(OUT)/HOL-Base $(OUT)/HOL-Boogie \
705b58fde476 more precise dependencies for HOL-Word-SMT_Examples; wenzelm parents: 36916 diff changeset	1745	$(OUT)/HOL-Main $(OUT)/HOL-Multivariate_Analysis \
705b58fde476 more precise dependencies for HOL-Word-SMT_Examples; wenzelm parents: 36916 diff changeset	1746	$(OUT)/HOL-NSA $(OUT)/HOL-Nominal $(OUT)/HOL-Plain \
35931 6c9f7dc1ad07 more accurate dependencies; wenzelm parents: 35928 diff changeset	1747	$(OUT)/HOL-Probability $(OUT)/HOL-Proofs \
41569 98f59921c420 Also added SPARK to test and clean targets. berghofe parents: 41566 diff changeset	1748	$(OUT)/HOL-SPARK \
40774 0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1749	$(OUT)/HOL-Word $(OUT)/HOL4 $(OUT)/TLA \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1750	$(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1751	$(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1752	$(LOG)/IOA.gz $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1753	$(LOG)/IOA-Storage.gz $(LOG)/HOLCF-Library.gz \
0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40676 diff changeset	1754	$(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz

author	blanchet
	Fri, 27 May 2011 10:30:08 +0200
changeset 43016	42330f25142c
parent 42861	16375b493b64
child 43018	121aa59b4d17
permissions	-rw-r--r--