isabelle: src/HOLCF/IsaMakefile@7b9b9ba532ca (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
11350 4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: 8602 diff changeset	9	test: HOLCF-IMP HOLCF-ex HOLCF-FOCUS \
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: 8602 diff changeset	10	IOA-ABP IOA-NTP IOA-Modelcheck IOA-Storage IOA-ex
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	11	all: images test
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	12
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	13
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	14	## global settings
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	15
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	16	SRC = $(ISABELLE_HOME)/src
3118 24dae6222579 fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?); wenzelm parents: 3081 diff changeset	17	OUT = $(ISABELLE_OUTPUT)
4447 b7ee449eb345 log files; wenzelm parents: 4129 diff changeset	18	LOG = $(OUT)/log
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	19
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	20
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	21	## HOLCF
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	22
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	23	HOLCF: HOL $(OUT)/HOLCF
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	24
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	25	HOL:
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27420 diff changeset	26	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	27
27420 aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	28	$(OUT)/HOLCF: $(OUT)/HOL \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	29	ROOT.ML \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	30	Adm.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	31	Algebraic.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	32	Bifinite.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	33	Cfun.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	34	CompactBasis.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	35	Completion.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	36	Cont.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	37	ConvexPD.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	38	Cprod.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	39	Discrete.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	40	Deflation.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	41	Domain.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	42	Eventual.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	43	Ffun.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	44	Fixrec.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	45	Fix.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	46	HOLCF.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	47	Lift.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	48	LowerPD.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	49	NatIso.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	50	One.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	51	Pcpodef.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	52	Pcpo.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	53	Porder.thy \
29530 9905b660612b change to simpler, more extensible continuity simproc huffman parents: 29130 diff changeset	54	Product_Cpo.thy \
27420 aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	55	Sprod.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	56	Ssum.thy \
29534 247e4c816004 rename Dsum.thy to Sum_Cpo.thy huffman parents: 29530 diff changeset	57	Sum_Cpo.thy \
27420 aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	58	Tr.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	59	Universal.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	60	UpperPD.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	61	Up.thy \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	62	Tools/adm_tac.ML \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	63	Tools/cont_consts.ML \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	64	Tools/cont_proc.ML \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	65	Tools/domain/domain_extender.ML \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	66	Tools/domain/domain_axioms.ML \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	67	Tools/domain/domain_library.ML \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	68	Tools/domain/domain_syntax.ML \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	69	Tools/domain/domain_theorems.ML \
31738 7b9b9ba532ca discontinued ancient tradition to suffix certain ML module names with "_package" haftmann parents: 30920 diff changeset	70	Tools/fixrec.ML \
7b9b9ba532ca discontinued ancient tradition to suffix certain ML module names with "_package" haftmann parents: 30920 diff changeset	71	Tools/pcpodef.ML \
27420 aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	72	holcf_logic.ML \
aa335405f0c5 put file dependencies on separate lines huffman parents: 27412 diff changeset	73	document/root.tex
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27420 diff changeset	74	@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	75
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	76
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	77	## HOLCF-IMP
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	78
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	79	HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	80
12433 654acbf26fcc HOLCF/IMP converted to Isar kleing parents: 12035 diff changeset	81	$(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF IMP/HoareEx.thy \
12599 8bc47cf91bf6 IMP/document/root.tex; wenzelm parents: 12433 diff changeset	82	IMP/Denotational.thy IMP/ROOT.ML IMP/document/root.tex
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27420 diff changeset	83	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF IMP
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	84
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	85
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	86	## HOLCF-ex
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	87
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	88	HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	89
30920 811ab0923a62 add HOLCF/ex/Domain_ex.thy, with example uses of the domain package huffman parents: 29992 diff changeset	90	$(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF \
811ab0923a62 add HOLCF/ex/Domain_ex.thy, with example uses of the domain package huffman parents: 29992 diff changeset	91	../HOL/Library/Nat_Infinity.thy \
811ab0923a62 add HOLCF/ex/Domain_ex.thy, with example uses of the domain package huffman parents: 29992 diff changeset	92	ex/Dagstuhl.thy \
811ab0923a62 add HOLCF/ex/Domain_ex.thy, with example uses of the domain package huffman parents: 29992 diff changeset	93	ex/Dnat.thy \
811ab0923a62 add HOLCF/ex/Domain_ex.thy, with example uses of the domain package huffman parents: 29992 diff changeset	94	ex/Domain_ex.thy \
811ab0923a62 add HOLCF/ex/Domain_ex.thy, with example uses of the domain package huffman parents: 29992 diff changeset	95	ex/Fix2.thy \
811ab0923a62 add HOLCF/ex/Domain_ex.thy, with example uses of the domain package huffman parents: 29992 diff changeset	96	ex/Fixrec_ex.thy \
811ab0923a62 add HOLCF/ex/Domain_ex.thy, with example uses of the domain package huffman parents: 29992 diff changeset	97	ex/Focus_ex.thy \
811ab0923a62 add HOLCF/ex/Domain_ex.thy, with example uses of the domain package huffman parents: 29992 diff changeset	98	ex/Hoare.thy \
811ab0923a62 add HOLCF/ex/Domain_ex.thy, with example uses of the domain package huffman parents: 29992 diff changeset	99	ex/Loop.thy \
29992 5deee36e33c4 add Powerdomain_ex.thy huffman parents: 29534 diff changeset	100	ex/Powerdomain_ex.thy \
30920 811ab0923a62 add HOLCF/ex/Domain_ex.thy, with example uses of the domain package huffman parents: 29992 diff changeset	101	ex/Stream.thy \
811ab0923a62 add HOLCF/ex/Domain_ex.thy, with example uses of the domain package huffman parents: 29992 diff changeset	102	ex/ROOT.ML
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27420 diff changeset	103	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex
3081 71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	104
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	105
11350 4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: 8602 diff changeset	106	## HOLCF-FOCUS
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: 8602 diff changeset	107
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: 8602 diff changeset	108	HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: 8602 diff changeset	109
15188 9d57263faf9e integrated Streams with ex/Stream.; added FOCUS/Fstreams.thy oheimb* parents: 14535 diff changeset	110	$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF FOCUS/Fstreams.thy \
19759 2d0896653e7a removed legacy ML scripts huffman parents: 19742 diff changeset	111	FOCUS/Fstream.thy FOCUS/FOCUS.thy \
2d0896653e7a removed legacy ML scripts huffman parents: 19742 diff changeset	112	FOCUS/Stream_adm.thy ../HOL/Library/Continuity.thy \
2d0896653e7a removed legacy ML scripts huffman parents: 19742 diff changeset	113	FOCUS/Buffer.thy FOCUS/Buffer_adm.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27420 diff changeset	114	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF FOCUS
11350 4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: 8602 diff changeset	115
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	116	## IOA
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	117
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	118	IOA: HOLCF $(OUT)/IOA
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	119
19741 f65265d71426 removed legacy ML scripts; wenzelm parents: 19740 diff changeset	120	$(OUT)/IOA: $(OUT)/HOLCF IOA/ROOT.ML IOA/meta_theory/Traces.thy \
f65265d71426 removed legacy ML scripts; wenzelm parents: 19740 diff changeset	121	IOA/meta_theory/Asig.thy IOA/meta_theory/CompoScheds.thy \
f65265d71426 removed legacy ML scripts; wenzelm parents: 19740 diff changeset	122	IOA/meta_theory/CompoTraces.thy IOA/meta_theory/Seq.thy \
f65265d71426 removed legacy ML scripts; wenzelm parents: 19740 diff changeset	123	IOA/meta_theory/RefCorrectness.thy IOA/meta_theory/Automata.thy \
f65265d71426 removed legacy ML scripts; wenzelm parents: 19740 diff changeset	124	IOA/meta_theory/ShortExecutions.thy IOA/meta_theory/IOA.thy \
f65265d71426 removed legacy ML scripts; wenzelm parents: 19740 diff changeset	125	IOA/meta_theory/Sequence.thy IOA/meta_theory/CompoExecs.thy \
f65265d71426 removed legacy ML scripts; wenzelm parents: 19740 diff changeset	126	IOA/meta_theory/RefMappings.thy IOA/meta_theory/Compositionality.thy \
f65265d71426 removed legacy ML scripts; wenzelm parents: 19740 diff changeset	127	IOA/meta_theory/TL.thy IOA/meta_theory/TLS.thy \
f65265d71426 removed legacy ML scripts; wenzelm parents: 19740 diff changeset	128	IOA/meta_theory/LiveIOA.thy IOA/meta_theory/Pred.thy \
f65265d71426 removed legacy ML scripts; wenzelm parents: 19740 diff changeset	129	IOA/meta_theory/Abstraction.thy IOA/meta_theory/Simulations.thy \
31738 7b9b9ba532ca discontinued ancient tradition to suffix certain ML module names with "_package" haftmann parents: 30920 diff changeset	130	IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/ioa.ML
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27420 diff changeset	131	@cd IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA
3081 71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	132
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	133
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	134	## IOA-ABP
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	135
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	136	IOA-ABP: IOA $(LOG)/IOA-ABP.gz
3081 71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	137
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	138	$(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	139	IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.thy \
19738 1ac610922636 removed legacy ML scripts; wenzelm parents: 19550 diff changeset	140	IOA/ABP/Check.ML IOA/ABP/Correctness.thy \
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	141	IOA/ABP/Env.thy IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy \
19738 1ac610922636 removed legacy ML scripts; wenzelm parents: 19550 diff changeset	142	IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	143	IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy IOA/ABP/Sender.thy \
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	144	IOA/ABP/Spec.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27420 diff changeset	145	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ABP
3081 71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	146
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	147	## IOA-NTP
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	148
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	149	IOA-NTP: IOA $(LOG)/IOA-NTP.gz
74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	150
19739 c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 19738 diff changeset	151	$(LOG)/IOA-NTP.gz: $(OUT)/IOA \
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 19738 diff changeset	152	IOA/NTP/Abschannel.thy IOA/NTP/Action.thy IOA/NTP/Correctness.thy \
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 19738 diff changeset	153	IOA/NTP/Impl.thy IOA/NTP/Lemmas.thy IOA/NTP/Multiset.thy \
c58ef2aa5430 removed legacy ML scripts; wenzelm parents: 19738 diff changeset	154	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	155	IOA/NTP/Spec.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27420 diff changeset	156	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA NTP
3081 71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	157
3951 d52a49a7d8f3 removed Dlist; wenzelm parents: 3921 diff changeset	158
6475 19e005e2f58d added ex and Modelcheck mueller parents: 6213 diff changeset	159	## IOA-Modelcheck
19e005e2f58d added ex and Modelcheck mueller parents: 6213 diff changeset	160
19e005e2f58d added ex and Modelcheck mueller parents: 6213 diff changeset	161	IOA-Modelcheck: IOA $(LOG)/IOA-Modelcheck.gz
19e005e2f58d added ex and Modelcheck mueller parents: 6213 diff changeset	162
19764 372065f34795 removed obsolete ML files; wenzelm parents: 19759 diff changeset	163	$(LOG)/IOA-Modelcheck.gz: $(OUT)/IOA IOA/Modelcheck/ROOT.ML \
22819 a7b425bb668c removed legacy ML files; wenzelm parents: 20775 diff changeset	164	IOA/Modelcheck/Cockpit.thy IOA/Modelcheck/MuIOA.thy \
a7b425bb668c removed legacy ML files; wenzelm parents: 20775 diff changeset	165	IOA/Modelcheck/MuIOAOracle.thy IOA/Modelcheck/Ring3.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27420 diff changeset	166	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA Modelcheck
6475 19e005e2f58d added ex and Modelcheck mueller parents: 6213 diff changeset	167
19e005e2f58d added ex and Modelcheck mueller parents: 6213 diff changeset	168
6010 fc58d3c1fd62 IOA-Storage: Memory storage case study. wenzelm parents: 4566 diff changeset	169	## IOA-Storage
fc58d3c1fd62 IOA-Storage: Memory storage case study. wenzelm parents: 4566 diff changeset	170
fc58d3c1fd62 IOA-Storage: Memory storage case study. wenzelm parents: 4566 diff changeset	171	IOA-Storage: IOA $(LOG)/IOA-Storage.gz
fc58d3c1fd62 IOA-Storage: Memory storage case study. wenzelm parents: 4566 diff changeset	172
19740 6b38551d0798 removed legacy ML scripts; wenzelm parents: 19739 diff changeset	173	$(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	174	IOA/Storage/Correctness.thy IOA/Storage/Impl.thy \
6011 c48050d6928d tuned; wenzelm parents: 6010 diff changeset	175	IOA/Storage/ROOT.ML IOA/Storage/Spec.thy
28500 4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL; wenzelm parents: 27420 diff changeset	176	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA Storage
6010 fc58d3c1fd62 IOA-Storage: Memory storage case study. wenzelm parents: 4566 diff changeset	177
fc58d3c1fd62 IOA-Storage: Memory storage case study. wenzelm parents: 4566 diff changeset	178
6475 19e005e2f58d added ex and Modelcheck mueller parents: 6213 diff changeset	179	## IOA-ex
19e005e2f58d added ex and Modelcheck mueller parents: 6213 diff changeset	180
19e005e2f58d added ex and Modelcheck mueller parents: 6213 diff changeset	181	IOA-ex: IOA $(LOG)/IOA-ex.gz
19e005e2f58d added ex and Modelcheck mueller parents: 6213 diff changeset	182
19740 6b38551d0798 removed legacy ML scripts; wenzelm parents: 19739 diff changeset	183	$(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	184	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ex
6475 19e005e2f58d added ex and Modelcheck mueller parents: 6213 diff changeset	185
19e005e2f58d added ex and Modelcheck mueller parents: 6213 diff changeset	186
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	187	## clean
4447 b7ee449eb345 log files; wenzelm parents: 4129 diff changeset	188
b7ee449eb345 log files; wenzelm parents: 4129 diff changeset	189	clean:
4518 74c01296e818 improved targets; wenzelm parents: 4447 diff changeset	190	@rm -f $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz \
11350 4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: 8602 diff changeset	191	$(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz \
4c55b020d6ee added FOCUS including the One-Element Buffer by Manfred Broy oheimb parents: 8602 diff changeset	192	$(OUT)/IOA $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz \
6475 19e005e2f58d added ex and Modelcheck mueller parents: 6213 diff changeset	193	$(LOG)/IOA-NTP.gz $(LOG)/IOA-Modelcheck.gz $(LOG)/IOA-Storage.gz

author	haftmann
	Sun, 21 Jun 2009 08:38:58 +0200
changeset 31738	7b9b9ba532ca
parent 30920	811ab0923a62
child 31773	4d33c5d7575b
permissions	-rw-r--r--