69 Tools/domain/domain_theorems.ML \ |
69 Tools/domain/domain_theorems.ML \ |
70 Tools/fixrec_package.ML \ |
70 Tools/fixrec_package.ML \ |
71 Tools/pcpodef_package.ML \ |
71 Tools/pcpodef_package.ML \ |
72 holcf_logic.ML \ |
72 holcf_logic.ML \ |
73 document/root.tex |
73 document/root.tex |
74 @$(ISATOOL) usedir -b -g true -r $(OUT)/HOL HOLCF |
74 @$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF |
75 |
75 |
76 |
76 |
77 ## HOLCF-IMP |
77 ## HOLCF-IMP |
78 |
78 |
79 HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz |
79 HOLCF-IMP: HOLCF $(LOG)/HOLCF-IMP.gz |
80 |
80 |
81 $(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF IMP/HoareEx.thy \ |
81 $(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF IMP/HoareEx.thy \ |
82 IMP/Denotational.thy IMP/ROOT.ML IMP/document/root.tex |
82 IMP/Denotational.thy IMP/ROOT.ML IMP/document/root.tex |
83 @$(ISATOOL) usedir $(OUT)/HOLCF IMP |
83 @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF IMP |
84 |
84 |
85 |
85 |
86 ## HOLCF-ex |
86 ## HOLCF-ex |
87 |
87 |
88 HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz |
88 HOLCF-ex: HOLCF $(LOG)/HOLCF-ex.gz |
89 |
89 |
90 $(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF ex/Stream.thy ex/Dagstuhl.thy \ |
90 $(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF ex/Stream.thy ex/Dagstuhl.thy \ |
91 ex/Dnat.thy ex/Fix2.thy ex/Focus_ex.thy ex/Hoare.thy ex/Loop.thy \ |
91 ex/Dnat.thy ex/Fix2.thy ex/Focus_ex.thy ex/Hoare.thy ex/Loop.thy \ |
92 ex/ROOT.ML ex/Fixrec_ex.thy ../HOL/Library/Nat_Infinity.thy |
92 ex/ROOT.ML ex/Fixrec_ex.thy ../HOL/Library/Nat_Infinity.thy |
93 @$(ISATOOL) usedir $(OUT)/HOLCF ex |
93 @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex |
94 |
94 |
95 |
95 |
96 ## HOLCF-FOCUS |
96 ## HOLCF-FOCUS |
97 |
97 |
98 HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz |
98 HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz |
99 |
99 |
100 $(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF FOCUS/Fstreams.thy \ |
100 $(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF FOCUS/Fstreams.thy \ |
101 FOCUS/Fstream.thy FOCUS/FOCUS.thy \ |
101 FOCUS/Fstream.thy FOCUS/FOCUS.thy \ |
102 FOCUS/Stream_adm.thy ../HOL/Library/Continuity.thy \ |
102 FOCUS/Stream_adm.thy ../HOL/Library/Continuity.thy \ |
103 FOCUS/Buffer.thy FOCUS/Buffer_adm.thy |
103 FOCUS/Buffer.thy FOCUS/Buffer_adm.thy |
104 @$(ISATOOL) usedir $(OUT)/HOLCF FOCUS |
104 @$(ISABELLE_TOOL) usedir $(OUT)/HOLCF FOCUS |
105 |
105 |
106 ## IOA |
106 ## IOA |
107 |
107 |
108 IOA: HOLCF $(OUT)/IOA |
108 IOA: HOLCF $(OUT)/IOA |
109 |
109 |
116 IOA/meta_theory/RefMappings.thy IOA/meta_theory/Compositionality.thy \ |
116 IOA/meta_theory/RefMappings.thy IOA/meta_theory/Compositionality.thy \ |
117 IOA/meta_theory/TL.thy IOA/meta_theory/TLS.thy \ |
117 IOA/meta_theory/TL.thy IOA/meta_theory/TLS.thy \ |
118 IOA/meta_theory/LiveIOA.thy IOA/meta_theory/Pred.thy \ |
118 IOA/meta_theory/LiveIOA.thy IOA/meta_theory/Pred.thy \ |
119 IOA/meta_theory/Abstraction.thy IOA/meta_theory/Simulations.thy \ |
119 IOA/meta_theory/Abstraction.thy IOA/meta_theory/Simulations.thy \ |
120 IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/ioa_package.ML |
120 IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/ioa_package.ML |
121 @cd IOA; $(ISATOOL) usedir -b $(OUT)/HOLCF IOA |
121 @cd IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA |
122 |
122 |
123 |
123 |
124 ## IOA-ABP |
124 ## IOA-ABP |
125 |
125 |
126 IOA-ABP: IOA $(LOG)/IOA-ABP.gz |
126 IOA-ABP: IOA $(LOG)/IOA-ABP.gz |
130 IOA/ABP/Check.ML IOA/ABP/Correctness.thy \ |
130 IOA/ABP/Check.ML IOA/ABP/Correctness.thy \ |
131 IOA/ABP/Env.thy IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy \ |
131 IOA/ABP/Env.thy IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy \ |
132 IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \ |
132 IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \ |
133 IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy IOA/ABP/Sender.thy \ |
133 IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy IOA/ABP/Sender.thy \ |
134 IOA/ABP/Spec.thy |
134 IOA/ABP/Spec.thy |
135 @cd IOA; $(ISATOOL) usedir $(OUT)/IOA ABP |
135 @cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ABP |
136 |
136 |
137 ## IOA-NTP |
137 ## IOA-NTP |
138 |
138 |
139 IOA-NTP: IOA $(LOG)/IOA-NTP.gz |
139 IOA-NTP: IOA $(LOG)/IOA-NTP.gz |
140 |
140 |
141 $(LOG)/IOA-NTP.gz: $(OUT)/IOA \ |
141 $(LOG)/IOA-NTP.gz: $(OUT)/IOA \ |
142 IOA/NTP/Abschannel.thy IOA/NTP/Action.thy IOA/NTP/Correctness.thy \ |
142 IOA/NTP/Abschannel.thy IOA/NTP/Action.thy IOA/NTP/Correctness.thy \ |
143 IOA/NTP/Impl.thy IOA/NTP/Lemmas.thy IOA/NTP/Multiset.thy \ |
143 IOA/NTP/Impl.thy IOA/NTP/Lemmas.thy IOA/NTP/Multiset.thy \ |
144 IOA/NTP/Packet.thy IOA/NTP/ROOT.ML IOA/NTP/Receiver.thy IOA/NTP/Sender.thy \ |
144 IOA/NTP/Packet.thy IOA/NTP/ROOT.ML IOA/NTP/Receiver.thy IOA/NTP/Sender.thy \ |
145 IOA/NTP/Spec.thy |
145 IOA/NTP/Spec.thy |
146 @cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP |
146 @cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA NTP |
147 |
147 |
148 |
148 |
149 ## IOA-Modelcheck |
149 ## IOA-Modelcheck |
150 |
150 |
151 IOA-Modelcheck: IOA $(LOG)/IOA-Modelcheck.gz |
151 IOA-Modelcheck: IOA $(LOG)/IOA-Modelcheck.gz |
152 |
152 |
153 $(LOG)/IOA-Modelcheck.gz: $(OUT)/IOA IOA/Modelcheck/ROOT.ML \ |
153 $(LOG)/IOA-Modelcheck.gz: $(OUT)/IOA IOA/Modelcheck/ROOT.ML \ |
154 IOA/Modelcheck/Cockpit.thy IOA/Modelcheck/MuIOA.thy \ |
154 IOA/Modelcheck/Cockpit.thy IOA/Modelcheck/MuIOA.thy \ |
155 IOA/Modelcheck/MuIOAOracle.thy IOA/Modelcheck/Ring3.thy |
155 IOA/Modelcheck/MuIOAOracle.thy IOA/Modelcheck/Ring3.thy |
156 @cd IOA; $(ISATOOL) usedir $(OUT)/IOA Modelcheck |
156 @cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA Modelcheck |
157 |
157 |
158 |
158 |
159 ## IOA-Storage |
159 ## IOA-Storage |
160 |
160 |
161 IOA-Storage: IOA $(LOG)/IOA-Storage.gz |
161 IOA-Storage: IOA $(LOG)/IOA-Storage.gz |
162 |
162 |
163 $(LOG)/IOA-Storage.gz: $(OUT)/IOA IOA/Storage/Action.thy \ |
163 $(LOG)/IOA-Storage.gz: $(OUT)/IOA IOA/Storage/Action.thy \ |
164 IOA/Storage/Correctness.thy IOA/Storage/Impl.thy \ |
164 IOA/Storage/Correctness.thy IOA/Storage/Impl.thy \ |
165 IOA/Storage/ROOT.ML IOA/Storage/Spec.thy |
165 IOA/Storage/ROOT.ML IOA/Storage/Spec.thy |
166 @cd IOA; $(ISATOOL) usedir $(OUT)/IOA Storage |
166 @cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA Storage |
167 |
167 |
168 |
168 |
169 ## IOA-ex |
169 ## IOA-ex |
170 |
170 |
171 IOA-ex: IOA $(LOG)/IOA-ex.gz |
171 IOA-ex: IOA $(LOG)/IOA-ex.gz |
172 |
172 |
173 $(LOG)/IOA-ex.gz: $(OUT)/IOA IOA/ex/ROOT.ML IOA/ex/TrivEx.thy IOA/ex/TrivEx2.thy |
173 $(LOG)/IOA-ex.gz: $(OUT)/IOA IOA/ex/ROOT.ML IOA/ex/TrivEx.thy IOA/ex/TrivEx2.thy |
174 @cd IOA; $(ISATOOL) usedir $(OUT)/IOA ex |
174 @cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ex |
175 |
175 |
176 |
176 |
177 ## clean |
177 ## clean |
178 |
178 |
179 clean: |
179 clean: |