isabelle: src/HOLCF/IsaMakefile@a3abf29660e6 (annotated)

2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	1	#
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	2	# $Id$
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	3	#
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	4	# IsaMakefile for HOLCF
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	5	#
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	6
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	7	#### Base system
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	8
3118 24dae6222579 fixed ISABELLE_OUTPUT, ISABELLE_PATH (finally?); wenzelm parents: 3081 diff changeset	9	OUT = $(ISABELLE_OUTPUT)
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	10
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2571 diff changeset	11	THYS = Porder.thy Porder0.thy Pcpo.thy \
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	12	Fun1.thy Fun2.thy Fun3.thy \
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	13	Cfun1.thy Cfun2.thy Cfun3.thy Cont.thy \
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	14	Cprod1.thy Cprod2.thy Cprod3.thy \
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	15	Sprod0.thy Sprod1.thy Sprod2.thy Sprod3.thy \
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	16	Ssum0.thy Ssum1.thy Ssum2.thy Ssum3.thy \
3350 a3abf29660e6 removed ccc1 slotosch parents: 3324 diff changeset	17	Up1.thy Up2.thy Up3.thy Fix.thy \
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2571 diff changeset	18	One.thy Tr.thy\
2841 c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift" nipkow parents: 2828 diff changeset	19	Discrete0.thy Discrete1.thy Discrete.thy\
3324 6b26b886ff69 Eliminated the prediates flat,chfin slotosch parents: 3190 diff changeset	20	Lift1.thy Lift2.thy Lift3.thy Lift.thy HOLCF.thy
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	21
3324 6b26b886ff69 Eliminated the prediates flat,chfin slotosch parents: 3190 diff changeset	22	ONLYTHYS =
2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2571 diff changeset	23
3028 45204c79ad1d added dependencies on ax_ops/.ML and domain/.ML oheimb parents: 2841 diff changeset	24	FILES = ROOT.ML $(THYS) $(ONLYTHYS) $(THYS:.thy=.ML) \
3043 63a77d6b7eca removed space; wenzelm parents: 3028 diff changeset	25	ax_ops/holcflogic.ML ax_ops/thy_axioms.ML \
3028 45204c79ad1d added dependencies on ax_ops/.ML and domain/.ML oheimb parents: 2841 diff changeset	26	ax_ops/thy_ops.ML ax_ops/thy_syntax.ML \
45204c79ad1d added dependencies on ax_ops/.ML and domain/.ML oheimb parents: 2841 diff changeset	27	domain/library.ML domain/syntax.ML domain/axioms.ML \
45204c79ad1d added dependencies on ax_ops/.ML and domain/.ML oheimb parents: 2841 diff changeset	28	domain/theorems.ML domain/extender.ML domain/interface.ML
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	29
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	30	$(OUT)/HOLCF: $(OUT)/HOL $(FILES)
3057 a5a42ff18a40 removed -c option; wenzelm parents: 3043 diff changeset	31	@$(ISATOOL) usedir -b $(OUT)/HOL HOLCF
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	32	@chmod -w $@
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	33
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	34	$(OUT)/HOL:
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	35	@cd ../HOL; $(ISATOOL) make
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	36
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	37
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	38
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	39	#### Tests and examples
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	40
3081 71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	41	## IOA meta theory and examples
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	42
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	43
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	44	IOA_FILES = IOA/ROOT.ML IOA/meta_theory/Traces.thy \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	45	IOA/meta_theory/Asig.ML IOA/meta_theory/Asig.thy \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	46	IOA/meta_theory/CompoScheds.thy IOA/meta_theory/CompoExecs.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	47	IOA/meta_theory/CompoTraces.thy IOA/meta_theory/CompoScheds.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	48	IOA/meta_theory/CompoTraces.ML IOA/meta_theory/Sequence.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	49	IOA/meta_theory/Seq.thy IOA/meta_theory/RefCorrectness.thy \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	50	IOA/meta_theory/Automata.thy IOA/meta_theory/Traces.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	51	IOA/meta_theory/Seq.ML IOA/meta_theory/RefMappings.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	52	IOA/meta_theory/ShortExecutions.thy IOA/meta_theory/ShortExecutions.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	53	IOA/meta_theory/IOA.thy IOA/meta_theory/IOA.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	54	IOA/meta_theory/Sequence.thy IOA/meta_theory/Automata.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	55	IOA/meta_theory/CompoExecs.thy IOA/meta_theory/RefMappings.thy \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	56	IOA/meta_theory/RefCorrectness.ML IOA/meta_theory/Compositionality.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	57	IOA/meta_theory/Compositionality.thy
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	58
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	59
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	60	IOA_ABP_FILES = IOA/ABP/Abschannel.thy \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	61	IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	62	IOA/ABP/Action.thy IOA/ABP/Check.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	63	IOA/ABP/Correctness.ML IOA/ABP/Correctness.thy \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	64	IOA/ABP/Env.thy IOA/ABP/Impl.thy \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	65	IOA/ABP/Impl_finite.thy IOA/ABP/Lemmas.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	66	IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	67	IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	68	IOA/ABP/Sender.thy IOA/ABP/Spec.thy
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	69
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	70
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	71	IOA_NTP_FILES = IOA/NTP/Abschannel.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	72	IOA/NTP/Abschannel.thy IOA/NTP/Action.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	73	IOA/NTP/Action.thy IOA/NTP/Correctness.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	74	IOA/NTP/Correctness.thy IOA/NTP/Impl.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	75	IOA/NTP/Impl.thy IOA/NTP/Lemmas.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	76	IOA/NTP/Lemmas.thy IOA/NTP/Multiset.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	77	IOA/NTP/Multiset.thy IOA/NTP/Packet.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	78	IOA/NTP/Packet.thy IOA/NTP/ROOT.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	79	IOA/NTP/Receiver.ML IOA/NTP/Receiver.thy \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	80	IOA/NTP/Sender.ML IOA/NTP/Sender.thy \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	81	IOA/NTP/Spec.thy
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	82
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	83
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	84	IOA: $(OUT)/HOLCF $(IOA_FILES)
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	85	@cd IOA; $(ISATOOL) usedir -b $(OUT)/HOLCF IOA
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	86
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	87	IOA_ABP: $(OUT)/IOA $(IOA_ABP_FILES)
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	88	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA ABP
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	89
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	90	IOA_NTP: $(OUT)/IOA $(IOA_NTP_FILES)
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	91	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	92
2797 54ca927b831b Added the HOLCF-based den. sem. of IMP. nipkow parents: 2679 diff changeset	93	## IMP
54ca927b831b Added the HOLCF-based den. sem. of IMP. nipkow parents: 2679 diff changeset	94
54ca927b831b Added the HOLCF-based den. sem. of IMP. nipkow parents: 2679 diff changeset	95	IMP_THYS = IMP/Denotational.thy
54ca927b831b Added the HOLCF-based den. sem. of IMP. nipkow parents: 2679 diff changeset	96	IMP_FILES = IMP/ROOT.ML $(IMP_THYS) $(IMP_THYS:.thy=.ML)
54ca927b831b Added the HOLCF-based den. sem. of IMP. nipkow parents: 2679 diff changeset	97
54ca927b831b Added the HOLCF-based den. sem. of IMP. nipkow parents: 2679 diff changeset	98	IMP: $(OUT)/HOLCF $(IMP_FILES)
2828 13136dc7b9d0 isatool usedir; wenzelm parents: 2797 diff changeset	99	@$(ISATOOL) usedir $(OUT)/HOLCF IMP
2797 54ca927b831b Added the HOLCF-based den. sem. of IMP. nipkow parents: 2679 diff changeset	100
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	101	## Miscellaneous examples
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	102
3190 5aa3756a4bf2 remove Witness.thy; wenzelm parents: 3118 diff changeset	103	EX_THYS = ex/Classlib.thy\
2571 b9f641195b48 reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains oheimb parents: 2494 diff changeset	104	ex/Dnat.thy ex/Dlist.thy ex/Stream.thy\
b9f641195b48 reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains oheimb parents: 2494 diff changeset	105	ex/Dagstuhl.thy ex/Focus_ex.thy ex/Fix2.thy\
b9f641195b48 reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains oheimb parents: 2494 diff changeset	106	ex/Hoare.thy ex/Loop.thy
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	107
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	108	EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	109
2797 54ca927b831b Added the HOLCF-based den. sem. of IMP. nipkow parents: 2679 diff changeset	110	EX: ex/ROOT.ML $(EX_FILES)
2828 13136dc7b9d0 isatool usedir; wenzelm parents: 2797 diff changeset	111	@$(ISATOOL) usedir $(OUT)/HOLCF ex
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	112
2797 54ca927b831b Added the HOLCF-based den. sem. of IMP. nipkow parents: 2679 diff changeset	113	## Full test
54ca927b831b Added the HOLCF-based den. sem. of IMP. nipkow parents: 2679 diff changeset	114
3081 71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	115	test: $(OUT)/HOLCF IOA IOA_ABP IOA_NTP IMP EX
2797 54ca927b831b Added the HOLCF-based den. sem. of IMP. nipkow parents: 2679 diff changeset	116	echo 'Test examples ran successfully' > test
54ca927b831b Added the HOLCF-based den. sem. of IMP. nipkow parents: 2679 diff changeset	117
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	118	.PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF

author	slotosch
	Mon, 26 May 1997 13:51:03 +0200
changeset 3350	a3abf29660e6
parent 3324	6b26b886ff69
child 3505	1cb4ea47d967
permissions	-rw-r--r--