isabelle: src/HOL/IsaMakefile@509e51b7509a (annotated)

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

author	blanchet
	Wed, 15 Dec 2010 11:26:28 +0100
changeset 41144	509e51b7509a
parent 41112	866148b76247
child 41284	6d66975b711f
permissions	-rw-r--r--