isabelle: src/HOL/HOLCF/IsaMakefile@6f215c2ebd72 (annotated)

2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	1	#
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	2	# IsaMakefile for HOLCF
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	3	#
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	4
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	5	## targets
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	6
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	7	default: HOLCF
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	8	images: HOLCF IOA
37779 982b0668dcbd removed old HOL/HOLCF-Modelcheck setup, which has been unused/untested for many years; wenzelm parents: 37119 diff changeset	9	test: \
982b0668dcbd removed old HOL/HOLCF-Modelcheck setup, which has been unused/untested for many years; wenzelm parents: 37119 diff changeset	10	HOLCF-FOCUS \
982b0668dcbd removed old HOL/HOLCF-Modelcheck setup, which has been unused/untested for many years; wenzelm parents: 37119 diff changeset	11	HOLCF-IMP \
37110 7ffdbc24b27f move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path huffman parents: 37109 diff changeset	12	HOLCF-Library \
37000 41a22e7c1145 move some example files into new HOLCF/Tutorial directory huffman parents: 35932 diff changeset	13	HOLCF-Tutorial \
37779 982b0668dcbd removed old HOL/HOLCF-Modelcheck setup, which has been unused/untested for many years; wenzelm parents: 37119 diff changeset	14	HOLCF-ex \
982b0668dcbd removed old HOL/HOLCF-Modelcheck setup, which has been unused/untested for many years; wenzelm parents: 37119 diff changeset	15	IOA-ABP \
982b0668dcbd removed old HOL/HOLCF-Modelcheck setup, which has been unused/untested for many years; wenzelm parents: 37119 diff changeset	16	IOA-NTP \
982b0668dcbd removed old HOL/HOLCF-Modelcheck setup, which has been unused/untested for many years; wenzelm parents: 37119 diff changeset	17	IOA-Storage \
982b0668dcbd removed old HOL/HOLCF-Modelcheck setup, which has been unused/untested for many years; wenzelm parents: 37119 diff changeset	18	IOA-ex
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	19	all: images test
45860 93eda35a8377 more visible benchmarks; wenzelm parents: 43919 diff changeset	20	full: all
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	21
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	22
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	23	## global settings
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	24
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	25	SRC = $(ISABELLE_HOME)/src
3118 24dae6222579 fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?); wenzelm parents: 3081 diff changeset	26	OUT = $(ISABELLE_OUTPUT)
4447 b7ee449eb345 log files; wenzelm parents: 4129 diff changeset	27	LOG = $(OUT)/log
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	28
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	29
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	30	## HOLCF
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	31
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	32	HOLCF: HOL $(OUT)/HOLCF
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	33
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	34	HOL:
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27420 diff changeset	35	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	36
27420 aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	37	$(OUT)/HOLCF: $(OUT)/HOL \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	38	ROOT.ML \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	39	Adm.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	40	Algebraic.thy \
41286 3d7685a4a5ff reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9) huffman parents: 41285 diff changeset	41	Bifinite.thy \
27420 aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	42	Cfun.thy \
41284 6d66975b711f renamed CompactBasis.thy to Compact_Basis.thy huffman parents: 41112 diff changeset	43	Compact_Basis.thy \
27420 aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	44	Completion.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	45	Cont.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	46	ConvexPD.thy \
40772 c8b52f9e1680 rename Pcpodef.thy to Cpodef.thy; huffman parents: 40592 diff changeset	47	Cpodef.thy \
27420 aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	48	Cprod.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	49	Discrete.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	50	Deflation.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	51	Domain.thy \
35652 05ca920cd94b move take-proofs stuff into new theory Domain_Aux.thy huffman parents: 35530 diff changeset	52	Domain_Aux.thy \
27420 aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	53	Fixrec.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	54	Fix.thy \
40001 666c3751227c rename Ffun.thy to Fun_Cpo.thy huffman parents: 39999 diff changeset	55	Fun_Cpo.thy \
27420 aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	56	HOLCF.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	57	Lift.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	58	LowerPD.thy \
40502 8e92772bc0e8 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF huffman parents: 40040 diff changeset	59	Map_Functions.thy \
27420 aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	60	One.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	61	Pcpo.thy \
40502 8e92772bc0e8 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF huffman parents: 40040 diff changeset	62	Plain_HOLCF.thy \
27420 aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	63	Porder.thy \
35473 c4d3d65856dd move some powerdomain stuff into a new file huffman parents: 35214 diff changeset	64	Powerdomains.thy \
29530 9905b660612b change to simpler, more extensible continuity simproc huffman parents: 29130 diff changeset	65	Product_Cpo.thy \
41285 efd23c1d9886 renamed Bifinite.thy to Representable.thy huffman parents: 41284 diff changeset	66	Representable.thy \
40592 f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain huffman parents: 40575 diff changeset	67	Sfun.thy \
27420 aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	68	Sprod.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	69	Ssum.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	70	Tr.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	71	Universal.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	72	UpperPD.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	73	Up.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	74	Tools/cont_consts.ML \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	75	Tools/cont_proc.ML \
35475 979019ab92eb move common functions into new file holcf_library.ML huffman parents: 35473 diff changeset	76	Tools/holcf_library.ML \
40040 3adb92ee2f22 rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML huffman parents: 40026 diff changeset	77	Tools/Domain/domain.ML \
32126 a5042f260440 obey captialized directory names convention haftmann parents: 31773 diff changeset	78	Tools/Domain/domain_axioms.ML \
35473 c4d3d65856dd move some powerdomain stuff into a new file huffman parents: 35214 diff changeset	79	Tools/Domain/domain_constructors.ML \
40040 3adb92ee2f22 rename domain_theorems.ML to domain_induction.ML; rename domain_extender.ML to domain.ML huffman parents: 40026 diff changeset	80	Tools/Domain/domain_induction.ML \
33795 aa5cf0de1503 add dependency on domain_isomorphism.ML huffman parents: 33783 diff changeset	81	Tools/Domain/domain_isomorphism.ML \
35530 3bf57d8cb58d update HOLCF makefile huffman parents: 35475 diff changeset	82	Tools/Domain/domain_take_proofs.ML \
40772 c8b52f9e1680 rename Pcpodef.thy to Cpodef.thy; huffman parents: 40592 diff changeset	83	Tools/cpodef.ML \
40575 b9a86f15e763 rename 'repdef' to 'domaindef' huffman parents: 40504 diff changeset	84	Tools/domaindef.ML \
31738 7b9b9ba532ca discontinued ancient tradition to suffix certain ML module names with "_package" haftmann parents: 30920 diff changeset	85	Tools/fixrec.ML \
27420 aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	86	document/root.tex
40774 0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40772 diff changeset	87	@$(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOLCF
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	88
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	89
37000 41a22e7c1145 move some example files into new HOLCF/Tutorial directory huffman parents: 35932 diff changeset	90	## HOLCF-Tutorial
41a22e7c1145 move some example files into new HOLCF/Tutorial directory huffman parents: 35932 diff changeset	91
41a22e7c1145 move some example files into new HOLCF/Tutorial directory huffman parents: 35932 diff changeset	92	HOLCF-Tutorial: HOLCF $(LOG)/HOLCF-Tutorial.gz
41a22e7c1145 move some example files into new HOLCF/Tutorial directory huffman parents: 35932 diff changeset	93
41a22e7c1145 move some example files into new HOLCF/Tutorial directory huffman parents: 35932 diff changeset	94	$(LOG)/HOLCF-Tutorial.gz: $(OUT)/HOLCF \
41a22e7c1145 move some example files into new HOLCF/Tutorial directory huffman parents: 35932 diff changeset	95	Tutorial/Domain_ex.thy \
41a22e7c1145 move some example files into new HOLCF/Tutorial directory huffman parents: 35932 diff changeset	96	Tutorial/Fixrec_ex.thy \
41a22e7c1145 move some example files into new HOLCF/Tutorial directory huffman parents: 35932 diff changeset	97	Tutorial/New_Domain.thy \
41a22e7c1145 move some example files into new HOLCF/Tutorial directory huffman parents: 35932 diff changeset	98	Tutorial/document/root.tex \
41a22e7c1145 move some example files into new HOLCF/Tutorial directory huffman parents: 35932 diff changeset	99	Tutorial/ROOT.ML
41a22e7c1145 move some example files into new HOLCF/Tutorial directory huffman parents: 35932 diff changeset	100	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Tutorial
41a22e7c1145 move some example files into new HOLCF/Tutorial directory huffman parents: 35932 diff changeset	101
41a22e7c1145 move some example files into new HOLCF/Tutorial directory huffman parents: 35932 diff changeset	102
37110 7ffdbc24b27f move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path huffman parents: 37109 diff changeset	103	## HOLCF-Library
7ffdbc24b27f move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path huffman parents: 37109 diff changeset	104
7ffdbc24b27f move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path huffman parents: 37109 diff changeset	105	HOLCF-Library: HOLCF $(LOG)/HOLCF-Library.gz
7ffdbc24b27f move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path huffman parents: 37109 diff changeset	106
7ffdbc24b27f move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path huffman parents: 37109 diff changeset	107	$(LOG)/HOLCF-Library.gz: $(OUT)/HOLCF \
39999 e3948547b541 add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite huffman parents: 39974 diff changeset	108	Library/Defl_Bifinite.thy \
41112 866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types huffman parents: 40774 diff changeset	109	Library/Bool_Discrete.thy \
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types huffman parents: 40774 diff changeset	110	Library/Char_Discrete.thy \
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types huffman parents: 40774 diff changeset	111	Library/HOL_Cpo.thy \
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types huffman parents: 40774 diff changeset	112	Library/Int_Discrete.thy \
39143 d80990d8b909 add List_Cpo.thy to HOLCF/Library huffman parents: 38137 diff changeset	113	Library/List_Cpo.thy \
41112 866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types huffman parents: 40774 diff changeset	114	Library/List_Predomain.thy \
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types huffman parents: 40774 diff changeset	115	Library/Nat_Discrete.thy \
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types huffman parents: 40774 diff changeset	116	Library/Option_Cpo.thy \
37110 7ffdbc24b27f move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path huffman parents: 37109 diff changeset	117	Library/Stream.thy \
37111 3f84f1f4de64 move HOLCF/Sum_Cpo.thy to HOLCF/Library huffman parents: 37110 diff changeset	118	Library/Sum_Cpo.thy \
37110 7ffdbc24b27f move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path huffman parents: 37109 diff changeset	119	Library/HOLCF_Library.thy \
38137 6fda94059baa renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1); wenzelm parents: 37785 diff changeset	120	Library/ROOT.ML
6fda94059baa renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1); wenzelm parents: 37785 diff changeset	121	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF Library
37110 7ffdbc24b27f move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path huffman parents: 37109 diff changeset	122
7ffdbc24b27f move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path huffman parents: 37109 diff changeset	123
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	124	## HOLCF-IMP
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	125
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	126	HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	127
12433 654acbf26fcc HOLCF/IMP converted to Isar kleing parents: 12035 diff changeset	128	$(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF IMP/HoareEx.thy \
12599 8bc47cf91bf6 IMP/document/root.tex; wenzelm parents: 12433 diff changeset	129	IMP/Denotational.thy IMP/ROOT.ML IMP/document/root.tex
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27420 diff changeset	130	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF IMP
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	131
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	132
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	133	## HOLCF-ex
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	134
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	135	HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	136
30920 811ab0923a62 add HOLCF/ex/Domain_ex.thy, with example uses of the domain package huffman parents: 29992 diff changeset	137	$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF \
43919 a7e4fb1a0502 rename Nat_Infinity (inat) to Extended_Nat (enat) hoelzl parents: 43524 diff changeset	138	../Library/Extended_Nat.thy \
43524 d75e285fcf3e add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis huffman parents: 41286 diff changeset	139	ex/Concurrency_Monad.thy \
30920 811ab0923a62 add HOLCF/ex/Domain_ex.thy, with example uses of the domain package huffman parents: 29992 diff changeset	140	ex/Dagstuhl.thy \
811ab0923a62 add HOLCF/ex/Domain_ex.thy, with example uses of the domain package huffman parents: 29992 diff changeset	141	ex/Dnat.thy \
35167 eba22d68a0a7 add theory HOLCF/ex/Strict_Fun.thy huffman parents: 33813 diff changeset	142	ex/Domain_Proofs.thy \
30920 811ab0923a62 add HOLCF/ex/Domain_ex.thy, with example uses of the domain package huffman parents: 29992 diff changeset	143	ex/Fix2.thy \
811ab0923a62 add HOLCF/ex/Domain_ex.thy, with example uses of the domain package huffman parents: 29992 diff changeset	144	ex/Focus_ex.thy \
811ab0923a62 add HOLCF/ex/Domain_ex.thy, with example uses of the domain package huffman parents: 29992 diff changeset	145	ex/Hoare.thy \
35932 86559356502d move letrec stuff to new file HOLCF/ex/Letrec.thy huffman parents: 35908 diff changeset	146	ex/Letrec.thy \
30920 811ab0923a62 add HOLCF/ex/Domain_ex.thy, with example uses of the domain package huffman parents: 29992 diff changeset	147	ex/Loop.thy \
37109 e67760c1b851 move unused pattern match syntax stuff into HOLCF/ex huffman parents: 37000 diff changeset	148	ex/Pattern_Match.thy \
29992 5deee36e33c4 add Powerdomain_ex.thy huffman parents: 29534 diff changeset	149	ex/Powerdomain_ex.thy \
30920 811ab0923a62 add HOLCF/ex/Domain_ex.thy, with example uses of the domain package huffman parents: 29992 diff changeset	150	ex/ROOT.ML
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27420 diff changeset	151	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex
3081 71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	152
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	153
11350 4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: 8602 diff changeset	154	## HOLCF-FOCUS
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: 8602 diff changeset	155
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: 8602 diff changeset	156	HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: 8602 diff changeset	157
35214 67689d276c70 HOLCF-FOCUS depends on ex/Stream.thy huffman parents: 35167 diff changeset	158	$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF \
37110 7ffdbc24b27f move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path huffman parents: 37109 diff changeset	159	Library/Stream.thy \
35214 67689d276c70 HOLCF-FOCUS depends on ex/Stream.thy huffman parents: 35167 diff changeset	160	FOCUS/Fstreams.thy \
19759 2d0896653e7a removed legacy ML scripts huffman parents: 19742 diff changeset	161	FOCUS/Fstream.thy FOCUS/FOCUS.thy \
40774 0437dbc127b3 moved directory src/HOLCF to src/HOL/HOLCF; huffman parents: 40772 diff changeset	162	FOCUS/Stream_adm.thy ../Library/Continuity.thy \
19759 2d0896653e7a removed legacy ML scripts huffman parents: 19742 diff changeset	163	FOCUS/Buffer.thy FOCUS/Buffer_adm.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27420 diff changeset	164	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF FOCUS
11350 4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: 8602 diff changeset	165
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	166	## IOA
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	167
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	168	IOA: HOLCF $(OUT)/IOA
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	169
19741 f65265d71426 removed legacy ML scripts; wenzelm parents: 19740 diff changeset	170	$(OUT)/IOA: $(OUT)/HOLCF IOA/ROOT.ML IOA/meta_theory/Traces.thy \
f65265d71426 removed legacy ML scripts; wenzelm parents: 19740 diff changeset	171	IOA/meta_theory/Asig.thy IOA/meta_theory/CompoScheds.thy \
f65265d71426 removed legacy ML scripts; wenzelm parents: 19740 diff changeset	172	IOA/meta_theory/CompoTraces.thy IOA/meta_theory/Seq.thy \
f65265d71426 removed legacy ML scripts; wenzelm parents: 19740 diff changeset	173	IOA/meta_theory/RefCorrectness.thy IOA/meta_theory/Automata.thy \
f65265d71426 removed legacy ML scripts; wenzelm parents: 19740 diff changeset	174	IOA/meta_theory/ShortExecutions.thy IOA/meta_theory/IOA.thy \
f65265d71426 removed legacy ML scripts; wenzelm parents: 19740 diff changeset	175	IOA/meta_theory/Sequence.thy IOA/meta_theory/CompoExecs.thy \
f65265d71426 removed legacy ML scripts; wenzelm parents: 19740 diff changeset	176	IOA/meta_theory/RefMappings.thy IOA/meta_theory/Compositionality.thy \
f65265d71426 removed legacy ML scripts; wenzelm parents: 19740 diff changeset	177	IOA/meta_theory/TL.thy IOA/meta_theory/TLS.thy \
f65265d71426 removed legacy ML scripts; wenzelm parents: 19740 diff changeset	178	IOA/meta_theory/LiveIOA.thy IOA/meta_theory/Pred.thy \
f65265d71426 removed legacy ML scripts; wenzelm parents: 19740 diff changeset	179	IOA/meta_theory/Abstraction.thy IOA/meta_theory/Simulations.thy \
37785 173667d73115 removed unused/untested IOA 'automaton' package; wenzelm parents: 37779 diff changeset	180	IOA/meta_theory/SimCorrectness.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27420 diff changeset	181	@cd IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA
3081 71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	182
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	183
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	184	## IOA-ABP
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	185
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	186	IOA-ABP: IOA $(LOG)/IOA-ABP.gz
3081 71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	187
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	188	$(LOG)/IOA-ABP.gz: $(OUT)/IOA IOA/ABP/Abschannel.thy \
8602 f077613e8e7b mods because of weak_case_cong -> removed Action.ML twice nipkow parents: 6475 diff changeset	189	IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.thy \
19738 1ac610922636 removed legacy ML scripts; wenzelm parents: 19550 diff changeset	190	IOA/ABP/Check.ML IOA/ABP/Correctness.thy \
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	191	IOA/ABP/Env.thy IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy \
19738 1ac610922636 removed legacy ML scripts; wenzelm parents: 19550 diff changeset	192	IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	193	IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy IOA/ABP/Sender.thy \
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	194	IOA/ABP/Spec.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27420 diff changeset	195	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ABP
3081 71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	196
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	197	## IOA-NTP
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	198
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	199	IOA-NTP: IOA $(LOG)/IOA-NTP.gz
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	200
19739 c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 19738 diff changeset	201	$(LOG)/IOA-NTP.gz: $(OUT)/IOA \
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 19738 diff changeset	202	IOA/NTP/Abschannel.thy IOA/NTP/Action.thy IOA/NTP/Correctness.thy \
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 19738 diff changeset	203	IOA/NTP/Impl.thy IOA/NTP/Lemmas.thy IOA/NTP/Multiset.thy \
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 19738 diff changeset	204	IOA/NTP/Packet.thy IOA/NTP/ROOT.ML IOA/NTP/Receiver.thy IOA/NTP/Sender.thy \
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	205	IOA/NTP/Spec.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27420 diff changeset	206	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA NTP
3081 71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	207
3951 d52a49a7d8f3 removed Dlist; wenzelm parents: 3921 diff changeset	208
6010 fc58d3c1fd62 IOA-Storage: Memory storage case study. wenzelm parents: 4566 diff changeset	209	## IOA-Storage
fc58d3c1fd62 IOA-Storage: Memory storage case study. wenzelm parents: 4566 diff changeset	210
fc58d3c1fd62 IOA-Storage: Memory storage case study. wenzelm parents: 4566 diff changeset	211	IOA-Storage: IOA $(LOG)/IOA-Storage.gz
fc58d3c1fd62 IOA-Storage: Memory storage case study. wenzelm parents: 4566 diff changeset	212
19740 6b38551d0798 removed legacy ML scripts; wenzelm parents: 19739 diff changeset	213	$(LOG)/IOA-Storage.gz: $(OUT)/IOA IOA/Storage/Action.thy \
17238 b1cf9189104e removed IOA/Storage/Impl.ML, IOA/Storage/Action.ML; wenzelm parents: 16698 diff changeset	214	IOA/Storage/Correctness.thy IOA/Storage/Impl.thy \
6011 c48050d6928d tuned; wenzelm parents: 6010 diff changeset	215	IOA/Storage/ROOT.ML IOA/Storage/Spec.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27420 diff changeset	216	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA Storage
6010 fc58d3c1fd62 IOA-Storage: Memory storage case study. wenzelm parents: 4566 diff changeset	217
fc58d3c1fd62 IOA-Storage: Memory storage case study. wenzelm parents: 4566 diff changeset	218
6475 19e005e2f58d added ex and Modelcheck mueller parents: 6213 diff changeset	219	## IOA-ex
19e005e2f58d added ex and Modelcheck mueller parents: 6213 diff changeset	220
19e005e2f58d added ex and Modelcheck mueller parents: 6213 diff changeset	221	IOA-ex: IOA $(LOG)/IOA-ex.gz
19e005e2f58d added ex and Modelcheck mueller parents: 6213 diff changeset	222
19740 6b38551d0798 removed legacy ML scripts; wenzelm parents: 19739 diff changeset	223	$(LOG)/IOA-ex.gz: $(OUT)/IOA IOA/ex/ROOT.ML IOA/ex/TrivEx.thy IOA/ex/TrivEx2.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27420 diff changeset	224	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ex
6475 19e005e2f58d added ex and Modelcheck mueller parents: 6213 diff changeset	225
19e005e2f58d added ex and Modelcheck mueller parents: 6213 diff changeset	226
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	227	## clean
4447 b7ee449eb345 log files; wenzelm parents: 4129 diff changeset	228
b7ee449eb345 log files; wenzelm parents: 4129 diff changeset	229	clean:
33450 4389ec600ba7 more accurate cleanup; wenzelm parents: 32126 diff changeset	230	@rm -f $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz \
4389ec600ba7 more accurate cleanup; wenzelm parents: 32126 diff changeset	231	$(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA \
4389ec600ba7 more accurate cleanup; wenzelm parents: 32126 diff changeset	232	$(LOG)/IOA.gz $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz \
37779 982b0668dcbd removed old HOL/HOLCF-Modelcheck setup, which has been unused/untested for many years; wenzelm parents: 37119 diff changeset	233	$(LOG)/IOA-Storage.gz $(LOG)/HOLCF-Library.gz \
37000 41a22e7c1145 move some example files into new HOLCF/Tutorial directory huffman parents: 35932 diff changeset	234	$(LOG)/IOA-ex.gz $(LOG)/HOLCF-Tutorial.gz

author	sultana
	Tue, 17 Apr 2012 16:14:06 +0100
changeset 47509	6f215c2ebd72
parent 45860	93eda35a8377
permissions	-rw-r--r--