equal
deleted
inserted
replaced
149 IMP/Natural.ML IMP/Natural.thy IMP/ROOT.ML IMP/Transition.ML \ |
149 IMP/Natural.ML IMP/Natural.thy IMP/ROOT.ML IMP/Transition.ML \ |
150 IMP/Transition.thy IMP/VC.ML IMP/VC.thy |
150 IMP/Transition.thy IMP/VC.ML IMP/VC.thy |
151 @$(ISATOOL) usedir $(OUT)/HOL IMP |
151 @$(ISATOOL) usedir $(OUT)/HOL IMP |
152 |
152 |
153 |
153 |
|
154 ## HOL-IMPP |
|
155 |
|
156 HOL-IMPP: HOL $(LOG)/HOL-IMPP.gz |
|
157 |
|
158 $(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy IMPP/Com.ML \ |
|
159 IMPP/Natural.thy IMPP/Natural.ML IMPP/Hoare.thy IMPP/Hoare.ML \ |
|
160 IMPP/Misc.thy IMPP/Misc.ML IMPP/EvenOdd.thy IMPP/EvenOdd.ML |
|
161 @$(ISATOOL) usedir $(OUT)/HOL IMPP |
|
162 |
|
163 |
154 ## HOL-Hoare |
164 ## HOL-Hoare |
155 |
165 |
156 HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz |
166 HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz |
157 |
167 |
158 $(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.ML Hoare/Arith2.thy \ |
168 $(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.ML Hoare/Arith2.thy \ |
476 |
486 |
477 ## clean |
487 ## clean |
478 |
488 |
479 clean: |
489 clean: |
480 @rm -f $(OUT)/HOL $(OUT)/HOL-Real $(LOG)/HOL.gz $(LOG)/HOL-Subst.gz \ |
490 @rm -f $(OUT)/HOL $(OUT)/HOL-Real $(LOG)/HOL.gz $(LOG)/HOL-Subst.gz \ |
481 $(LOG)/HOL-Induct.gz $(LOG)/HOL-IMP.gz $(LOG)/HOL-Hoare.gz \ |
491 $(LOG)/HOL-IMP.gz $(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz \ |
482 $(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \ |
492 $(LOG)/HOL-Induct.gz $(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \ |
|
493 $(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \ |
483 $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \ |
494 $(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \ |
484 $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz $(LOG)/HOL-BCV.gz $(LOG)/HOL-IOA.gz \ |
495 $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz $(LOG)/HOL-BCV.gz $(LOG)/HOL-IOA.gz \ |
485 $(LOG)/HOL-AxClasses-Group.gz \ |
496 $(LOG)/HOL-AxClasses-Group.gz \ |
486 $(LOG)/HOL-AxClasses-Lattice.gz \ |
497 $(LOG)/HOL-AxClasses-Lattice.gz \ |
487 $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz \ |
498 $(LOG)/HOL-AxClasses-Tutorial.gz $(LOG)/HOL-Quot.gz \ |