2494

1 
#


2 
# $Id$


3 
#


4 
# IsaMakefile for HOLCF


5 
#


6 

4518

7 
## targets

2494

8 

4518

9 
default: HOLCF


10 
images: HOLCF IOA

6010

11 
test: HOLCFIMP HOLCFex IOAABP IOANTP IOAStorage

4518

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 \

4562

82 
IOA/meta_theory/Compositionality.thy \


83 
IOA/meta_theory/TL.thy IOA/meta_theory/TL.ML IOA/meta_theory/TLS.thy \


84 
IOA/meta_theory/TLS.ML IOA/meta_theory/LiveIOA.thy IOA/meta_theory/LiveIOA.ML \


85 
IOA/meta_theory/Pred.thy IOA/meta_theory/Abstraction.thy \


86 
IOA/meta_theory/Abstraction.ML IOA/meta_theory/TrivEx.thy IOA/meta_theory/TrivEx.ML \

4566

87 
IOA/meta_theory/TrivEx2.thy IOA/meta_theory/TrivEx2.ML \


88 
IOA/meta_theory/Simulations.thy IOA/meta_theory/Simulations.ML \


89 
IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/SimCorrectness.ML

4518

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

3081

91 


92 

4518

93 
## IOAABP


94 


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

3081

96 

4518

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


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


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


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


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


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


103 
IOA/ABP/Spec.thy

3081

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


105 

4518

106 


107 
## IOANTP


108 


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


110 


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


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


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


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


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


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


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


118 
IOA/NTP/Spec.thy

3081

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


120 

3951

121 

6010

122 
## IOAStorage


123 


124 
IOAStorage: IOA $(LOG)/IOAStorage.gz


125 


126 
$(LOG)/IOAStorage.gz: IOA/Storage/Action.ML IOA/Storage/Action.thy \


127 
IOA/Storage/Correctness.ML IOA/Storage/Correctness.thy \


128 
IOA/Storage/Impl.ML IOA/Storage/Impl.thy IOA/Storage/ROOT.ML \


129 
IOA/Storage/Spec.thy


130 
@cd IOA; $(ISATOOL) usedir $(OUT)/IOA Storage


131 


132 

4518

133 
## clean

4447

134 


135 
clean:

4518

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


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

6010

138 
$(LOG)/IOANTP.gz $(LOG)/IOAStorage.gz
