isabelle: src/HOLCF/IsaMakefile@e88ea232977c (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
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	33	$(OUT)/HOL:
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	34	@cd ../HOL; $(ISATOOL) make
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	35
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	#### Tests and examples
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	39
3081 71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	40	## IOA meta theory and examples
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	41
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	IOA_FILES = IOA/ROOT.ML IOA/meta_theory/Traces.thy \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	44	IOA/meta_theory/Asig.ML IOA/meta_theory/Asig.thy \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	45	IOA/meta_theory/CompoScheds.thy IOA/meta_theory/CompoExecs.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	46	IOA/meta_theory/CompoTraces.thy IOA/meta_theory/CompoScheds.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	47	IOA/meta_theory/CompoTraces.ML IOA/meta_theory/Sequence.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	48	IOA/meta_theory/Seq.thy IOA/meta_theory/RefCorrectness.thy \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	49	IOA/meta_theory/Automata.thy IOA/meta_theory/Traces.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	50	IOA/meta_theory/Seq.ML IOA/meta_theory/RefMappings.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	51	IOA/meta_theory/ShortExecutions.thy IOA/meta_theory/ShortExecutions.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	52	IOA/meta_theory/IOA.thy IOA/meta_theory/IOA.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	53	IOA/meta_theory/Sequence.thy IOA/meta_theory/Automata.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	54	IOA/meta_theory/CompoExecs.thy IOA/meta_theory/RefMappings.thy \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	55	IOA/meta_theory/RefCorrectness.ML IOA/meta_theory/Compositionality.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	56	IOA/meta_theory/Compositionality.thy
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	57
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	IOA_ABP_FILES = IOA/ABP/Abschannel.thy \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	60	IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	61	IOA/ABP/Action.thy IOA/ABP/Check.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	62	IOA/ABP/Correctness.ML IOA/ABP/Correctness.thy \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	63	IOA/ABP/Env.thy IOA/ABP/Impl.thy \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	64	IOA/ABP/Impl_finite.thy IOA/ABP/Lemmas.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	65	IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	66	IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	67	IOA/ABP/Sender.thy IOA/ABP/Spec.thy
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	68
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	IOA_NTP_FILES = IOA/NTP/Abschannel.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	71	IOA/NTP/Abschannel.thy IOA/NTP/Action.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	72	IOA/NTP/Action.thy IOA/NTP/Correctness.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	73	IOA/NTP/Correctness.thy IOA/NTP/Impl.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	74	IOA/NTP/Impl.thy IOA/NTP/Lemmas.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	75	IOA/NTP/Lemmas.thy IOA/NTP/Multiset.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	76	IOA/NTP/Multiset.thy IOA/NTP/Packet.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	77	IOA/NTP/Packet.thy IOA/NTP/ROOT.ML \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	78	IOA/NTP/Receiver.ML IOA/NTP/Receiver.thy \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	79	IOA/NTP/Sender.ML IOA/NTP/Sender.thy \
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	80	IOA/NTP/Spec.thy
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	81
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	IOA: $(OUT)/HOLCF $(IOA_FILES)
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	84	@cd IOA; $(ISATOOL) usedir -b $(OUT)/HOLCF IOA
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	85
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	86	IOA_ABP: $(OUT)/IOA $(IOA_ABP_FILES)
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	87	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA ABP
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	88
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	89	IOA_NTP: $(OUT)/IOA $(IOA_NTP_FILES)
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	90	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP
71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	91
2797 54ca927b831b Added the HOLCF-based den. sem. of IMP. nipkow parents: 2679 diff changeset	92	## IMP
54ca927b831b Added the HOLCF-based den. sem. of IMP. nipkow parents: 2679 diff changeset	93
54ca927b831b Added the HOLCF-based den. sem. of IMP. nipkow parents: 2679 diff changeset	94	IMP_THYS = IMP/Denotational.thy
54ca927b831b Added the HOLCF-based den. sem. of IMP. nipkow parents: 2679 diff changeset	95	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	96
54ca927b831b Added the HOLCF-based den. sem. of IMP. nipkow parents: 2679 diff changeset	97	IMP: $(OUT)/HOLCF $(IMP_FILES)
2828 13136dc7b9d0 isatool usedir; wenzelm parents: 2797 diff changeset	98	@$(ISATOOL) usedir $(OUT)/HOLCF IMP
2797 54ca927b831b Added the HOLCF-based den. sem. of IMP. nipkow parents: 2679 diff changeset	99
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	100	## Miscellaneous examples
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	101
3921 e88ea232977c removed Classlib; wenzelm parents: 3505 diff changeset	102	EX_THYS = ex/Dnat.thy ex/Dlist.thy ex/Stream.thy \
e88ea232977c removed Classlib; wenzelm parents: 3505 diff changeset	103	ex/Dagstuhl.thy ex/Focus_ex.thy ex/Fix2.thy \
2571 b9f641195b48 reflecting the changes made in HOLCF/ex and HOLCF/explicit_domains oheimb parents: 2494 diff changeset	104	ex/Hoare.thy ex/Loop.thy
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	105
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	106	EX_FILES = ex/ROOT.ML ex/loeckx.ML $(EX_THYS) $(EX_THYS:.thy=.ML)
5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	107
2797 54ca927b831b Added the HOLCF-based den. sem. of IMP. nipkow parents: 2679 diff changeset	108	EX: ex/ROOT.ML $(EX_FILES)
2828 13136dc7b9d0 isatool usedir; wenzelm parents: 2797 diff changeset	109	@$(ISATOOL) usedir $(OUT)/HOLCF ex
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	110
2797 54ca927b831b Added the HOLCF-based den. sem. of IMP. nipkow parents: 2679 diff changeset	111	## Full test
54ca927b831b Added the HOLCF-based den. sem. of IMP. nipkow parents: 2679 diff changeset	112
3081 71c54eb8ed1d added IOA (meta theory and ABP, NTP examples); mueller parents: 3057 diff changeset	113	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	114	echo 'Test examples ran successfully' > test
54ca927b831b Added the HOLCF-based den. sem. of IMP. nipkow parents: 2679 diff changeset	115
2494 5d45c2094ff6 IsaMakefile for HOLCF; wenzelm parents: diff changeset	116	.PRECIOUS: $(OUT)/HOL $(OUT)/HOLCF

author	wenzelm
	Fri, 17 Oct 1997 17:33:22 +0200
changeset 3921	e88ea232977c
parent 3505	1cb4ea47d967
child 3951	d52a49a7d8f3
permissions	-rw-r--r--