isabelle: src/HOL/IsaMakefile@4d51ddd6aa5c (annotated)

2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	1	#
61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	2	# IsaMakefile for HOL
61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	3	#
61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	4
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	5	## targets
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	6
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	7	default: HOL
17460 7780d953598c generate: added HOL-Complex-Generate-HOLLight; wenzelm parents: 17430 diff changeset	8	generate: HOL-Complex-Generate-HOL HOL-Complex-Generate-HOLLight
24333 e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	9	images: HOL HOL-Algebra HOL-Complex HOL-Complex-Matrix HOL-Nominal \
e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	10	HOL-Word TLA HOL4
10135 c2a4dccf6e67 reorganized AxClasses; wenzelm parents: 10094 diff changeset	11
25321 e34b2265698a activated HOL-SizeChange; wenzelm parents: 25315 diff changeset	12	#Note: keep targets sorted (except for HOL-Library and HOL-ex)
10157 6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	13	test: \
24373 eb199bbbaec0 use HOL-ex later; wenzelm parents: 24339 diff changeset	14	HOL-Library \
24325 5c29e8822f50 make HOL-ex earlier; wenzelm parents: 24288 diff changeset	15	HOL-ex \
10157 6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	16	HOL-Auth \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	17	HOL-AxClasses \
14031 3240066af013 Added Bali to test schirmer parents: 14029 diff changeset	18	HOL-Bali \
17610 58778df33e2f tuned order of targets; wenzelm parents: 17546 diff changeset	19	HOL-Complex-HahnBanach \
15771 08cc20626a0f restored the target HOL-Complex-Import paulson parents: 15731 diff changeset	20	HOL-Complex-Import \
17610 58778df33e2f tuned order of targets; wenzelm parents: 17546 diff changeset	21	HOL-Complex-ex \
13403 bc2b32ee62fd Added theory for setting up program extraction. berghofe parents: 13224 diff changeset	22	HOL-Extraction \
10157 6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	23	HOL-Hoare \
13019 98f0a09a33c3 Target HoareParallel in IsaMakefile prensani parents: 13004 diff changeset	24	HOL-HoareParallel \
10157 6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	25	HOL-IMP \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	26	HOL-IMPP \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	27	HOL-IOA \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	28	HOL-Induct \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	29	HOL-Isar_examples \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	30	HOL-Lambda \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	31	HOL-Lattice \
23449 dd874e6a3282 integration of Metis prover paulson parents: 23445 diff changeset	32	HOL-MetisExamples \
10157 6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	33	HOL-MicroJava \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	34	HOL-Modelcheck \
11376 bf98ad1c22c6 added NanoJava oheimb parents: 11370 diff changeset	35	HOL-NanoJava \
19497 630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	36	HOL-Nominal-Examples \
10157 6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	37	HOL-NumberTheory \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	38	HOL-Prolog \
14199 d3b8d972a488 new session HOL-SET-Protocol paulson parents: 14182 diff changeset	39	HOL-SET-Protocol \
25321 e34b2265698a activated HOL-SizeChange; wenzelm parents: 25315 diff changeset	40	HOL-SizeChange \
25171 4a9c25bffc9b added Statespace library schirmer parents: 24994 diff changeset	41	HOL-Statespace \
10157 6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	42	HOL-Subst \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	43	TLA-Buffer \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	44	TLA-Inc \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	45	TLA-Memory \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	46	HOL-UNITY \
10966 8f2c27041a8e added HOL-Unix example; wenzelm parents: 10945 diff changeset	47	HOL-Unix \
10157 6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	48	HOL-W0 \
24442 39e29972cb96 HOL-Word-Examples huffman parents: 24411 diff changeset	49	HOL-Word-Examples \
24325 5c29e8822f50 make HOL-ex earlier; wenzelm parents: 24288 diff changeset	50	HOL-ZF
10157 6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	51	# ^ this is the sort position
10614 d5c14e205c24 added Library/Rational_Numbers.thy; wenzelm parents: 10574 diff changeset	52
24754 c6dd5afed3d1 Added target for proof term sessions (those that need -p 2) kleing parents: 24699 diff changeset	53	proofterms: HOL HOL-Extraction HOL-Lambda
c6dd5afed3d1 Added target for proof term sessions (those that need -p 2) kleing parents: 24699 diff changeset	54
10157 6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	55	all: test images
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	56
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	57
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	58	## global settings
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	59
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	60	SRC = $(ISABELLE_HOME)/src
3118 24dae6222579 fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?); wenzelm parents: 3079 diff changeset	61	OUT = $(ISABELLE_OUTPUT)
4447 b7ee449eb345 log files; wenzelm parents: 4289 diff changeset	62	LOG = $(OUT)/log
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	63
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	64
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	65	## HOL
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	66
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	67	HOL: Pure $(OUT)/HOL
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	68
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	69	Pure:
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	70	@cd $(SRC)/Pure; $(ISATOOL) make Pure
3232 19a2b853ba7b Removal of ex/LexProd; TFL files; new treatment of Prover files paulson parents: 3222 diff changeset	71
23194 085fa3def13b tuned webertj parents: 23193 diff changeset	72	$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \
085fa3def13b tuned webertj parents: 23193 diff changeset	73	$(SRC)/Provers/Arith/assoc_fold.ML \
085fa3def13b tuned webertj parents: 23193 diff changeset	74	$(SRC)/Provers/Arith/cancel_div_mod.ML \
085fa3def13b tuned webertj parents: 23193 diff changeset	75	$(SRC)/Provers/Arith/cancel_numeral_factor.ML \
085fa3def13b tuned webertj parents: 23193 diff changeset	76	$(SRC)/Provers/Arith/cancel_numerals.ML \
085fa3def13b tuned webertj parents: 23193 diff changeset	77	$(SRC)/Provers/Arith/cancel_sums.ML \
085fa3def13b tuned webertj parents: 23193 diff changeset	78	$(SRC)/Provers/Arith/combine_numerals.ML \
085fa3def13b tuned webertj parents: 23193 diff changeset	79	$(SRC)/Provers/Arith/extract_common_term.ML \
085fa3def13b tuned webertj parents: 23193 diff changeset	80	$(SRC)/Provers/Arith/fast_lin_arith.ML \
085fa3def13b tuned webertj parents: 23193 diff changeset	81	$(SRC)/Tools/IsaPlanner/isand.ML \
085fa3def13b tuned webertj parents: 23193 diff changeset	82	$(SRC)/Tools/IsaPlanner/rw_inst.ML \
085fa3def13b tuned webertj parents: 23193 diff changeset	83	$(SRC)/Tools/IsaPlanner/rw_tools.ML \
24830 a7b3ab44d993 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML; wenzelm parents: 24754 diff changeset	84	$(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/induct.ML $(SRC)/Provers/blast.ML \
23194 085fa3def13b tuned webertj parents: 23193 diff changeset	85	$(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
085fa3def13b tuned webertj parents: 23193 diff changeset	86	$(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML \
24830 a7b3ab44d993 moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML; wenzelm parents: 24754 diff changeset	87	$(SRC)/Provers/order.ML \
23194 085fa3def13b tuned webertj parents: 23193 diff changeset	88	$(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \
085fa3def13b tuned webertj parents: 23193 diff changeset	89	$(SRC)/Provers/quasi.ML $(SRC)/Provers/splitter.ML \
25728 71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML; wenzelm parents: 25725 diff changeset	90	$(SRC)/Provers/trancl.ML $(SRC)/Tools/Metis/metis.ML \
71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML; wenzelm parents: 25725 diff changeset	91	$(SRC)/Tools/code/code_funcgr.ML $(SRC)/Tools/code/code_name.ML \
71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML; wenzelm parents: 25725 diff changeset	92	$(SRC)/Tools/code/code_package.ML $(SRC)/Tools/code/code_target.ML \
26583 9f81ab1b7b64 fixed makefiles krauss parents: 26348 diff changeset	93	$(SRC)/Tools/code/code_thingol.ML $(SRC)/Tools/nbe.ML $(SRC)/Tools/atomize_elim.ML \
25728 71e33d95ac55 moved Pure/General/random_word.ML to Tools/random_word.ML; wenzelm parents: 25725 diff changeset	94	$(SRC)/Tools/random_word.ML $(SRC)/Tools/rat.ML Tools/TFL/casesplit.ML ATP_Linkup.thy \
26748 4d51ddd6aa5c Merged theories about wellfoundedness into one: Wellfounded.thy krauss parents: 26737 diff changeset	95	Arith_Tools.thy Code_Setup.thy Datatype.thy \
26155 7c265e3da23c HOL/Dense_Linear_Order.thy moved to Library ; resulting dependencies updated chaieb parents: 26127 diff changeset	96	Divides.thy Equiv_Relations.thy Extraction.thy \
24915 fc90277c0dd7 integrated FixedPoint into Inductive haftmann parents: 24898 diff changeset	97	Finite_Set.thy Fun.thy FunDef.thy HOL.thy \
25919 8b1c0d434824 joined theories IntDef, Numeral, IntArith to theory Int haftmann parents: 25763 diff changeset	98	Hilbert_Choice.thy Inductive.thy Int.thy IntDiv.thy \
23882 83b0f2518380 dropped Nat.ML legacy bindings haftmann parents: 23854 diff changeset	99	Lattices.thy List.thy Main.thy Map.thy Nat.thy NatBin.thy \
26737 3d46c55f03af dropped theory PreList haftmann parents: 26735 diff changeset	100	OrderedGroup.thy Orderings.thy Power.thy \
23462 11728d83794c renamed NatSimprocs.thy to Arith_Tools.thy; wenzelm parents: 23454 diff changeset	101	Predicate.thy Product_Type.thy ROOT.ML Recdef.thy \
23252 67268bb40b21 Semiring normalization and Groebner Bases. wenzelm parents: 23247 diff changeset	102	Record.thy Refute.thy Relation.thy Relation_Power.thy \
67268bb40b21 Semiring normalization and Groebner Bases. wenzelm parents: 23247 diff changeset	103	Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy Sum_Type.thy \
24288 4016baca4973 combining the relevance filter with res_atp paulson parents: 24280 diff changeset	104	Groebner_Basis.thy Tools/watcher.ML \
23252 67268bb40b21 Semiring normalization and Groebner Bases. wenzelm parents: 23247 diff changeset	105	Tools/Groebner_Basis/groebner.ML Tools/Groebner_Basis/misc.ML \
23466 886655a150f6 moved quantifier elimination tools to Tools/Qelim/; wenzelm parents: 23462 diff changeset	106	Tools/Groebner_Basis/normalizer.ML \
886655a150f6 moved quantifier elimination tools to Tools/Qelim/; wenzelm parents: 23462 diff changeset	107	Tools/Groebner_Basis/normalizer_data.ML Tools/Qelim/cooper.ML \
24082 2811a7c0f3b1 Added dependency on langford files in Tools/Qelim chaieb parents: 24036 diff changeset	108	Tools/Qelim/langford_data.ML Tools/Qelim/langford.ML \
23466 886655a150f6 moved quantifier elimination tools to Tools/Qelim/; wenzelm parents: 23462 diff changeset	109	Tools/Qelim/cooper_data.ML Tools/Qelim/ferrante_rackoff.ML \
886655a150f6 moved quantifier elimination tools to Tools/Qelim/; wenzelm parents: 23462 diff changeset	110	Tools/Qelim/ferrante_rackoff_data.ML Tools/Qelim/generated_cooper.ML \
886655a150f6 moved quantifier elimination tools to Tools/Qelim/; wenzelm parents: 23462 diff changeset	111	Tools/Qelim/presburger.ML Tools/Qelim/qelim.ML \
23454 c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL; wenzelm parents: 23449 diff changeset	112	Tools/TFL/dcterm.ML Tools/TFL/post.ML Tools/TFL/rules.ML \
c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL; wenzelm parents: 23449 diff changeset	113	Tools/TFL/tfl.ML Tools/TFL/thms.ML Tools/TFL/thry.ML \
c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL; wenzelm parents: 23449 diff changeset	114	Tools/TFL/usyntax.ML Tools/TFL/utils.ML Tools/cnf_funcs.ML \
c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL; wenzelm parents: 23449 diff changeset	115	Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL; wenzelm parents: 23449 diff changeset	116	Tools/datatype_case.ML Tools/datatype_codegen.ML \
24626 85eceef2edc7 introduced generic concepts for theory interpretators haftmann parents: 24625 diff changeset	117	Tools/datatype_package.ML \
23454 c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL; wenzelm parents: 23449 diff changeset	118	Tools/datatype_prop.ML Tools/datatype_realizer.ML \
24625 0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML haftmann parents: 24616 diff changeset	119	Tools/datatype_rep_proofs.ML Tools/dseq.ML \
0398a5e802d3 separated code for inductive sequences from inductive_codegen.ML haftmann parents: 24616 diff changeset	120	Tools/function_package/auto_term.ML \
23194 085fa3def13b tuned webertj parents: 23193 diff changeset	121	Tools/function_package/context_tree.ML \
085fa3def13b tuned webertj parents: 23193 diff changeset	122	Tools/function_package/fundef_common.ML \
085fa3def13b tuned webertj parents: 23193 diff changeset	123	Tools/function_package/fundef_core.ML \
085fa3def13b tuned webertj parents: 23193 diff changeset	124	Tools/function_package/fundef_datatype.ML \
085fa3def13b tuned webertj parents: 23193 diff changeset	125	Tools/function_package/fundef_lib.ML \
085fa3def13b tuned webertj parents: 23193 diff changeset	126	Tools/function_package/fundef_package.ML \
085fa3def13b tuned webertj parents: 23193 diff changeset	127	Tools/function_package/inductive_wrap.ML \
085fa3def13b tuned webertj parents: 23193 diff changeset	128	Tools/function_package/lexicographic_order.ML \
085fa3def13b tuned webertj parents: 23193 diff changeset	129	Tools/function_package/mutual.ML \
24699 c6674504103f datatype interpretators for size and datatype_realizer haftmann parents: 24633 diff changeset	130	Tools/function_package/pattern_split.ML \
c6674504103f datatype interpretators for size and datatype_realizer haftmann parents: 24633 diff changeset	131	Tools/function_package/size.ML Tools/inductive_codegen.ML \
23734 0e11b904b3a3 Added new package for inductive sets. berghofe parents: 23666 diff changeset	132	Tools/inductive_package.ML Tools/inductive_realizer.ML \
24091 109f19a13872 added Tools/lin_arith.ML; wenzelm parents: 24082 diff changeset	133	Tools/inductive_set_package.ML Tools/lin_arith.ML Tools/meson.ML \
23574 42765aff66d6 added Tools/numeral.ML; wenzelm parents: 23549 diff changeset	134	Tools/metis_tools.ML Tools/numeral.ML Tools/numeral_syntax.ML \
25557 ea6b11021e79 added new primrec package haftmann parents: 25543 diff changeset	135	Tools/old_primrec_package.ML \
23734 0e11b904b3a3 Added new package for inductive sets. berghofe parents: 23666 diff changeset	136	Tools/polyhash.ML Tools/primrec_package.ML Tools/prop_logic.ML \
23454 c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL; wenzelm parents: 23449 diff changeset	137	Tools/recdef_package.ML Tools/recfun_codegen.ML \
c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL; wenzelm parents: 23449 diff changeset	138	Tools/record_package.ML Tools/refute.ML Tools/refute_isar.ML \
c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL; wenzelm parents: 23449 diff changeset	139	Tools/res_atp.ML Tools/res_atp_methods.ML Tools/res_atp_provers.ML \
24036 936cc23a3472 removed obsolete Tools/res_atpset.ML; wenzelm parents: 23882 diff changeset	140	Tools/res_axioms.ML Tools/res_clause.ML Tools/res_hol_clause.ML \
936cc23a3472 removed obsolete Tools/res_atpset.ML; wenzelm parents: 23882 diff changeset	141	Tools/res_reconstruct.ML Tools/rewrite_hol_proof.ML \
936cc23a3472 removed obsolete Tools/res_atpset.ML; wenzelm parents: 23882 diff changeset	142	Tools/sat_funcs.ML Tools/sat_solver.ML Tools/specification_package.ML \
936cc23a3472 removed obsolete Tools/res_atpset.ML; wenzelm parents: 23882 diff changeset	143	Tools/split_rule.ML Tools/string_syntax.ML Tools/typecopy_package.ML \
23194 085fa3def13b tuned webertj parents: 23193 diff changeset	144	Tools/typedef_codegen.ML Tools/typedef_package.ML \
26748 4d51ddd6aa5c Merged theories about wellfoundedness into one: Wellfounded.thy krauss parents: 26737 diff changeset	145	Transitive_Closure.thy Typedef.thy Wellfounded.thy \
4d51ddd6aa5c Merged theories about wellfoundedness into one: Wellfounded.thy krauss parents: 26737 diff changeset	146	arith_data.ML document/root.tex hologic.ML \
23164 69e55066dbca moved Integ files to canonical place; wenzelm parents: 23150 diff changeset	147	int_arith1.ML int_factor_simprocs.ML nat_simprocs.ML simpdata.ML
16187 6ec757011ad6 renamed HOL_PROOF_OBJECTS to HOL_USEDIR_OPTIONS; wenzelm parents: 16090 diff changeset	148	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	149
13029 84e4ba7fb033 added HOL-Hyperreal-ex; wenzelm parents: 13019 diff changeset	150
13967 9cdab3186c0b fixed HOL-Real-HahnBanach (-> HOL-Complex-HahnBanach) kleing parents: 13966 diff changeset	151	## HOL-Complex-HahnBanach
13029 84e4ba7fb033 added HOL-Hyperreal-ex; wenzelm parents: 13019 diff changeset	152
13967 9cdab3186c0b fixed HOL-Real-HahnBanach (-> HOL-Complex-HahnBanach) kleing parents: 13966 diff changeset	153	HOL-Complex-HahnBanach: HOL-Complex $(LOG)/HOL-Complex-HahnBanach.gz
13029 84e4ba7fb033 added HOL-Hyperreal-ex; wenzelm parents: 13019 diff changeset	154
16019 0e1405402d53 Simplifier already setup in Pure; wenzelm parents: 15871 diff changeset	155	$(LOG)/HOL-Complex-HahnBanach.gz: $(OUT)/HOL-Complex \
0e1405402d53 Simplifier already setup in Pure; wenzelm parents: 15871 diff changeset	156	Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy \
0e1405402d53 Simplifier already setup in Pure; wenzelm parents: 15871 diff changeset	157	Real/HahnBanach/FunctionOrder.thy Real/HahnBanach/HahnBanach.thy \
0e1405402d53 Simplifier already setup in Pure; wenzelm parents: 15871 diff changeset	158	Real/HahnBanach/HahnBanachExtLemmas.thy \
0e1405402d53 Simplifier already setup in Pure; wenzelm parents: 15871 diff changeset	159	Real/HahnBanach/HahnBanachSupLemmas.thy \
0e1405402d53 Simplifier already setup in Pure; wenzelm parents: 15871 diff changeset	160	Real/HahnBanach/Linearform.thy Real/HahnBanach/NormedSpace.thy \
0e1405402d53 Simplifier already setup in Pure; wenzelm parents: 15871 diff changeset	161	Real/HahnBanach/README.html Real/HahnBanach/ROOT.ML \
0e1405402d53 Simplifier already setup in Pure; wenzelm parents: 15871 diff changeset	162	Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy \
0e1405402d53 Simplifier already setup in Pure; wenzelm parents: 15871 diff changeset	163	Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/root.bib \
13029 84e4ba7fb033 added HOL-Hyperreal-ex; wenzelm parents: 13019 diff changeset	164	Real/HahnBanach/document/root.tex
13966 2160abf7cfe7 removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex paulson parents: 13964 diff changeset	165	@cd Real; $(ISATOOL) usedir -g true $(OUT)/HOL-Complex HahnBanach
13029 84e4ba7fb033 added HOL-Hyperreal-ex; wenzelm parents: 13019 diff changeset	166
84e4ba7fb033 added HOL-Hyperreal-ex; wenzelm parents: 13019 diff changeset	167
13961 233dd3bb2390 new directory Complex paulson parents: 13949 diff changeset	168	## HOL-Complex
10751 a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: 10732 diff changeset	169
13966 2160abf7cfe7 removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex paulson parents: 13964 diff changeset	170	HOL-Complex: HOL $(OUT)/HOL-Complex
10751 a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: 10732 diff changeset	171
23247 b99dce43d252 merged Code_Generator.thy into HOL.thy haftmann parents: 23243 diff changeset	172	$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML $(SRC)/Tools/float.ML \
26271 e324f8918c98 Added lemmas nipkow parents: 26265 diff changeset	173	Library/Zorn.thy Library/Order_Relation.thy \
23454 c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL; wenzelm parents: 23449 diff changeset	174	Real/ContNotDenum.thy Real/float_arith.ML Real/Float.thy \
24103 c13243a11e37 removed obsolete HOL/Real/ROOT.ML; wenzelm parents: 24091 diff changeset	175	Real/Lubs.thy Real/PReal.thy Real/RComplete.thy \
23454 c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL; wenzelm parents: 23449 diff changeset	176	Real/Rational.thy Real/Real.thy Real/RealDef.thy Real/RealPow.thy \
c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL; wenzelm parents: 23449 diff changeset	177	Real/RealVector.thy Real/rat_arith.ML Real/real_arith.ML \
25600 73431bd8c4c4 joined EvenOdd theory with Parity haftmann parents: 25568 diff changeset	178	Hyperreal/StarDef.thy \
73431bd8c4c4 joined EvenOdd theory with Parity haftmann parents: 25568 diff changeset	179	Hyperreal/Fact.thy Hyperreal/HLog.thy \
23194 085fa3def13b tuned webertj parents: 23193 diff changeset	180	Hyperreal/Filter.thy Hyperreal/HSeries.thy Hyperreal/transfer.ML \
085fa3def13b tuned webertj parents: 23193 diff changeset	181	Hyperreal/HLim.thy Hyperreal/HSEQ.thy Hyperreal/HTranscendental.thy \
085fa3def13b tuned webertj parents: 23193 diff changeset	182	Hyperreal/HDeriv.thy Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy \
085fa3def13b tuned webertj parents: 23193 diff changeset	183	Hyperreal/Hyperreal.thy \
085fa3def13b tuned webertj parents: 23193 diff changeset	184	Hyperreal/Integration.thy Hyperreal/Lim.thy Hyperreal/Log.thy \
085fa3def13b tuned webertj parents: 23193 diff changeset	185	Hyperreal/Ln.thy Hyperreal/MacLaurin.thy Hyperreal/NatStar.thy \
26116 159afd21502f Included theories Library/Univ_Poly.thy and Complex/Fundamental_Theorem_Algebra.thy ; Theory Hyperreal/Poly.thy Removed chaieb parents: 26103 diff changeset	186	Hyperreal/NSA.thy Hyperreal/NthRoot.thy Library/Univ_Poly.thy \
23194 085fa3def13b tuned webertj parents: 23193 diff changeset	187	Hyperreal/SEQ.thy Hyperreal/Series.thy Hyperreal/Star.thy \
085fa3def13b tuned webertj parents: 23193 diff changeset	188	Hyperreal/Taylor.thy Hyperreal/FrechetDeriv.thy Hyperreal/Deriv.thy \
085fa3def13b tuned webertj parents: 23193 diff changeset	189	Hyperreal/Transcendental.thy Hyperreal/hypreal_arith.ML \
26116 159afd21502f Included theories Library/Univ_Poly.thy and Complex/Fundamental_Theorem_Algebra.thy ; Theory Hyperreal/Poly.thy Removed chaieb parents: 26103 diff changeset	190	Complex/Complex_Main.thy Complex/Fundamental_Theorem_Algebra.thy \
159afd21502f Included theories Library/Univ_Poly.thy and Complex/Fundamental_Theorem_Algebra.thy ; Theory Hyperreal/Poly.thy Removed chaieb parents: 26103 diff changeset	191	Complex/CLim.thy \
23194 085fa3def13b tuned webertj parents: 23193 diff changeset	192	Complex/CStar.thy Complex/Complex.thy Complex/NSCA.thy \
085fa3def13b tuned webertj parents: 23193 diff changeset	193	Complex/NSComplex.thy \
22897 c714f6d0a8d7 removed Complex/ComplexBin.thy; wenzelm parents: 22839 diff changeset	194	Complex/document/root.tex Library/Infinite_Set.thy Library/Parity.thy
15057 b1a368d93c50 added Complex/root nipkow parents: 15037 diff changeset	195	@cd Complex; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Complex
10751 a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real paulson parents: 10732 diff changeset	196
7395 66a3d3bb28e4 clean: include HOL-Real-ex; wenzelm parents: 7393 diff changeset	197
13961 233dd3bb2390 new directory Complex paulson parents: 13949 diff changeset	198	## HOL-Complex-ex
7392 4137c951b36b new directory HOL/Real/ex of real examples paulson parents: 7383 diff changeset	199
13961 233dd3bb2390 new directory Complex paulson parents: 13949 diff changeset	200	HOL-Complex-ex: HOL-Complex $(LOG)/HOL-Complex-ex.gz
7535 599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar) wenzelm parents: 7513 diff changeset	201
13961 233dd3bb2390 new directory Complex paulson parents: 13949 diff changeset	202	$(LOG)/HOL-Complex-ex.gz: $(OUT)/HOL-Complex Library/Primes.thy \
233dd3bb2390 new directory Complex paulson parents: 13949 diff changeset	203	Complex/ex/ROOT.ML Complex/ex/document/root.tex \
23194 085fa3def13b tuned webertj parents: 23193 diff changeset	204	Complex/ex/BigO_Complex.thy Complex/ex/BinEx.thy \
23265 a6992b91fdde Added two examples in Complex/ex :Reflected QE for linear real arith and QE for mixed integer real linear arithmetic chaieb parents: 23252 diff changeset	205	Complex/ex/NSPrimes.thy Complex/ex/Sqrt.thy Complex/ex/Sqrt_Script.thy \
a6992b91fdde Added two examples in Complex/ex :Reflected QE for linear real arith and QE for mixed integer real linear arithmetic chaieb parents: 23252 diff changeset	206	Complex/ex/MIR.thy Complex/ex/mirtac.ML Complex/ex/mireif.ML \
a6992b91fdde Added two examples in Complex/ex :Reflected QE for linear real arith and QE for mixed integer real linear arithmetic chaieb parents: 23252 diff changeset	207	Complex/ex/ReflectedFerrack.thy Complex/ex/linreif.ML Complex/ex/linrtac.ML
13961 233dd3bb2390 new directory Complex paulson parents: 13949 diff changeset	208	@cd Complex; $(ISATOOL) usedir $(OUT)/HOL-Complex ex
7535 599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar) wenzelm parents: 7513 diff changeset	209
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar) wenzelm parents: 7513 diff changeset	210
10255 bb66874b4750 added HOL/Library, rearranged several files; wenzelm parents: 10214 diff changeset	211	## HOL-Library
bb66874b4750 added HOL/Library, rearranged several files; wenzelm parents: 10214 diff changeset	212
bb66874b4750 added HOL/Library, rearranged several files; wenzelm parents: 10214 diff changeset	213	HOL-Library: HOL $(LOG)/HOL-Library.gz
bb66874b4750 added HOL/Library, rearranged several files; wenzelm parents: 10214 diff changeset	214
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: 19499 diff changeset	215	$(LOG)/HOL-Library.gz: $(OUT)/HOL \
19944 60e0cbeae3d8 Introduction of Ramsey's theorem paulson parents: 19839 diff changeset	216	Library/SetsAndFunctions.thy Library/BigO.thy Library/Ramsey.thy \
23854 688a8a7bcd4e uniform naming conventions for CG theories haftmann parents: 23772 diff changeset	217	Library/Efficient_Nat.thy Library/Executable_Set.thy \
26155 7c265e3da23c HOL/Dense_Linear_Order.thy moved to Library ; resulting dependencies updated chaieb parents: 26127 diff changeset	218	Library/Infinite_Set.thy Library/Dense_Linear_Order.thy\
23192 ec73b9707d48 Moved list comprehension into List nipkow parents: 23172 diff changeset	219	Library/FuncSet.thy Library/Library.thy \
23194 085fa3def13b tuned webertj parents: 23193 diff changeset	220	Library/List_Prefix.thy Library/State_Monad.thy Library/Multiset.thy \
26127 70ef56eb650a Added dependency of Library on Pocklington.thy chaieb parents: 26116 diff changeset	221	Library/NatPair.thy Library/Permutation.thy \
70ef56eb650a Added dependency of Library on Pocklington.thy chaieb parents: 26116 diff changeset	222	Library/Primes.thy Library/Pocklington.thy Library/Quotient.thy \
24616 fac3dd4ade83 sorting nipkow parents: 24607 diff changeset	223	Library/Quicksort.thy Library/Nat_Infinity.thy Library/Word.thy \
11349 fcb507c945c3 added Library/Nat_Infinity.thy and Library/Continuity.thy oheimb parents: 11287 diff changeset	224	Library/README.html Library/Continuity.thy \
14365 3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development paulson parents: 14355 diff changeset	225	Library/Nested_Environment.thy Library/Zorn.thy\
12816 668073849ca9 fixed document setup of HOL-Library; wenzelm parents: 12793 diff changeset	226	Library/Library/ROOT.ML Library/Library/document/root.tex \
15731 29ae73d8a84e Removed dir Orderings in Library nipkow parents: 15697 diff changeset	227	Library/Library/document/root.bib Library/While_Combinator.thy \
22799 ed7d53db2170 moved code generation pretty integers and characters to separate theories haftmann parents: 22784 diff changeset	228	Library/Product_ord.thy Library/Char_nat.thy Library/Char_ord.thy \
26735 39be3c7e643a added theory Sublist_Order haftmann parents: 26688 diff changeset	229	Library/Option_ord.thy Library/Sublist_Order.thy \
18397 2d94eb7ff17f added HOL/Library/Coinductive_List.thy; wenzelm parents: 18005 diff changeset	230	Library/List_lexord.thy Library/Commutative_Ring.thy Library/comm_ring.ML \
21256 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 21254 diff changeset	231	Library/Coinductive_List.thy Library/AssocList.thy \
22359 94a794672c8b Added formalization of size-change principle (experimental). krauss parents: 22327 diff changeset	232	Library/Parity.thy Library/GCD.thy Library/Binomial.thy \
25763 474f8ba9dfa9 improved evaluation mechanism haftmann parents: 25728 diff changeset	233	Library/Eval.thy Library/Eval_Witness.thy \
24994 c385c4eabb3b consolidated naming conventions for code generator theories haftmann parents: 24915 diff changeset	234	Library/Code_Index.thy Library/Code_Char.thy Library/Code_Char_chr.thy \
c385c4eabb3b consolidated naming conventions for code generator theories haftmann parents: 24915 diff changeset	235	Library/Code_Integer.thy Library/Code_Message.thy \
26116 159afd21502f Included theories Library/Univ_Poly.thy and Complex/Fundamental_Theorem_Algebra.thy ; Theory Hyperreal/Poly.thy Removed chaieb parents: 26103 diff changeset	236	Library/Abstract_Rat.thy Library/Univ_Poly.thy\
26170 66e6b967ccf1 added theories for imperative HOL haftmann parents: 26155 diff changeset	237	Library/Numeral_Type.thy Library/Boolean_Algebra.thy Library/Countable.thy \
66e6b967ccf1 added theories for imperative HOL haftmann parents: 26155 diff changeset	238	Library/RType.thy Library/Heap.thy Library/Heap_Monad.thy Library/Array.thy \
26348 0f8e23edd357 added theory Library/Enum.thy haftmann parents: 26271 diff changeset	239	Library/Ref.thy Library/Imperative_HOL.thy Library/RBT.thy Library/Enum.thy
11398 d7711be8c3a9 Library/ROOT.ML moved to Library/Library/ROOT.ML to avoid accidential wenzelm parents: 11394 diff changeset	240	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
10255 bb66874b4750 added HOL/Library, rearranged several files; wenzelm parents: 10214 diff changeset	241
bb66874b4750 added HOL/Library, rearranged several files; wenzelm parents: 10214 diff changeset	242
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	243	## HOL-Subst
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	244
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	245	HOL-Subst: HOL $(LOG)/HOL-Subst.gz
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	246
15635 8408a06590a6 converted HOL-Subst to tactic scripts paulson parents: 15622 diff changeset	247	$(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.thy \
8408a06590a6 converted HOL-Subst to tactic scripts paulson parents: 15622 diff changeset	248	Subst/ROOT.ML Subst/Subst.thy Subst/UTerm.thy Subst/Unifier.thy \
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	249	Subst/Unify.thy
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	250	@$(ISATOOL) usedir $(OUT)/HOL Subst
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	251
61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	252
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	253	## HOL-Induct
2473 3eb12c85846c minor tuning; wenzelm parents: 2448 diff changeset	254
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	255	HOL-Induct: HOL $(LOG)/HOL-Induct.gz
3125 3f0ab2c306f7 Moved induction examples to directory Induct paulson parents: 3118 diff changeset	256
10255 bb66874b4750 added HOL/Library, rearranged several files; wenzelm parents: 10214 diff changeset	257	$(LOG)/HOL-Induct.gz: $(OUT)/HOL \
24616 fac3dd4ade83 sorting nipkow parents: 24607 diff changeset	258	Induct/Com.thy Induct/Comb.thy Induct/LFilter.thy \
13075 d3e1d554cd6d conversion of some HOL/Induct proof scripts to Isar paulson parents: 13059 diff changeset	259	Induct/LList.thy Induct/Mutil.thy Induct/Ordinals.thy \
15172 73069e033a0b new example of a quotiented nested data type paulson parents: 15150 diff changeset	260	Induct/PropLog.thy Induct/QuoNestedDataType.thy Induct/QuoDataType.thy\
73069e033a0b new example of a quotiented nested data type paulson parents: 15150 diff changeset	261	Induct/ROOT.ML \
13079 e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts paulson parents: 13075 diff changeset	262	Induct/Sexp.thy Induct/Sigma_Algebra.thy \
e7738aa7267f conversion of Induct/{Slist,Sexp} to Isar scripts paulson parents: 13075 diff changeset	263	Induct/SList.thy Induct/ABexp.thy Induct/Term.thy \
11046 b5f5942781a0 Induct: converted some theories to new-style format; wenzelm parents: 11026 diff changeset	264	Induct/Tree.thy Induct/document/root.tex
3125 3f0ab2c306f7 Moved induction examples to directory Induct paulson parents: 3118 diff changeset	265	@$(ISATOOL) usedir $(OUT)/HOL Induct
3f0ab2c306f7 Moved induction examples to directory Induct paulson parents: 3118 diff changeset	266
3f0ab2c306f7 Moved induction examples to directory Induct paulson parents: 3118 diff changeset	267
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	268	## HOL-IMP
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	269
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	270	HOL-IMP: HOL $(LOG)/HOL-IMP.gz
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	271
13129 bb448fb75191 added dep on IMP/Compiler0 nipkow parents: 13117 diff changeset	272	$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Compiler0.thy IMP/Compiler.thy \
12432 90b0fc84f8d9 HOL/IMP converted to Isar kleing parents: 12410 diff changeset	273	IMP/Denotation.thy IMP/Expr.thy IMP/Hoare.thy \
90b0fc84f8d9 HOL/IMP converted to Isar kleing parents: 12410 diff changeset	274	IMP/Natural.thy IMP/Examples.thy \
90b0fc84f8d9 HOL/IMP converted to Isar kleing parents: 12410 diff changeset	275	IMP/Transition.thy IMP/VC.thy IMP/ROOT.ML IMP/document/root.tex \
90b0fc84f8d9 HOL/IMP converted to Isar kleing parents: 12410 diff changeset	276	IMP/document/root.bib
12548 9d247ad51c81 HOL/IMP: include session graph; wenzelm parents: 12521 diff changeset	277	@$(ISATOOL) usedir -g true $(OUT)/HOL IMP
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	278
61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	279
8179 6a0b1037bab3 added forgotten rules to make IMPP oheimb parents: 8177 diff changeset	280	## HOL-IMPP
6a0b1037bab3 added forgotten rules to make IMPP oheimb parents: 8177 diff changeset	281
6a0b1037bab3 added forgotten rules to make IMPP oheimb parents: 8177 diff changeset	282	HOL-IMPP: HOL $(LOG)/HOL-IMPP.gz
6a0b1037bab3 added forgotten rules to make IMPP oheimb parents: 8177 diff changeset	283
19803 aa2581752afb removed obsolete ML files; wenzelm parents: 19802 diff changeset	284	$(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy \
aa2581752afb removed obsolete ML files; wenzelm parents: 19802 diff changeset	285	IMPP/Natural.thy IMPP/Hoare.thy IMPP/Misc.thy IMPP/EvenOdd.thy
8179 6a0b1037bab3 added forgotten rules to make IMPP oheimb parents: 8177 diff changeset	286	@$(ISATOOL) usedir $(OUT)/HOL IMPP
6a0b1037bab3 added forgotten rules to make IMPP oheimb parents: 8177 diff changeset	287
6a0b1037bab3 added forgotten rules to make IMPP oheimb parents: 8177 diff changeset	288
14516 a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	289	## HOL-Complex-Import
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	290
19097 2fc1a6da9366 removed Import/lazy_scan.ML; wenzelm parents: 19085 diff changeset	291	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	292	Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \
14516 a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	293	Import/HOL4Syntax.thy Import/HOL4Compat.thy Import/import_syntax.ML \
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	294	Import/hol4rews.ML Import/import_package.ML Import/ROOT.ML
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	295
17323 2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight obua parents: 17308 diff changeset	296	IMPORTER_HOLLIGHT_FILES = Import/proof_kernel.ML Import/replay.ML \
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight obua parents: 17308 diff changeset	297	Import/shuffler.ML Import/MakeEqual.thy Import/HOL4Setup.thy \
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight obua parents: 17308 diff changeset	298	Import/HOL4Syntax.thy Import/HOLLightCompat.thy Import/import_syntax.ML \
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight obua parents: 17308 diff changeset	299	Import/hol4rews.ML Import/import_package.ML Import/ROOT.ML
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight obua parents: 17308 diff changeset	300
14516 a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	301	HOL-Complex-Import: HOL-Complex $(LOG)/HOL-Complex-Import.gz
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	302
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	303	$(LOG)/HOL-Complex-Import.gz: $(OUT)/HOL-Complex $(IMPORTER_FILES)
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	304	@$(ISATOOL) usedir $(OUT)/HOL-Complex Import
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	305
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	306
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	307	## HOL-Complex-Generate-HOL
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	308
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	309	HOL-Complex-Generate-HOL: HOL-Complex $(LOG)/HOL-Complex-Generate-HOL.gz
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	310
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	311	$(LOG)/HOL-Complex-Generate-HOL.gz: $(OUT)/HOL-Complex $(IMPORTER_FILES) \
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	312	Import/Generate-HOL/GenHOL4Base.thy Import/Generate-HOL/GenHOL4Prob.thy \
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	313	Import/Generate-HOL/GenHOL4Real.thy Import/Generate-HOL/GenHOL4Vec.thy \
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	314	Import/Generate-HOL/GenHOL4Word32.thy Import/Generate-HOL/ROOT.ML
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	315	@cd Import; $(ISATOOL) usedir $(OUT)/HOL-Complex Generate-HOL
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	316
17460 7780d953598c generate: added HOL-Complex-Generate-HOLLight; wenzelm parents: 17430 diff changeset	317
7780d953598c generate: added HOL-Complex-Generate-HOLLight; wenzelm parents: 17430 diff changeset	318	## HOL-Complex-Generate-HOLLight
7780d953598c generate: added HOL-Complex-Generate-HOLLight; wenzelm parents: 17430 diff changeset	319
17323 2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight obua parents: 17308 diff changeset	320	HOL-Complex-Generate-HOLLight: HOL-Complex $(LOG)/HOL-Complex-Generate-HOLLight.gz
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight obua parents: 17308 diff changeset	321
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight obua parents: 17308 diff changeset	322	$(LOG)/HOL-Complex-Generate-HOLLight.gz: $(OUT)/HOL-Complex $(IMPORTER_HOLLIGHT_FILES) \
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight obua parents: 17308 diff changeset	323	Import/Generate-HOLLight/GenHOLLight.thy Import/Generate-HOLLight/ROOT.ML
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight obua parents: 17308 diff changeset	324	@cd Import; $(ISATOOL) usedir $(OUT)/HOL-Complex Generate-HOLLight
14516 a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	325
17460 7780d953598c generate: added HOL-Complex-Generate-HOLLight; wenzelm parents: 17430 diff changeset	326
14516 a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	327	## HOL-Import-HOL
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	328
14626 dfb8d2977263 renamed HOL-Import-HOL to HOL4, added to images target kleing parents: 14610 diff changeset	329	HOL4: HOL-Complex $(LOG)/HOL4.gz
14516 a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	330
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	331	HOL_IMPORT_FILES = arithmetic.imp bits.imp boolean_sequence.imp bool.imp \
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	332	bword_arith.imp bword_bitop.imp bword_num.imp combin.imp divides.imp \
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	333	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	334	numeral.imp num.imp one.imp operator.imp option.imp pair.imp poly.imp \
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	335	powser.imp pred_set.imp prime.imp prim_rec.imp prob_algebra.imp \
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	336	prob_canon.imp prob_extra.imp prob.imp prob_indep.imp prob_pseudo.imp \
23194 085fa3def13b tuned webertj parents: 23193 diff changeset	337	prob_uniform.imp realax.imp real.imp relation.imp res_quan.imp \
085fa3def13b tuned webertj parents: 23193 diff changeset	338	rich_list.imp \
14516 a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	339	seq.imp state_transformer.imp sum.imp topology.imp transc.imp word32.imp \
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	340	word_base.imp word_bitop.imp word_num.imp
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	341
14626 dfb8d2977263 renamed HOL-Import-HOL to HOL4, added to images target kleing parents: 14610 diff changeset	342	$(LOG)/HOL4.gz: $(OUT)/HOL-Complex $(IMPORTER_FILES) \
14516 a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	343	$(HOL_IMPORT_FILES:%=Import/HOL/%) Import/HOL/HOL4Base.thy \
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	344	Import/HOL/HOL4Prob.thy Import/HOL/HOL4Real.thy Import/HOL/HOL4Vec.thy \
a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	345	Import/HOL/HOL4Word32.thy Import/HOL/HOL4.thy Import/HOL/ROOT.ML
14626 dfb8d2977263 renamed HOL-Import-HOL to HOL4, added to images target kleing parents: 14610 diff changeset	346	@cd Import/HOL; $(ISATOOL) usedir -b $(OUT)/HOL-Complex HOL4
14516 a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	347
17645 940371ea0ff3 added entry for running HOLLight obua parents: 17637 diff changeset	348	HOLLight: HOL-Complex $(LOG)/HOLLight.gz
940371ea0ff3 added entry for running HOLLight obua parents: 17637 diff changeset	349
940371ea0ff3 added entry for running HOLLight obua parents: 17637 diff changeset	350	$(LOG)/HOLLight.gz: $(OUT)/HOL-Complex $(IMPORTER_HOLLIGHT_FILES) \
940371ea0ff3 added entry for running HOLLight obua parents: 17637 diff changeset	351	Import/HOLLight/hollight.imp Import/HOLLight/HOLLight.thy \
940371ea0ff3 added entry for running HOLLight obua parents: 17637 diff changeset	352	Import/HOLLight/ROOT.ML
940371ea0ff3 added entry for running HOLLight obua parents: 17637 diff changeset	353	@cd Import/HOLLight; $(ISATOOL) usedir -b $(OUT)/HOL-Complex HOLLight
940371ea0ff3 added entry for running HOLLight obua parents: 17637 diff changeset	354
14516 a183dec876ab Added HOL proof importer. skalberg parents: 14515 diff changeset	355
9510 dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied paulson parents: 9481 diff changeset	356	## HOL-NumberTheory
dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied paulson parents: 9481 diff changeset	357
dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied paulson parents: 9481 diff changeset	358	HOL-NumberTheory: HOL $(LOG)/HOL-NumberTheory.gz
dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied paulson parents: 9481 diff changeset	359
dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied paulson parents: 9481 diff changeset	360	$(LOG)/HOL-NumberTheory.gz: $(OUT)/HOL \
11363 a548865b1b6a moved Primes.thy from NumberTheory to Library paulson parents: 11362 diff changeset	361	Library/Permutation.thy Library/Primes.thy NumberTheory/Fib.thy \
11049 7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 11046 diff changeset	362	NumberTheory/Factorization.thy NumberTheory/BijectionRel.thy \
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 11046 diff changeset	363	NumberTheory/Chinese.thy NumberTheory/EulerFermat.thy \
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 11046 diff changeset	364	NumberTheory/IntFact.thy NumberTheory/IntPrimes.thy \
7eef34adb852 HOL-NumberTheory: converted to new-style format and proper document setup; wenzelm parents: 11046 diff changeset	365	NumberTheory/WilsonBij.thy NumberTheory/WilsonRuss.thy \
13873 f9f49a1ec0f2 quadratic reciprocity files paulson parents: 13870 diff changeset	366	NumberTheory/Finite2.thy NumberTheory/Int2.thy NumberTheory/EvenOdd.thy\
f9f49a1ec0f2 quadratic reciprocity files paulson parents: 13870 diff changeset	367	NumberTheory/Residues.thy NumberTheory/Euler.thy NumberTheory/Gauss.thy\
20808 96d413f78870 moved Infinite_Set.thy to Library; wenzelm parents: 20787 diff changeset	368	NumberTheory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy\
9510 dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied paulson parents: 9481 diff changeset	369	NumberTheory/ROOT.ML
11850 cdfc3fce577e document graphs for several sessions; wenzelm parents: 11837 diff changeset	370	@$(ISATOOL) usedir -g true $(OUT)/HOL NumberTheory
9510 dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied paulson parents: 9481 diff changeset	371
dbcb1a6c92e1 new files Integ/IntPower.{thy.ML}; tidied paulson parents: 9481 diff changeset	372
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	373	## HOL-Hoare
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	374
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	375	HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	376
19802 c2860c37e574 removed obsolete ML files; wenzelm parents: 19801 diff changeset	377	$(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.thy \
24472 943ef707396c added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy); wenzelm parents: 24470 diff changeset	378	Hoare/Examples.thy Hoare/Hoare.thy Hoare/hoare_tac.ML \
13875 12997e3ddd8d * empty log message * nipkow parents: 13873 diff changeset	379	Hoare/Heap.thy Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy \
12997e3ddd8d * empty log message * nipkow parents: 13873 diff changeset	380	Hoare/ROOT.ML Hoare/ExamplesAbort.thy Hoare/HeapSyntaxAbort.thy \
24470 41c81e23c08d removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system); wenzelm parents: 24465 diff changeset	381	Hoare/HoareAbort.thy Hoare/SchorrWaite.thy \
19402 742b7934ccfc Hoare(Parallel) dependencies on document/* nipkow parents: 19234 diff changeset	382	Hoare/Separation.thy Hoare/SepLogHeap.thy \
742b7934ccfc Hoare(Parallel) dependencies on document/* nipkow parents: 19234 diff changeset	383	Hoare/document/root.tex Hoare/document/root.bib
2826 0b0d9e3bc661 isatool usedir; wenzelm parents: 2635 diff changeset	384	@$(ISATOOL) usedir $(OUT)/HOL Hoare
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	385
61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	386
12996 7ac0a7e306db Completed annonce of HoareParallel prensani parents: 12951 diff changeset	387	## HOL-HoareParallel
7ac0a7e306db Completed annonce of HoareParallel prensani parents: 12951 diff changeset	388
7ac0a7e306db Completed annonce of HoareParallel prensani parents: 12951 diff changeset	389	HOL-HoareParallel: HOL $(LOG)/HOL-HoareParallel.gz
7ac0a7e306db Completed annonce of HoareParallel prensani parents: 12951 diff changeset	390
7ac0a7e306db Completed annonce of HoareParallel prensani parents: 12951 diff changeset	391	$(LOG)/HOL-HoareParallel.gz: $(OUT)/HOL HoareParallel/Gar_Coll.thy \
7ac0a7e306db Completed annonce of HoareParallel prensani parents: 12951 diff changeset	392	HoareParallel/Graph.thy HoareParallel/Mul_Gar_Coll.thy \
7ac0a7e306db Completed annonce of HoareParallel prensani parents: 12951 diff changeset	393	HoareParallel/OG_Com.thy HoareParallel/OG_Examples.thy \
7ac0a7e306db Completed annonce of HoareParallel prensani parents: 12951 diff changeset	394	HoareParallel/OG_Hoare.thy HoareParallel/OG_Syntax.thy \
7ac0a7e306db Completed annonce of HoareParallel prensani parents: 12951 diff changeset	395	HoareParallel/OG_Tactics.thy HoareParallel/OG_Tran.thy \
13019 98f0a09a33c3 Target HoareParallel in IsaMakefile prensani parents: 13004 diff changeset	396	HoareParallel/Quote_Antiquote.thy \
12996 7ac0a7e306db Completed annonce of HoareParallel prensani parents: 12951 diff changeset	397	HoareParallel/RG_Com.thy HoareParallel/RG_Examples.thy \
7ac0a7e306db Completed annonce of HoareParallel prensani parents: 12951 diff changeset	398	HoareParallel/RG_Hoare.thy HoareParallel/RG_Syntax.thy \
7ac0a7e306db Completed annonce of HoareParallel prensani parents: 12951 diff changeset	399	HoareParallel/RG_Tran.thy HoareParallel/ROOT.ML \
19402 742b7934ccfc Hoare(Parallel) dependencies on document/* nipkow parents: 19234 diff changeset	400	HoareParallel/document/root.tex HoareParallel/document/root.bib
13029 84e4ba7fb033 added HOL-Hyperreal-ex; wenzelm parents: 13019 diff changeset	401	@$(ISATOOL) usedir -g true $(OUT)/HOL HoareParallel
12996 7ac0a7e306db Completed annonce of HoareParallel prensani parents: 12951 diff changeset	402
7ac0a7e306db Completed annonce of HoareParallel prensani parents: 12951 diff changeset	403
23449 dd874e6a3282 integration of Metis prover paulson parents: 23445 diff changeset	404	## HOL-MetisExamples
dd874e6a3282 integration of Metis prover paulson parents: 23445 diff changeset	405
dd874e6a3282 integration of Metis prover paulson parents: 23445 diff changeset	406	HOL-MetisExamples: HOL $(LOG)/HOL-MetisExamples.gz
dd874e6a3282 integration of Metis prover paulson parents: 23445 diff changeset	407
dd874e6a3282 integration of Metis prover paulson parents: 23445 diff changeset	408	$(LOG)/HOL-MetisExamples.gz: $(OUT)/HOL \
dd874e6a3282 integration of Metis prover paulson parents: 23445 diff changeset	409	MetisExamples/ROOT.ML \
dd874e6a3282 integration of Metis prover paulson parents: 23445 diff changeset	410	MetisExamples/Abstraction.thy MetisExamples/BigO.thy MetisExamples/BT.thy \
dd874e6a3282 integration of Metis prover paulson parents: 23445 diff changeset	411	MetisExamples/Message.thy MetisExamples/Tarski.thy MetisExamples/TransClosure.thy \
dd874e6a3282 integration of Metis prover paulson parents: 23445 diff changeset	412	MetisExamples/set.thy
23454 c54975167be9 replaced Real/Ferrante-Rackoff tool by generic version in Main HOL; wenzelm parents: 23449 diff changeset	413	@$(ISATOOL) usedir $(OUT)/HOL MetisExamples
23449 dd874e6a3282 integration of Metis prover paulson parents: 23445 diff changeset	414
dd874e6a3282 integration of Metis prover paulson parents: 23445 diff changeset	415
7999 7acf6eb8eec1 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: 7985 diff changeset	416	## HOL-Algebra
7acf6eb8eec1 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: 7985 diff changeset	417
7acf6eb8eec1 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: 7985 diff changeset	418	HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz
7acf6eb8eec1 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: 7985 diff changeset	419
21423 6cdd0589aa73 HOL-Algebra: converted legacy ML scripts; wenzelm parents: 21317 diff changeset	420	$(LOG)/HOL-Algebra.gz: $(OUT)/HOL Algebra/ROOT.ML Library/Primes.thy \
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts; wenzelm parents: 21317 diff changeset	421	Library/FuncSet.thy Algebra/AbelCoset.thy Algebra/Bij.thy \
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts; wenzelm parents: 21317 diff changeset	422	Algebra/Coset.thy Algebra/Exponent.thy Algebra/FiniteProduct.thy \
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts; wenzelm parents: 21317 diff changeset	423	Algebra/Group.thy Algebra/Ideal.thy Algebra/IntRing.thy \
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts; wenzelm parents: 21317 diff changeset	424	Algebra/Lattice.thy Algebra/Module.thy Algebra/QuotRing.thy \
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts; wenzelm parents: 21317 diff changeset	425	Algebra/Ring.thy Algebra/RingHom.thy Algebra/Sylow.thy \
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts; wenzelm parents: 21317 diff changeset	426	Algebra/UnivPoly.thy Algebra/abstract/Abstract.thy \
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts; wenzelm parents: 21317 diff changeset	427	Algebra/abstract/Factor.thy Algebra/abstract/Field.thy \
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts; wenzelm parents: 21317 diff changeset	428	Algebra/abstract/Ideal2.thy Algebra/abstract/PID.thy \
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts; wenzelm parents: 21317 diff changeset	429	Algebra/abstract/Ring2.thy Algebra/abstract/RingHomo.thy \
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts; wenzelm parents: 21317 diff changeset	430	Algebra/document/root.tex Algebra/poly/LongDiv.thy \
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts; wenzelm parents: 21317 diff changeset	431	Algebra/poly/PolyHomo.thy Algebra/poly/Polynomial.thy \
6cdd0589aa73 HOL-Algebra: converted legacy ML scripts; wenzelm parents: 21317 diff changeset	432	Algebra/poly/UnivPoly2.thy Algebra/ringsimp.ML
14578 1f3f7e58b195 session graph; wenzelm parents: 14569 diff changeset	433	@cd Algebra; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Algebra
7999 7acf6eb8eec1 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: 7985 diff changeset	434
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	435	## HOL-Auth
3819 5a6a6f18b109 added TLA stuff; wenzelm parents: 3616 diff changeset	436
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	437	HOL-Auth: HOL $(LOG)/HOL-Auth.gz
3819 5a6a6f18b109 added TLA stuff; wenzelm parents: 3616 diff changeset	438
14132 4d682b249437 new theory Library/NatPair paulson parents: 14115 diff changeset	439	$(LOG)/HOL-Auth.gz: $(OUT)/HOL Library/NatPair.thy \
13926 6e62e5357a10 converting more HOL-Auth to new-style theories paulson parents: 13923 diff changeset	440	Auth/CertifiedEmail.thy Auth/Event.thy \
6e62e5357a10 converting more HOL-Auth to new-style theories paulson parents: 13923 diff changeset	441	Auth/Message.thy Auth/NS_Public.thy Auth/NS_Public_Bad.thy \
23194 085fa3def13b tuned webertj parents: 23193 diff changeset	442	Auth/NS_Shared.thy Auth/OtwayRees.thy Auth/OtwayReesBella.thy \
085fa3def13b tuned webertj parents: 23193 diff changeset	443	Auth/OtwayRees_AN.thy \
13923 019342d03d81 Auth: certified email protocol paulson parents: 13908 diff changeset	444	Auth/OtwayRees_Bad.thy Auth/Public.thy Auth/ROOT.ML \
13926 6e62e5357a10 converting more HOL-Auth to new-style theories paulson parents: 13923 diff changeset	445	Auth/Recur.thy Auth/Shared.thy \
23194 085fa3def13b tuned webertj parents: 23193 diff changeset	446	Auth/TLS.thy Auth/WooLam.thy Auth/Kerberos_BAN.thy \
085fa3def13b tuned webertj parents: 23193 diff changeset	447	Auth/Kerberos_BAN_Gets.thy \
18886 9f27383426db new and updated protocol proofs by Giamp Bella paulson parents: 18793 diff changeset	448	Auth/KerberosIV.thy Auth/KerberosIV_Gets.thy Auth/KerberosV.thy \
13508 890d736b93a5 Frederic Blanqui's new "guard" examples paulson parents: 13481 diff changeset	449	Auth/Yahalom.thy Auth/Yahalom2.thy Auth/Yahalom_Bad.thy \
14145 2e31b8cc8788 ZhouGollmann: new example (fair non-repudiation protocol) paulson parents: 14132 diff changeset	450	Auth/ZhouGollmann.thy \
13508 890d736b93a5 Frederic Blanqui's new "guard" examples paulson parents: 13481 diff changeset	451	Auth/Guard/Analz.thy Auth/Guard/Extensions.thy Auth/Guard/GuardK.thy \
890d736b93a5 Frederic Blanqui's new "guard" examples paulson parents: 13481 diff changeset	452	Auth/Guard/Guard_Public.thy Auth/Guard/Guard_Shared.thy \
890d736b93a5 Frederic Blanqui's new "guard" examples paulson parents: 13481 diff changeset	453	Auth/Guard/Guard.thy Auth/Guard/List_Msg.thy \
17394 a8c9ed3f9818 renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions; wenzelm parents: 17384 diff changeset	454	Auth/Guard/Guard_NS_Public.thy Auth/Guard/Guard_OtwayRees.thy \
13508 890d736b93a5 Frederic Blanqui's new "guard" examples paulson parents: 13481 diff changeset	455	Auth/Guard/P1.thy Auth/Guard/P2.thy \
23194 085fa3def13b tuned webertj parents: 23193 diff changeset	456	Auth/Guard/Proto.thy Auth/Guard/Guard_Yahalom.thy \
085fa3def13b tuned webertj parents: 23193 diff changeset	457	Auth/Smartcard/EventSC.thy Auth/Smartcard/ShoupRubinBella.thy \
085fa3def13b tuned webertj parents: 23193 diff changeset	458	Auth/Smartcard/ShoupRubin.thy Auth/Smartcard/Smartcard.thy \
23164 69e55066dbca moved Integ files to canonical place; wenzelm parents: 23150 diff changeset	459	Auth/document/root.tex
13964 bfca18e9ab72 fixed missing -g true for HOL-Auth kleing parents: 13961 diff changeset	460	@$(ISATOOL) usedir -g true $(OUT)/HOL Auth
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	461
61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	462
4777 379f32b0ae40 New target HOL-UNITY paulson parents: 4729 diff changeset	463	## HOL-UNITY
379f32b0ae40 New target HOL-UNITY paulson parents: 4729 diff changeset	464
379f32b0ae40 New target HOL-UNITY paulson parents: 4729 diff changeset	465	HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz
379f32b0ae40 New target HOL-UNITY paulson parents: 4729 diff changeset	466
10787 f42353afd6d3 new UNITY examples by Sidi Ehmety paulson parents: 10772 diff changeset	467	$(LOG)/HOL-UNITY.gz: $(OUT)/HOL Library/Multiset.thy UNITY/ROOT.ML \
13790 8d7e9fce8c50 converting UNITY to new-style theories paulson parents: 13787 diff changeset	468	UNITY/UNITY_Main.thy UNITY/UNITY_tactics.ML \
13797 baefae13ad37 conversion of UNITY theories to new-style paulson parents: 13796 diff changeset	469	UNITY/Comp.thy UNITY/Constrains.thy UNITY/Detects.thy UNITY/ELT.thy \
13853 89131afa9f01 New theory ProgressSets. Definition of closure sets paulson parents: 13851 diff changeset	470	UNITY/Extend.thy UNITY/FP.thy UNITY/Follows.thy UNITY/Guar.thy\
89131afa9f01 New theory ProgressSets. Definition of closure sets paulson parents: 13851 diff changeset	471	UNITY/Lift_prog.thy UNITY/ListOrder.thy UNITY/ProgressSets.thy\
89131afa9f01 New theory ProgressSets. Definition of closure sets paulson parents: 13851 diff changeset	472	UNITY/PPROD.thy UNITY/Project.thy UNITY/Rename.thy UNITY/Transformers.thy\
13797 baefae13ad37 conversion of UNITY theories to new-style paulson parents: 13796 diff changeset	473	UNITY/SubstAx.thy UNITY/UNITY.thy UNITY/Union.thy UNITY/WFair.thy \
13790 8d7e9fce8c50 converting UNITY to new-style theories paulson parents: 13787 diff changeset	474	UNITY/Simple/Channel.thy UNITY/Simple/Common.thy \
8d7e9fce8c50 converting UNITY to new-style theories paulson parents: 13787 diff changeset	475	UNITY/Simple/Deadlock.thy UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy \
14199 d3b8d972a488 new session HOL-SET-Protocol paulson parents: 14182 diff changeset	476	UNITY/Simple/NSP_Bad.thy UNITY/Simple/Network.thy\
13790 8d7e9fce8c50 converting UNITY to new-style theories paulson parents: 13787 diff changeset	477	UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy UNITY/Simple/Token.thy\
21632 e7c1f1a77d18 converted legacy ML script; wenzelm parents: 21624 diff changeset	478	UNITY/Comp/Alloc.thy UNITY/Comp/AllocBase.thy UNITY/Comp/AllocImpl.thy \
e7c1f1a77d18 converted legacy ML script; wenzelm parents: 21624 diff changeset	479	UNITY/Comp/Client.thy UNITY/Comp/Counter.thy UNITY/Comp/Counterc.thy \
e7c1f1a77d18 converted legacy ML script; wenzelm parents: 21624 diff changeset	480	UNITY/Comp/Handshake.thy UNITY/Comp/PriorityAux.thy \
14087 cb07c3948668 Conversion of UNITY/Comp/Priority.thy to a linear Isar script paulson parents: 14075 diff changeset	481	UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \
14150 9a23e4eb5eb3 A document for UNITY paulson parents: 14145 diff changeset	482	UNITY/Comp/TimerArray.thy\
9a23e4eb5eb3 A document for UNITY paulson parents: 14145 diff changeset	483	UNITY/document/root.tex
9a23e4eb5eb3 A document for UNITY paulson parents: 14145 diff changeset	484	@$(ISATOOL) usedir -g true $(OUT)/HOL UNITY
4777 379f32b0ae40 New target HOL-UNITY paulson parents: 4729 diff changeset	485
379f32b0ae40 New target HOL-UNITY paulson parents: 4729 diff changeset	486
10966 8f2c27041a8e added HOL-Unix example; wenzelm parents: 10945 diff changeset	487	## HOL-Unix
8f2c27041a8e added HOL-Unix example; wenzelm parents: 10945 diff changeset	488
8f2c27041a8e added HOL-Unix example; wenzelm parents: 10945 diff changeset	489	HOL-Unix: HOL $(LOG)/HOL-Unix.gz
8f2c27041a8e added HOL-Unix example; wenzelm parents: 10945 diff changeset	490
8f2c27041a8e added HOL-Unix example; wenzelm parents: 10945 diff changeset	491	$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy \
8f2c27041a8e added HOL-Unix example; wenzelm parents: 10945 diff changeset	492	Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy \
8f2c27041a8e added HOL-Unix example; wenzelm parents: 10945 diff changeset	493	Unix/document/root.bib Unix/document/root.tex
8f2c27041a8e added HOL-Unix example; wenzelm parents: 10945 diff changeset	494	@$(ISATOOL) usedir $(OUT)/HOL Unix
8f2c27041a8e added HOL-Unix example; wenzelm parents: 10945 diff changeset	495
19203 778507520684 Added HOL-ZF to Isabelle. obua parents: 19192 diff changeset	496	## HOL-ZF
778507520684 Added HOL-ZF to Isabelle. obua parents: 19192 diff changeset	497
778507520684 Added HOL-ZF to Isabelle. obua parents: 19192 diff changeset	498	HOL-ZF: HOL $(LOG)/HOL-ZF.gz
778507520684 Added HOL-ZF to Isabelle. obua parents: 19192 diff changeset	499
778507520684 Added HOL-ZF to Isabelle. obua parents: 19192 diff changeset	500	$(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML \
778507520684 Added HOL-ZF to Isabelle. obua parents: 19192 diff changeset	501	ZF/Helper.thy ZF/LProd.thy ZF/HOLZF.thy \
778507520684 Added HOL-ZF to Isabelle. obua parents: 19192 diff changeset	502	ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex
778507520684 Added HOL-ZF to Isabelle. obua parents: 19192 diff changeset	503	@$(ISATOOL) usedir $(OUT)/HOL ZF
10966 8f2c27041a8e added HOL-Unix example; wenzelm parents: 10945 diff changeset	504
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	505	## HOL-Modelcheck
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	506
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	507	HOL-Modelcheck: HOL $(LOG)/HOL-Modelcheck.gz
3218 44f01b718eab added Modelcheck example; mueller parents: 3195 diff changeset	508
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	509	$(LOG)/HOL-Modelcheck.gz: $(OUT)/HOL Modelcheck/CTL.thy \
22819 a7b425bb668c removed legacy ML files; wenzelm parents: 22799 diff changeset	510	Modelcheck/EindhovenExample.thy Modelcheck/EindhovenSyn.thy \
a7b425bb668c removed legacy ML files; wenzelm parents: 22799 diff changeset	511	Modelcheck/MuCalculus.thy Modelcheck/MuckeExample1.thy \
a7b425bb668c removed legacy ML files; wenzelm parents: 22799 diff changeset	512	Modelcheck/MuckeExample2.thy Modelcheck/MuckeSyn.thy \
a7b425bb668c removed legacy ML files; wenzelm parents: 22799 diff changeset	513	Modelcheck/ROOT.ML Modelcheck/mucke_oracle.ML
3218 44f01b718eab added Modelcheck example; mueller parents: 3195 diff changeset	514	@$(ISATOOL) usedir $(OUT)/HOL Modelcheck
44f01b718eab added Modelcheck example; mueller parents: 3195 diff changeset	515
25314 5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: 25298 diff changeset	516	## HOL-SizeChange
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: 25298 diff changeset	517
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: 25298 diff changeset	518	HOL-SizeChange: HOL $(LOG)/HOL-SizeChange.gz
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: 25298 diff changeset	519
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: 25298 diff changeset	520	$(LOG)/HOL-SizeChange.gz: $(OUT)/HOL \
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: 25298 diff changeset	521	SizeChange/Kleene_Algebras.thy SizeChange/Graphs.thy \
25321 e34b2265698a activated HOL-SizeChange; wenzelm parents: 25315 diff changeset	522	SizeChange/Misc_Tools.thy SizeChange/Criterion.thy \
e34b2265698a activated HOL-SizeChange; wenzelm parents: 25315 diff changeset	523	SizeChange/Correctness.thy SizeChange/Interpretation.thy \
e34b2265698a activated HOL-SizeChange; wenzelm parents: 25315 diff changeset	524	SizeChange/Implementation.thy SizeChange/Size_Change_Termination.thy \
e34b2265698a activated HOL-SizeChange; wenzelm parents: 25315 diff changeset	525	SizeChange/Examples.thy SizeChange/sct.ML \
25314 5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: 25298 diff changeset	526	SizeChange/ROOT.ML
5eaf3e8b50a4 moved stuff about size change termination to its own session krauss parents: 25298 diff changeset	527	@$(ISATOOL) usedir $(OUT)/HOL SizeChange
3218 44f01b718eab added Modelcheck example; mueller parents: 3195 diff changeset	528
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	529	## HOL-Lambda
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	530
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	531	HOL-Lambda: HOL $(LOG)/HOL-Lambda.gz
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	532
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: 19499 diff changeset	533	$(LOG)/HOL-Lambda.gz: $(OUT)/HOL \
23194 085fa3def13b tuned webertj parents: 23193 diff changeset	534	Lambda/Commutation.thy Lambda/Eta.thy Lambda/InductTermi.thy \
085fa3def13b tuned webertj parents: 23193 diff changeset	535	Lambda/Lambda.thy \
9771 54c6a2c6e569 converted Lambda scripts; wenzelm parents: 9762 diff changeset	536	Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy \
24540 68dab042dea8 - New theories Lambda/NormalForm and Lambda/Standardization berghofe parents: 24472 diff changeset	537	Lambda/NormalForm.thy Lambda/ParRed.thy Lambda/Standardization.thy \
68dab042dea8 - New theories Lambda/NormalForm and Lambda/Standardization berghofe parents: 24472 diff changeset	538	Lambda/StrongNorm.thy Lambda/Type.thy \
14070 86c56794b641 Added new theories StrongNorm and WeakNorm to Lambda example. berghofe parents: 14044 diff changeset	539	Lambda/WeakNorm.thy Lambda/ROOT.ML \
86c56794b641 Added new theories StrongNorm and WeakNorm to Lambda example. berghofe parents: 14044 diff changeset	540	Lambda/document/root.bib Lambda/document/root.tex
22100 33d7468302bb HOL-Lambda: usedir -m no_brackets; wenzelm parents: 22077 diff changeset	541	@$(ISATOOL) usedir -g true -m no_brackets $(OUT)/HOL Lambda
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	542
61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	543
9015 8006e9009621 added HOL/Prolog oheimb parents: 8958 diff changeset	544	## HOL-Prolog
8006e9009621 added HOL/Prolog oheimb parents: 8958 diff changeset	545
8006e9009621 added HOL/Prolog oheimb parents: 8958 diff changeset	546	HOL-Prolog: HOL $(LOG)/HOL-Prolog.gz
8006e9009621 added HOL/Prolog oheimb parents: 8958 diff changeset	547
23194 085fa3def13b tuned webertj parents: 23193 diff changeset	548	$(LOG)/HOL-Prolog.gz: $(OUT)/HOL Prolog/ROOT.ML Prolog/prolog.ML \
085fa3def13b tuned webertj parents: 23193 diff changeset	549	Prolog/HOHH.thy \
21425 c11ab38b78a7 HOL-Prolog: converted legacy ML scripts; wenzelm parents: 21423 diff changeset	550	Prolog/Test.thy Prolog/Func.thy Prolog/Type.thy
9015 8006e9009621 added HOL/Prolog oheimb parents: 8958 diff changeset	551	@$(ISATOOL) usedir $(OUT)/HOL Prolog
8006e9009621 added HOL/Prolog oheimb parents: 8958 diff changeset	552
8006e9009621 added HOL/Prolog oheimb parents: 8958 diff changeset	553
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	554	## HOL-W0
2527 0ba3755ce398 Added W0 and modified MiniML. nipkow parents: 2473 diff changeset	555
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	556	HOL-W0: HOL $(LOG)/HOL-W0.gz
2527 0ba3755ce398 Added W0 and modified MiniML. nipkow parents: 2473 diff changeset	557
12946 75447c743810 Isar_examples/W_correct moved to W0; wenzelm parents: 12918 diff changeset	558	$(LOG)/HOL-W0.gz: $(OUT)/HOL W0/ROOT.ML W0/W0.thy W0/document/root.tex
2826 0b0d9e3bc661 isatool usedir; wenzelm parents: 2635 diff changeset	559	@$(ISATOOL) usedir $(OUT)/HOL W0
2527 0ba3755ce398 Added W0 and modified MiniML. nipkow parents: 2473 diff changeset	560
0ba3755ce398 Added W0 and modified MiniML. nipkow parents: 2473 diff changeset	561
8012 bbdf3c51c3b8 Added MicroJava nipkow parents: 8008 diff changeset	562	## HOL-MicroJava
bbdf3c51c3b8 Added MicroJava nipkow parents: 8008 diff changeset	563
bbdf3c51c3b8 Added MicroJava nipkow parents: 8008 diff changeset	564	HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
bbdf3c51c3b8 Added MicroJava nipkow parents: 8008 diff changeset	565
23854 688a8a7bcd4e uniform naming conventions for CG theories haftmann parents: 23772 diff changeset	566	$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL Library/Executable_Set.thy \
17637 409983bbaf00 Added ExecutableSet and Taylor. berghofe parents: 17618 diff changeset	567	MicroJava/ROOT.ML \
13672 b95d12325b51 Added compiler streckem parents: 13589 diff changeset	568	MicroJava/Comp/AuxLemmas.thy \
b95d12325b51 Added compiler streckem parents: 13589 diff changeset	569	MicroJava/Comp/CorrComp.thy \
b95d12325b51 Added compiler streckem parents: 13589 diff changeset	570	MicroJava/Comp/CorrCompTp.thy \
b95d12325b51 Added compiler streckem parents: 13589 diff changeset	571	MicroJava/Comp/DefsComp.thy \
b95d12325b51 Added compiler streckem parents: 13589 diff changeset	572	MicroJava/Comp/Index.thy \
b95d12325b51 Added compiler streckem parents: 13589 diff changeset	573	MicroJava/Comp/LemmasComp.thy \
b95d12325b51 Added compiler streckem parents: 13589 diff changeset	574	MicroJava/Comp/NatCanonify.thy \
b95d12325b51 Added compiler streckem parents: 13589 diff changeset	575	MicroJava/Comp/TranslComp.thy \
b95d12325b51 Added compiler streckem parents: 13589 diff changeset	576	MicroJava/Comp/TranslCompTp.thy \
b95d12325b51 Added compiler streckem parents: 13589 diff changeset	577	MicroJava/Comp/TypeInf.thy \
11026 a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 11024 diff changeset	578	MicroJava/J/Conform.thy MicroJava/J/Eval.thy MicroJava/J/JBasis.thy \
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 11024 diff changeset	579	MicroJava/J/JTypeSafe.thy MicroJava/J/Decl.thy MicroJava/J/State.thy \
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 11024 diff changeset	580	MicroJava/J/Term.thy MicroJava/J/Type.thy MicroJava/J/TypeRel.thy \
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 11024 diff changeset	581	MicroJava/J/WellForm.thy MicroJava/J/Value.thy \
a50365d21144 converted to Isar, simplifying recursion on class hierarchy oheimb parents: 11024 diff changeset	582	MicroJava/J/WellType.thy MicroJava/J/Example.thy \
12438 afd41635dcf9 Added new files (code generator and examples). berghofe parents: 12432 diff changeset	583	MicroJava/J/JListExample.thy \
9381 a0491eed2270 MicroJava structure changed kleing parents: 9353 diff changeset	584	MicroJava/JVM/JVMExec.thy MicroJava/JVM/JVMInstructions.thy\
a0491eed2270 MicroJava structure changed kleing parents: 9353 diff changeset	585	MicroJava/JVM/JVMState.thy MicroJava/JVM/JVMExecInstr.thy\
12521 b1ebe0320d79 MicroJava exception merge kleing parents: 12438 diff changeset	586	MicroJava/JVM/JVMListExample.thy MicroJava/JVM/JVMExceptions.thy \
11228 5516e806dc09 MicroJava/BV dependencies incomplete nipkow parents: 11220 diff changeset	587	MicroJava/BV/BVSpec.thy MicroJava/BV/BVSpecTypeSafe.thy \
5516e806dc09 MicroJava/BV dependencies incomplete nipkow parents: 11220 diff changeset	588	MicroJava/BV/Correct.thy MicroJava/BV/Err.thy MicroJava/BV/JType.thy \
5516e806dc09 MicroJava/BV dependencies incomplete nipkow parents: 11220 diff changeset	589	MicroJava/BV/JVM.thy MicroJava/BV/JVMType.thy MicroJava/BV/Kildall.thy \
5516e806dc09 MicroJava/BV dependencies incomplete nipkow parents: 11220 diff changeset	590	MicroJava/BV/LBVSpec.thy MicroJava/BV/Listn.thy MicroJava/BV/Opt.thy \
5516e806dc09 MicroJava/BV dependencies incomplete nipkow parents: 11220 diff changeset	591	MicroJava/BV/Product.thy MicroJava/BV/Semilat.thy \
12521 b1ebe0320d79 MicroJava exception merge kleing parents: 12438 diff changeset	592	MicroJava/BV/Effect.thy MicroJava/BV/EffectMono.thy \
11228 5516e806dc09 MicroJava/BV dependencies incomplete nipkow parents: 11220 diff changeset	593	MicroJava/BV/Typing_Framework.thy MicroJava/BV/Typing_Framework_err.thy \
13224 6f0928a942d1 LBV instantiantion refactored, streamlined kleing parents: 13200 diff changeset	594	MicroJava/BV/Typing_Framework_JVM.thy MicroJava/BV/BVExample.thy \
6f0928a942d1 LBV instantiantion refactored, streamlined kleing parents: 13200 diff changeset	595	MicroJava/BV/LBVSpec.thy MicroJava/BV/LBVCorrect.thy \
6f0928a942d1 LBV instantiantion refactored, streamlined kleing parents: 13200 diff changeset	596	MicroJava/BV/LBVComplete.thy MicroJava/BV/LBVJVM.thy \
12915 2832fba717ec new MicroJava document kleing parents: 12897 diff changeset	597	MicroJava/document/root.bib MicroJava/document/root.tex \
2832fba717ec new MicroJava document kleing parents: 12897 diff changeset	598	MicroJava/document/introduction.tex
11850 cdfc3fce577e document graphs for several sessions; wenzelm parents: 11837 diff changeset	599	@$(ISATOOL) usedir -g true $(OUT)/HOL MicroJava
cdfc3fce577e document graphs for several sessions; wenzelm parents: 11837 diff changeset	600
8012 bbdf3c51c3b8 Added MicroJava nipkow parents: 8008 diff changeset	601
11376 bf98ad1c22c6 added NanoJava oheimb parents: 11370 diff changeset	602	## HOL-NanoJava
bf98ad1c22c6 added NanoJava oheimb parents: 11370 diff changeset	603
bf98ad1c22c6 added NanoJava oheimb parents: 11370 diff changeset	604	HOL-NanoJava: HOL $(LOG)/HOL-NanoJava.gz
bf98ad1c22c6 added NanoJava oheimb parents: 11370 diff changeset	605
bf98ad1c22c6 added NanoJava oheimb parents: 11370 diff changeset	606	$(LOG)/HOL-NanoJava.gz: $(OUT)/HOL NanoJava/ROOT.ML \
bf98ad1c22c6 added NanoJava oheimb parents: 11370 diff changeset	607	NanoJava/Term.thy NanoJava/Decl.thy NanoJava/TypeRel.thy NanoJava/State.thy \
bf98ad1c22c6 added NanoJava oheimb parents: 11370 diff changeset	608	NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy \
bf98ad1c22c6 added NanoJava oheimb parents: 11370 diff changeset	609	NanoJava/document/root.bib NanoJava/document/root.tex
11850 cdfc3fce577e document graphs for several sessions; wenzelm parents: 11837 diff changeset	610	@$(ISATOOL) usedir -g true $(OUT)/HOL NanoJava
cdfc3fce577e document graphs for several sessions; wenzelm parents: 11837 diff changeset	611
8193 33e4ec7a2daa added MicroJava/document; wenzelm parents: 8179 diff changeset	612
12855 21225338f8db Bali added schirmer parents: 12816 diff changeset	613	## HOL-Bali
21225338f8db Bali added schirmer parents: 12816 diff changeset	614
21225338f8db Bali added schirmer parents: 12816 diff changeset	615	HOL-Bali: HOL $(LOG)/HOL-Bali.gz
21225338f8db Bali added schirmer parents: 12816 diff changeset	616
21225338f8db Bali added schirmer parents: 12816 diff changeset	617	$(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/AxCompl.thy Bali/AxExample.thy \
21225338f8db Bali added schirmer parents: 12816 diff changeset	618	Bali/AxSem.thy Bali/AxSound.thy Bali/Basis.thy Bali/Conform.thy \
21225338f8db Bali added schirmer parents: 12816 diff changeset	619	Bali/Decl.thy Bali/DeclConcepts.thy Bali/Eval.thy Bali/Evaln.thy \
21225338f8db Bali added schirmer parents: 12816 diff changeset	620	Bali/Example.thy Bali/Name.thy Bali/ROOT.ML Bali/State.thy \
21225338f8db Bali added schirmer parents: 12816 diff changeset	621	Bali/Table.thy Bali/Term.thy Bali/Trans.thy Bali/Type.thy \
21225338f8db Bali added schirmer parents: 12816 diff changeset	622	Bali/TypeRel.thy Bali/TypeSafe.thy Bali/Value.thy Bali/WellForm.thy \
13695 3e48dcd25746 two new Bali files kleing parents: 13682 diff changeset	623	Bali/DefiniteAssignment.thy Bali/DefiniteAssignmentCorrect.thy \
12855 21225338f8db Bali added schirmer parents: 12816 diff changeset	624	Bali/WellType.thy Bali/document/root.tex
21225338f8db Bali added schirmer parents: 12816 diff changeset	625	@$(ISATOOL) usedir -g true $(OUT)/HOL Bali
21225338f8db Bali added schirmer parents: 12816 diff changeset	626
21225338f8db Bali added schirmer parents: 12816 diff changeset	627
13403 bc2b32ee62fd Added theory for setting up program extraction. berghofe parents: 13224 diff changeset	628	## HOL-Extraction
bc2b32ee62fd Added theory for setting up program extraction. berghofe parents: 13224 diff changeset	629
bc2b32ee62fd Added theory for setting up program extraction. berghofe parents: 13224 diff changeset	630	HOL-Extraction: HOL $(LOG)/HOL-Extraction.gz
bc2b32ee62fd Added theory for setting up program extraction. berghofe parents: 13224 diff changeset	631
23854 688a8a7bcd4e uniform naming conventions for CG theories haftmann parents: 23772 diff changeset	632	$(LOG)/HOL-Extraction.gz: $(OUT)/HOL Library/Efficient_Nat.thy \
25423 2c6167e2c587 Added new program extraction examples. berghofe parents: 25321 diff changeset	633	Extraction/Euclid.thy Extraction/Greatest_Common_Divisor.thy \
2c6167e2c587 Added new program extraction examples. berghofe parents: 25321 diff changeset	634	Extraction/Higman.thy Extraction/Pigeonhole.thy Extraction/QuotRem.thy \
2c6167e2c587 Added new program extraction examples. berghofe parents: 25321 diff changeset	635	Extraction/ROOT.ML Extraction/Util.thy \
13403 bc2b32ee62fd Added theory for setting up program extraction. berghofe parents: 13224 diff changeset	636	Extraction/Warshall.thy Extraction/document/root.tex \
bc2b32ee62fd Added theory for setting up program extraction. berghofe parents: 13224 diff changeset	637	Extraction/document/root.bib
bc2b32ee62fd Added theory for setting up program extraction. berghofe parents: 13224 diff changeset	638	@$(ISATOOL) usedir $(OUT)/HOL Extraction
bc2b32ee62fd Added theory for setting up program extraction. berghofe parents: 13224 diff changeset	639
bc2b32ee62fd Added theory for setting up program extraction. berghofe parents: 13224 diff changeset	640
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	641	## HOL-IOA
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	642
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	643	HOL-IOA: HOL $(LOG)/HOL-IOA.gz
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	644
19801 b2af2549efd1 removed obsolete ML files; wenzelm parents: 19767 diff changeset	645	$(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.thy IOA/IOA.thy \
b2af2549efd1 removed obsolete ML files; wenzelm parents: 19767 diff changeset	646	IOA/ROOT.ML IOA/Solve.thy
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	647	@$(ISATOOL) usedir $(OUT)/HOL IOA
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	648
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	649
10135 c2a4dccf6e67 reorganized AxClasses; wenzelm parents: 10094 diff changeset	650	## HOL-AxClasses
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	651
10135 c2a4dccf6e67 reorganized AxClasses; wenzelm parents: 10094 diff changeset	652	HOL-AxClasses: HOL $(LOG)/HOL-AxClasses.gz
2545 d10abc8c11fb added AxClasses test; wenzelm parents: 2527 diff changeset	653
10135 c2a4dccf6e67 reorganized AxClasses; wenzelm parents: 10094 diff changeset	654	$(LOG)/HOL-AxClasses.gz: $(OUT)/HOL AxClasses/Group.thy \
c2a4dccf6e67 reorganized AxClasses; wenzelm parents: 10094 diff changeset	655	AxClasses/Product.thy AxClasses/ROOT.ML AxClasses/Semigroups.thy
c2a4dccf6e67 reorganized AxClasses; wenzelm parents: 10094 diff changeset	656	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
2545 d10abc8c11fb added AxClasses test; wenzelm parents: 2527 diff changeset	657
d10abc8c11fb added AxClasses test; wenzelm parents: 2527 diff changeset	658
10157 6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	659	## HOL-Lattice
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	660
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	661	HOL-Lattice: HOL $(LOG)/HOL-Lattice.gz
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	662
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	663	$(LOG)/HOL-Lattice.gz: $(OUT)/HOL Lattice/Bounds.thy \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	664	Lattice/CompleteLattice.thy Lattice/Lattice.thy Lattice/Orders.thy \
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	665	Lattice/ROOT.ML Lattice/document/root.tex
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	666	@$(ISATOOL) usedir $(OUT)/HOL Lattice
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	667
6d3987f3aad9 * HOL/Lattice: fundamental concepts of lattice theory and order structures; wenzelm parents: 10143 diff changeset	668
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	669	## HOL-ex
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	670
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	671	HOL-ex: HOL $(LOG)/HOL-ex.gz
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	672
23194 085fa3def13b tuned webertj parents: 23193 diff changeset	673	$(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy \
085fa3def13b tuned webertj parents: 23193 diff changeset	674	ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy \
23213 43553703267c HOL-ex: tuned deps; wenzelm parents: 23194 diff changeset	675	ex/BT.thy ex/BinEx.thy ex/CTL.thy \
25543 6b2031004d3f dropped Classpackage.thy haftmann parents: 25423 diff changeset	676	ex/Chinese.thy ex/Classical.thy ex/Dense_Linear_Order_Ex.thy \
26265 4b63b9e9b10d separated Random.thy from Quickcheck.thy haftmann parents: 26232 diff changeset	677	ex/Eval_Examples.thy ex/Groebner_Examples.thy ex/Random.thy ex/Quickcheck.thy \
24194 96013f81faef re-eliminated Option.thy haftmann parents: 24162 diff changeset	678	ex/Codegenerator.thy ex/Codegenerator_Pretty.thy \
25963 07e08dad8a77 distinguished examples for Efficient_Nat.thy haftmann parents: 25919 diff changeset	679	ex/Commutative_RingEx.thy ex/Efficient_Nat_examples.thy ex/Hex_Bin_Examples.thy \
23194 085fa3def13b tuned webertj parents: 23193 diff changeset	680	ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy \
085fa3def13b tuned webertj parents: 23193 diff changeset	681	ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy ex/Binary.thy \
24616 fac3dd4ade83 sorting nipkow parents: 24607 diff changeset	682	ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy \
25568 7bb10db582cf Adding "ex/Induction_Scheme.thy" to tests krauss parents: 25557 diff changeset	683	ex/Induction_Scheme.thy \
23194 085fa3def13b tuned webertj parents: 23193 diff changeset	684	ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \
24326 3e9d3ba894b8 converted ex/MT.ML; wenzelm parents: 24325 diff changeset	685	ex/Intuitionistic.thy ex/Lagrange.thy ex/Locales.thy ex/LocaleTest2.thy \
23194 085fa3def13b tuned webertj parents: 23193 diff changeset	686	ex/MT.thy ex/MergeSort.thy ex/MonoidGroup.thy ex/Multiquote.thy \
26103 b9fc7ac04c8b removed ex/NBE.thy; wenzelm parents: 25963 diff changeset	687	ex/NatSum.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
24616 fac3dd4ade83 sorting nipkow parents: 24607 diff changeset	688	ex/Puzzle.thy ex/Quickcheck_Examples.thy \
23549 88190085bb82 Dependency on reflection_data.ML to build HOL-ex chaieb parents: 23519 diff changeset	689	ex/Reflection.thy ex/reflection_data.ML ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy \
23274 f997514ad8f4 New Reflected Presburger added to HOL/ex chaieb parents: 23267 diff changeset	690	ex/Records.thy ex/Reflected_Presburger.thy ex/coopertac.ML ex/coopereif.ML \
24470 41c81e23c08d removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system); wenzelm parents: 24465 diff changeset	691	ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \
23194 085fa3def13b tuned webertj parents: 23193 diff changeset	692	ex/Sudoku.thy ex/Tarski.thy ex/Unification.thy ex/document/root.bib \
24127 a56b6ed2e49c converted Meson tests to proper theory; wenzelm parents: 24103 diff changeset	693	ex/document/root.tex ex/Meson_Test.thy ex/reflection.ML \
23003 4b0bf04a4d68 updated krauss parents: 22981 diff changeset	694	ex/set.thy ex/svc_funcs.ML ex/svc_test.thy Library/Parity.thy Library/GCD.thy
2826 0b0d9e3bc661 isatool usedir; wenzelm parents: 2635 diff changeset	695	@$(ISATOOL) usedir $(OUT)/HOL ex
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	696
61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	697
6445 931fc1daa8b1 added Isar_examples; wenzelm parents: 6440 diff changeset	698	## HOL-Isar_examples
931fc1daa8b1 added Isar_examples; wenzelm parents: 6440 diff changeset	699
931fc1daa8b1 added Isar_examples; wenzelm parents: 6440 diff changeset	700	HOL-Isar_examples: HOL $(LOG)/HOL-Isar_examples.gz
931fc1daa8b1 added Isar_examples; wenzelm parents: 6440 diff changeset	701
931fc1daa8b1 added Isar_examples; wenzelm parents: 6440 diff changeset	702	$(LOG)/HOL-Isar_examples.gz: $(OUT)/HOL Isar_examples/BasicLogic.thy \
20767 9bc632ae588f removed obsolete Real/document/root.tex; wenzelm parents: 20762 diff changeset	703	Isar_examples/Cantor.thy Isar_examples/Drinker.thy \
8050 ad6440cd84be added Isar_examples/Fibonacci.thy; wenzelm parents: 8040 diff changeset	704	Isar_examples/ExprCompiler.thy Isar_examples/Fibonacci.thy \
10143 86c39bba873f added Isar_examples/Hoare.thy Isar_examples/HoareEx.thy; wenzelm parents: 10135 diff changeset	705	Isar_examples/Group.thy Isar_examples/Hoare.thy Isar_examples/HoareEx.thy \
10255 bb66874b4750 added HOL/Library, rearranged several files; wenzelm parents: 10214 diff changeset	706	Isar_examples/KnasterTarski.thy Isar_examples/MutilatedCheckerboard.thy \
8677 de62440762b8 added Isar_examples/NestedDatatype.thy; wenzelm parents: 8569 diff changeset	707	Isar_examples/NestedDatatype.thy Isar_examples/Peirce.thy \
8050 ad6440cd84be added Isar_examples/Fibonacci.thy; wenzelm parents: 8040 diff changeset	708	Isar_examples/Puzzle.thy Isar_examples/Summation.thy \
12946 75447c743810 Isar_examples/W_correct moved to W0; wenzelm parents: 12918 diff changeset	709	Isar_examples/ROOT.ML Isar_examples/document/proof.sty \
75447c743810 Isar_examples/W_correct moved to W0; wenzelm parents: 12918 diff changeset	710	Isar_examples/document/root.bib Isar_examples/document/root.tex \
24472 943ef707396c added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy); wenzelm parents: 24470 diff changeset	711	Isar_examples/document/style.tex Hoare/hoare_tac.ML
6445 931fc1daa8b1 added Isar_examples; wenzelm parents: 6440 diff changeset	712	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
931fc1daa8b1 added Isar_examples; wenzelm parents: 6440 diff changeset	713
931fc1daa8b1 added Isar_examples; wenzelm parents: 6440 diff changeset	714
14199 d3b8d972a488 new session HOL-SET-Protocol paulson parents: 14182 diff changeset	715	## HOL-SET-Protocol
d3b8d972a488 new session HOL-SET-Protocol paulson parents: 14182 diff changeset	716
d3b8d972a488 new session HOL-SET-Protocol paulson parents: 14182 diff changeset	717	HOL-SET-Protocol: HOL $(LOG)/HOL-SET-Protocol.gz
d3b8d972a488 new session HOL-SET-Protocol paulson parents: 14182 diff changeset	718
d3b8d972a488 new session HOL-SET-Protocol paulson parents: 14182 diff changeset	719	$(LOG)/HOL-SET-Protocol.gz: $(OUT)/HOL SET-Protocol/ROOT.ML \
d3b8d972a488 new session HOL-SET-Protocol paulson parents: 14182 diff changeset	720	SET-Protocol/MessageSET.thy\
d3b8d972a488 new session HOL-SET-Protocol paulson parents: 14182 diff changeset	721	SET-Protocol/EventSET.thy\
d3b8d972a488 new session HOL-SET-Protocol paulson parents: 14182 diff changeset	722	SET-Protocol/PublicSET.thy\
d3b8d972a488 new session HOL-SET-Protocol paulson parents: 14182 diff changeset	723	SET-Protocol/Cardholder_Registration.thy\
d3b8d972a488 new session HOL-SET-Protocol paulson parents: 14182 diff changeset	724	SET-Protocol/Merchant_Registration.thy\
d3b8d972a488 new session HOL-SET-Protocol paulson parents: 14182 diff changeset	725	SET-Protocol/Purchase.thy\
d3b8d972a488 new session HOL-SET-Protocol paulson parents: 14182 diff changeset	726	SET-Protocol/document/root.tex
d3b8d972a488 new session HOL-SET-Protocol paulson parents: 14182 diff changeset	727	@$(ISATOOL) usedir -g true $(OUT)/HOL SET-Protocol
d3b8d972a488 new session HOL-SET-Protocol paulson parents: 14182 diff changeset	728
d3b8d972a488 new session HOL-SET-Protocol paulson parents: 14182 diff changeset	729
16509 20f4c6a950f7 fixed HOL-Complex-Matrix target; wenzelm parents: 16484 diff changeset	730	## HOL-Complex-Matrix
14610 9c2e31e483b2 added HOL-Matrix, added HOL/Matrix/ROOT.ML kleing parents: 14603 diff changeset	731
17546 07371b92d382 HOL-Complex-Matrix: fixed deps; wenzelm parents: 17518 diff changeset	732	HOL-Complex-Matrix: HOL-Complex $(OUT)/HOL-Complex-Matrix
17323 2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight obua parents: 17308 diff changeset	733
2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight obua parents: 17308 diff changeset	734	$(OUT)/HOL-Complex-Matrix: $(OUT)/HOL-Complex \
23172 f1ae6a8648ef moved IsaPlanner from Provers to Tools; wenzelm parents: 23164 diff changeset	735	$(SRC)/Tools/Compute_Oracle/Compute_Oracle.thy \
f1ae6a8648ef moved IsaPlanner from Provers to Tools; wenzelm parents: 23164 diff changeset	736	$(SRC)/Tools/Compute_Oracle/am_compiler.ML \
f1ae6a8648ef moved IsaPlanner from Provers to Tools; wenzelm parents: 23164 diff changeset	737	$(SRC)/Tools/Compute_Oracle/am_interpreter.ML \
23772 b96db2903a9a changed sources for HOL-Complex-Matrix obua parents: 23734 diff changeset	738	$(SRC)/Tools/Compute_Oracle/am.ML \
b96db2903a9a changed sources for HOL-Complex-Matrix obua parents: 23734 diff changeset	739	$(SRC)/Tools/Compute_Oracle/linker.ML \
b96db2903a9a changed sources for HOL-Complex-Matrix obua parents: 23734 diff changeset	740	$(SRC)/Tools/Compute_Oracle/am_ghc.ML \
b96db2903a9a changed sources for HOL-Complex-Matrix obua parents: 23734 diff changeset	741	$(SRC)/Tools/Compute_Oracle/am_sml.ML \
23194 085fa3def13b tuned webertj parents: 23193 diff changeset	742	$(SRC)/Tools/Compute_Oracle/compute.ML \
23172 f1ae6a8648ef moved IsaPlanner from Provers to Tools; wenzelm parents: 23164 diff changeset	743	Matrix/MatrixGeneral.thy Matrix/Matrix.thy Matrix/SparseMatrix.thy \
f1ae6a8648ef moved IsaPlanner from Provers to Tools; wenzelm parents: 23164 diff changeset	744	Matrix/LP.thy Matrix/document/root.tex Matrix/ROOT.ML \
17489 f70d62d5f9c8 Removed superfluous HOL/Matrix/cplex/ROOT.ML. obua parents: 17488 diff changeset	745	Matrix/cplex/Cplex.thy Matrix/cplex/CplexMatrixConverter.ML \
16784 92ff7c903585 - added cplex package to HOL/Matrix obua parents: 16782 diff changeset	746	Matrix/cplex/Cplex_tools.ML Matrix/cplex/FloatSparseMatrix.thy \
16873 9ed940a1bebb proving bounds for real linear programs obua parents: 16784 diff changeset	747	Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML \
20787 406d990006af moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML; wenzelm parents: 20767 diff changeset	748	Matrix/cplex/MatrixLP.thy Matrix/cplex/matrixlp.ML
17323 2fc68de9de1f 1) Added target HOL-Complex-Generate-HOLLight obua parents: 17308 diff changeset	749	@cd Matrix; $(ISATOOL) usedir -b -g true $(OUT)/HOL-Complex HOL-Complex-Matrix
16873 9ed940a1bebb proving bounds for real linear programs obua parents: 16784 diff changeset	750
14199 d3b8d972a488 new session HOL-SET-Protocol paulson parents: 14182 diff changeset	751
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	752	## TLA
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	753
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	754	TLA: HOL $(OUT)/TLA
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	755
21624 6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 21542 diff changeset	756	$(OUT)/TLA: $(OUT)/HOL TLA/Action.thy TLA/Init.thy TLA/Intensional.thy \
6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 21542 diff changeset	757	TLA/ROOT.ML TLA/Stfun.thy TLA/TLA.thy
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	758	@cd TLA; $(ISATOOL) usedir -b $(OUT)/HOL TLA
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	759
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	760
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	761	## TLA-Inc
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	762
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	763	TLA-Inc: TLA $(LOG)/TLA-Inc.gz
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	764
21624 6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 21542 diff changeset	765	$(LOG)/TLA-Inc.gz: $(OUT)/TLA TLA/Inc/Inc.thy
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	766	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Inc
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	767
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	768
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	769	## TLA-Buffer
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	770
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	771	TLA-Buffer: TLA $(LOG)/TLA-Buffer.gz
2448 61337170db84 IsaMakefile for HOL; wenzelm parents: diff changeset	772
21624 6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 21542 diff changeset	773	$(LOG)/TLA-Buffer.gz: $(OUT)/TLA TLA/Buffer/Buffer.thy TLA/Buffer/DBuffer.thy
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	774	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Buffer
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	775
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	776
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	777	## TLA-Memory
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	778
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	779	TLA-Memory: TLA $(LOG)/TLA-Memory.gz
4447 b7ee449eb345 log files; wenzelm parents: 4289 diff changeset	780
26688 6a91e368590d removed unused TLA/Memory/MIParameters.thy; wenzelm parents: 26583 diff changeset	781	$(LOG)/TLA-Memory.gz: $(OUT)/TLA \
21624 6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 21542 diff changeset	782	TLA/Memory/MemClerk.thy TLA/Memory/MemClerkParameters.thy \
6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 21542 diff changeset	783	TLA/Memory/Memory.thy TLA/Memory/MemoryImplementation.thy \
23194 085fa3def13b tuned webertj parents: 23193 diff changeset	784	TLA/Memory/MemoryParameters.thy TLA/Memory/ProcedureInterface.thy \
085fa3def13b tuned webertj parents: 23193 diff changeset	785	TLA/Memory/RPC.thy \
21624 6f79647cf536 TLA: converted legacy ML scripts; wenzelm parents: 21542 diff changeset	786	TLA/Memory/RPCMemoryParams.thy TLA/Memory/RPCParameters.thy
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	787	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Memory
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	788
74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	789
19497 630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	790	## HOL-Nominal
630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	791
630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	792	HOL-Nominal: HOL $(OUT)/HOL-Nominal
630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	793
22245 1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls urbanc parents: 22167 diff changeset	794	$(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	795	Nominal/Nominal.thy \
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls urbanc parents: 22167 diff changeset	796	Nominal/nominal_atoms.ML \
22784 4637b69de71b Added datatype_case.ML and nominal_fresh_fun.ML. berghofe parents: 22657 diff changeset	797	Nominal/nominal_fresh_fun.ML \
22247 5bad0d429694 corrected typo introduced by me urbanc parents: 22245 diff changeset	798	Nominal/nominal_induct.ML \
22314 d541f13756a2 Added new file Nominal/nominal_inductive.ML berghofe parents: 22260 diff changeset	799	Nominal/nominal_inductive.ML \
22245 1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls urbanc parents: 22167 diff changeset	800	Nominal/nominal_package.ML \
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls urbanc parents: 22167 diff changeset	801	Nominal/nominal_permeq.ML \
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls urbanc parents: 22167 diff changeset	802	Nominal/nominal_primrec.ML \
1b8f4ef50c48 moved the infrastructure from the nominal_tags file to nominal_thmdecls urbanc parents: 22167 diff changeset	803	Nominal/nominal_thmdecls.ML \
21542 4462ee172ef0 Added nominal_primrec.ML berghofe parents: 21425 diff changeset	804	Library/Infinite_Set.thy
19497 630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	805	@cd Nominal; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Nominal
630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	806
630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	807
630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	808	## HOL-Nominal-Examples
630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	809
630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	810	HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz
630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	811
19564 d3e2f532459a First usable version of the new function definition package (HOL/function_packake/...). krauss parents: 19499 diff changeset	812	$(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal \
22073 c170dcbe6c9d formalisation of Crary's chapter on logical relations urbanc parents: 22067 diff changeset	813	Nominal/Examples/CR.thy \
22821 15b2e7ec1f3b alternative and much simpler proof for Church-Rosser of Beta-Reduction urbanc parents: 22819 diff changeset	814	Nominal/Examples/CR_Takahashi.thy \
24152 63cc746667a0 reactivated Nominal/Examples/Class.thy; wenzelm parents: 24139 diff changeset	815	Nominal/Examples/Class.thy \
22073 c170dcbe6c9d formalisation of Crary's chapter on logical relations urbanc parents: 22067 diff changeset	816	Nominal/Examples/Compile.thy \
25725 18bc59fb01b5 updated HOL-Nominal-Examples deps; wenzelm parents: 25600 diff changeset	817	Nominal/Examples/Contexts.thy \
18bc59fb01b5 updated HOL-Nominal-Examples deps; wenzelm parents: 25600 diff changeset	818	Nominal/Examples/Crary.thy \
22073 c170dcbe6c9d formalisation of Crary's chapter on logical relations urbanc parents: 22067 diff changeset	819	Nominal/Examples/Fsub.thy \
25725 18bc59fb01b5 updated HOL-Nominal-Examples deps; wenzelm parents: 25600 diff changeset	820	Nominal/Examples/Height.thy \
18bc59fb01b5 updated HOL-Nominal-Examples deps; wenzelm parents: 25600 diff changeset	821	Nominal/Examples/Lam_Funs.thy \
22073 c170dcbe6c9d formalisation of Crary's chapter on logical relations urbanc parents: 22067 diff changeset	822	Nominal/Examples/Lambda_mu.thy \
25725 18bc59fb01b5 updated HOL-Nominal-Examples deps; wenzelm parents: 25600 diff changeset	823	Nominal/Examples/LocalWeakening.thy \
18bc59fb01b5 updated HOL-Nominal-Examples deps; wenzelm parents: 25600 diff changeset	824	Nominal/Examples/ROOT.ML \
22073 c170dcbe6c9d formalisation of Crary's chapter on logical relations urbanc parents: 22067 diff changeset	825	Nominal/Examples/SN.thy \
23144 4a9c9e260abf included new example in the compiling process urbanc parents: 23100 diff changeset	826	Nominal/Examples/SOS.thy \
24896 70f238757695 added the two new examples from Nominal to the build process urbanc parents: 24830 diff changeset	827	Nominal/Examples/Support.thy \
25725 18bc59fb01b5 updated HOL-Nominal-Examples deps; wenzelm parents: 25600 diff changeset	828	Nominal/Examples/VC_Condition.thy \
26195 8292f8723e99 added new example urbanc parents: 26192 diff changeset	829	Nominal/Examples/W.thy \
25725 18bc59fb01b5 updated HOL-Nominal-Examples deps; wenzelm parents: 25600 diff changeset	830	Nominal/Examples/Weakening.thy
19497 630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	831	@cd Nominal; $(ISATOOL) usedir $(OUT)/HOL-Nominal Examples
630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	832
630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	833
24333 e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	834	## HOL-Word
e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	835
e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	836	HOL-Word: HOL $(OUT)/HOL-Word
e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	837
e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	838	$(OUT)/HOL-Word: $(OUT)/HOL Word/ROOT.ML \
e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	839	Library/Infinite_Set.thy Library/Parity.thy \
e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	840	Library/Boolean_Algebra.thy Library/Numeral_Type.thy \
e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	841	Word/Num_Lemmas.thy \
e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	842	Word/TdThs.thy \
24465 70f0214b3ecc revert to Word library version from 2007/08/20 huffman parents: 24462 diff changeset	843	Word/Size.thy \
24333 e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	844	Word/BinGeneral.thy \
e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	845	Word/BinOperations.thy \
e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	846	Word/BinBoolList.thy \
e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	847	Word/BitSyntax.thy \
e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	848	Word/WordDefinition.thy \
e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	849	Word/WordArith.thy \
e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	850	Word/WordBitwise.thy \
e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	851	Word/WordShift.thy \
e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	852	Word/WordGenLib.thy \
e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	853	Word/WordMain.thy \
25298 63f6d969253e add root.bib for Word document kleing parents: 25173 diff changeset	854	Word/document/root.tex Word/document/root.bib
24333 e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	855	@cd Word; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Word
e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	856
e77ea0ea7f2c * HOL-Word: kleing parents: 24332 diff changeset	857
24442 39e29972cb96 HOL-Word-Examples huffman parents: 24411 diff changeset	858	## HOL-Word-Examples
39e29972cb96 HOL-Word-Examples huffman parents: 24411 diff changeset	859
39e29972cb96 HOL-Word-Examples huffman parents: 24411 diff changeset	860	HOL-Word-Examples: HOL-Word $(LOG)/HOL-Word-Examples.gz
39e29972cb96 HOL-Word-Examples huffman parents: 24411 diff changeset	861
39e29972cb96 HOL-Word-Examples huffman parents: 24411 diff changeset	862	$(LOG)/HOL-Word-Examples.gz: $(OUT)/HOL-Word \
39e29972cb96 HOL-Word-Examples huffman parents: 24411 diff changeset	863	Word/Examples/ROOT.ML \
39e29972cb96 HOL-Word-Examples huffman parents: 24411 diff changeset	864	Word/Examples/WordExamples.thy
39e29972cb96 HOL-Word-Examples huffman parents: 24411 diff changeset	865	@cd Word; $(ISATOOL) usedir $(OUT)/HOL-Word Examples
39e29972cb96 HOL-Word-Examples huffman parents: 24411 diff changeset	866
25171 4a9c25bffc9b added Statespace library schirmer parents: 24994 diff changeset	867	## HOL-Statespace
4a9c25bffc9b added Statespace library schirmer parents: 24994 diff changeset	868
4a9c25bffc9b added Statespace library schirmer parents: 24994 diff changeset	869	HOL-Statespace: HOL $(LOG)/HOL-Statespace.gz
4a9c25bffc9b added Statespace library schirmer parents: 24994 diff changeset	870
4a9c25bffc9b added Statespace library schirmer parents: 24994 diff changeset	871	$(LOG)/HOL-Statespace.gz: $(OUT)/HOL Statespace/DistinctTreeProver.thy \
4a9c25bffc9b added Statespace library schirmer parents: 24994 diff changeset	872	Statespace/StateFun.thy Statespace/StateSpaceLocale.thy \
25173 7e1f197a36c5 fixed HOL-Statespace for case-sensitive file-system; wenzelm parents: 25171 diff changeset	873	Statespace/StateSpaceSyntax.thy Statespace/StateSpaceEx.thy \
25171 4a9c25bffc9b added Statespace library schirmer parents: 24994 diff changeset	874	Statespace/distinct_tree_prover.ML Statespace/state_space.ML \
4a9c25bffc9b added Statespace library schirmer parents: 24994 diff changeset	875	Statespace/state_fun.ML \
4a9c25bffc9b added Statespace library schirmer parents: 24994 diff changeset	876	Statespace/document/root.tex
4a9c25bffc9b added Statespace library schirmer parents: 24994 diff changeset	877	@$(ISATOOL) usedir -g true $(OUT)/HOL Statespace
24442 39e29972cb96 HOL-Word-Examples huffman parents: 24411 diff changeset	878
4518 74c01296e818 improved targets; wenzelm parents: 4455 diff changeset	879	## clean
4447 b7ee449eb345 log files; wenzelm parents: 4289 diff changeset	880
b7ee449eb345 log files; wenzelm parents: 4289 diff changeset	881	clean:
19497 630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	882	@rm -f $(OUT)/HOL $(OUT)/HOL-Complex $(OUT)/HOL-Nominal $(OUT)/TLA \
13980 f254d1c92a6a removed obsolete references to HOL-Real paulson parents: 13967 diff changeset	883	$(LOG)/HOL.gz $(LOG)/TLA.gz \
9481 b16624f1ea38 tuned; wenzelm parents: 9479 diff changeset	884	$(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \
b16624f1ea38 tuned; wenzelm parents: 9479 diff changeset	885	$(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \
b16624f1ea38 tuned; wenzelm parents: 9479 diff changeset	886	$(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \
12996 7ac0a7e306db Completed annonce of HoareParallel prensani parents: 12951 diff changeset	887	$(LOG)/HOL-HoareParallel.gz \
9481 b16624f1ea38 tuned; wenzelm parents: 9479 diff changeset	888	$(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
b16624f1ea38 tuned; wenzelm parents: 9479 diff changeset	889	$(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
b16624f1ea38 tuned; wenzelm parents: 9479 diff changeset	890	$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
15871 e524119dbf19 * empty log message * bauerg parents: 15858 diff changeset	891	$(LOG)/HOL-Bali.gz \
11376 bf98ad1c22c6 added NanoJava oheimb parents: 11370 diff changeset	892	$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
19497 630073ef9212 Added new targets for nominal datatype package. berghofe parents: 19404 diff changeset	893	$(LOG)/HOL-Nominal-Examples.gz \
10135 c2a4dccf6e67 reorganized AxClasses; wenzelm parents: 10094 diff changeset	894	$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
16509 20f4c6a950f7 fixed HOL-Complex-Matrix target; wenzelm parents: 16484 diff changeset	895	$(LOG)/HOL-Lattice $(LOG)/HOL-Complex-Matrix \
13980 f254d1c92a6a removed obsolete references to HOL-Real paulson parents: 13967 diff changeset	896	$(LOG)/HOL-Complex.gz \
13961 233dd3bb2390 new directory Complex paulson parents: 13949 diff changeset	897	$(LOG)/HOL-Complex-ex.gz \
14199 d3b8d972a488 new session HOL-SET-Protocol paulson parents: 14182 diff changeset	898	$(LOG)/HOL-Complex-HahnBanach.gz $(LOG)/HOL-SET-Protocol.gz \
d3b8d972a488 new session HOL-SET-Protocol paulson parents: 14182 diff changeset	899	$(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Memory.gz \
10981 8d37c8befbe6 tuned; wenzelm parents: 10980 diff changeset	900	$(LOG)/HOL-Library.gz $(LOG)/HOL-Unix.gz

author	krauss
	Fri, 25 Apr 2008 15:30:33 +0200
changeset 26748	4d51ddd6aa5c
parent 26737	3d46c55f03af
child 26878	1aeac4d6b377
permissions	-rw-r--r--