2494

1 
#


2 
# $Id$


3 
#


4 
# IsaMakefile for HOLCF


5 
#


6 

4518

7 
## targets

2494

8 

4518

9 
default: HOLCF


10 
images: HOLCF IOA


11 
test: HOLCFIMP HOLCFex IOAABP IOANTP


12 
all: images test


13 


14 


15 
## global settings


16 


17 
SRC = $(ISABELLE_HOME)/src

3118

18 
OUT = $(ISABELLE_OUTPUT)

4447

19 
LOG = $(OUT)/log

2494

20 

4518

21 


22 
## HOLCF


23 


24 
HOLCF: HOL $(OUT)/HOLCF


25 


26 
HOL:


27 
@cd $(SRC)/HOL; $(ISATOOL) make HOL

2494

28 

4518

29 
$(OUT)/HOLCF: $(OUT)/HOL Cfun1.ML Cfun1.thy Cfun2.ML Cfun2.thy \


30 
Cfun3.ML Cfun3.thy Cont.ML Cont.thy Cprod1.ML Cprod1.thy Cprod2.ML \


31 
Cprod2.thy Cprod3.ML Cprod3.thy Discrete.ML Discrete.thy Discrete0.ML \


32 
Discrete0.thy Discrete1.ML Discrete1.thy Fix.ML Fix.thy Fun1.ML \


33 
Fun1.thy Fun2.ML Fun2.thy Fun3.ML Fun3.thy HOLCF.ML HOLCF.thy Lift.ML \


34 
Lift.thy Lift1.ML Lift1.thy Lift2.ML Lift2.thy Lift3.ML Lift3.thy \


35 
One.ML One.thy Pcpo.ML Pcpo.thy Porder.ML Porder.thy Porder0.ML \


36 
Porder0.thy ROOT.ML Sprod0.ML Sprod0.thy Sprod1.ML Sprod1.thy \


37 
Sprod2.ML Sprod2.thy Sprod3.ML Sprod3.thy Ssum0.ML Ssum0.thy Ssum1.ML \


38 
Ssum1.thy Ssum2.ML Ssum2.thy Ssum3.ML Ssum3.thy Tr.ML Tr.thy Up1.ML \


39 
Up1.thy Up2.ML Up2.thy Up3.ML Up3.thy adm.ML cont_consts.ML \


40 
domain/axioms.ML domain/extender.ML domain/interface.ML \


41 
domain/library.ML domain/syntax.ML domain/theorems.ML holcf_logic.ML

3057

42 
@$(ISATOOL) usedir b $(OUT)/HOL HOLCF

2494

43 

4518

44 


45 
## HOLCFIMP

2494

46 

4518

47 
HOLCFIMP: HOLCF $(LOG)/HOLCFIMP.gz


48 


49 
$(LOG)/HOLCFIMP.gz: $(OUT)/HOLCF IMP/Denotational.ML \


50 
IMP/Denotational.thy IMP/ROOT.ML


51 
@$(ISATOOL) usedir $(OUT)/HOLCF IMP

2494

52 


53 

4518

54 
## HOLCFex


55 


56 
HOLCFex: HOLCF $(LOG)/HOLCFex.gz

2494

57 

4518

58 
$(LOG)/HOLCFex.gz: $(OUT)/HOLCF ex/Dagstuhl.ML ex/Dagstuhl.thy \


59 
ex/Dnat.ML ex/Dnat.thy ex/Fix2.ML ex/Fix2.thy ex/Focus_ex.ML \


60 
ex/Focus_ex.thy ex/Hoare.ML ex/Hoare.thy ex/Loop.ML ex/Loop.thy \


61 
ex/ROOT.ML ex/Stream.ML ex/Stream.thy ex/loeckx.ML


62 
@$(ISATOOL) usedir $(OUT)/HOLCF ex

3081

63 


64 

4518

65 
## IOA


66 


67 
IOA: HOLCF $(OUT)/IOA


68 


69 
$(OUT)/IOA: $(OUT)/HOLCF IOA/ROOT.ML IOA/meta_theory/Traces.thy \

3081

70 
IOA/meta_theory/Asig.ML IOA/meta_theory/Asig.thy \


71 
IOA/meta_theory/CompoScheds.thy IOA/meta_theory/CompoExecs.ML \


72 
IOA/meta_theory/CompoTraces.thy IOA/meta_theory/CompoScheds.ML \


73 
IOA/meta_theory/CompoTraces.ML IOA/meta_theory/Sequence.ML \


74 
IOA/meta_theory/Seq.thy IOA/meta_theory/RefCorrectness.thy \


75 
IOA/meta_theory/Automata.thy IOA/meta_theory/Traces.ML \


76 
IOA/meta_theory/Seq.ML IOA/meta_theory/RefMappings.ML \


77 
IOA/meta_theory/ShortExecutions.thy IOA/meta_theory/ShortExecutions.ML \


78 
IOA/meta_theory/IOA.thy IOA/meta_theory/IOA.ML \


79 
IOA/meta_theory/Sequence.thy IOA/meta_theory/Automata.ML \


80 
IOA/meta_theory/CompoExecs.thy IOA/meta_theory/RefMappings.thy \


81 
IOA/meta_theory/RefCorrectness.ML IOA/meta_theory/Compositionality.ML \


82 
IOA/meta_theory/Compositionality.thy

4518

83 
@cd IOA; $(ISATOOL) usedir b $(OUT)/HOLCF IOA

3081

84 


85 

4518

86 
## IOAABP


87 


88 
IOAABP: IOA $(LOG)/IOAABP.gz

3081

89 

4518

90 
$(LOG)/IOAABP.gz: $(OUT)/IOA IOA/ABP/Abschannel.thy \


91 
IOA/ABP/Abschannel_finite.thy IOA/ABP/Action.ML IOA/ABP/Action.thy \


92 
IOA/ABP/Check.ML IOA/ABP/Correctness.ML IOA/ABP/Correctness.thy \


93 
IOA/ABP/Env.thy IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy \


94 
IOA/ABP/Lemmas.ML IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \


95 
IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy IOA/ABP/Sender.thy \


96 
IOA/ABP/Spec.thy

3081

97 
@cd IOA; $(ISATOOL) usedir $(OUT)/IOA ABP


98 

4518

99 


100 
## IOANTP


101 


102 
IOANTP: IOA $(LOG)/IOANTP.gz


103 


104 
$(LOG)/IOANTP.gz: $(OUT)/IOA IOA/NTP/Abschannel.ML \


105 
IOA/NTP/Abschannel.thy IOA/NTP/Action.ML IOA/NTP/Action.thy \


106 
IOA/NTP/Correctness.ML IOA/NTP/Correctness.thy IOA/NTP/Impl.ML \


107 
IOA/NTP/Impl.thy IOA/NTP/Lemmas.ML IOA/NTP/Lemmas.thy \


108 
IOA/NTP/Multiset.ML IOA/NTP/Multiset.thy IOA/NTP/Packet.ML \


109 
IOA/NTP/Packet.thy IOA/NTP/ROOT.ML IOA/NTP/Receiver.ML \


110 
IOA/NTP/Receiver.thy IOA/NTP/Sender.ML IOA/NTP/Sender.thy \


111 
IOA/NTP/Spec.thy

3081

112 
@cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP


113 

3951

114 

4518

115 
## clean

4447

116 


117 
clean:

4518

118 
@rm f $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCFIMP.gz \


119 
$(LOG)/HOLCFex.gz $(OUT)/IOA $(LOG)/IOA.gz $(LOG)/IOAABP.gz \


120 
$(LOG)/IOANTP.gz
