equal
deleted
inserted
replaced
76 |
76 |
77 ## HOL-Trie |
77 ## HOL-Trie |
78 |
78 |
79 HOL-Trie: HOL $(LOG)/HOL-Trie.gz |
79 HOL-Trie: HOL $(LOG)/HOL-Trie.gz |
80 |
80 |
81 $(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/Option2.thy Trie/Trie.thy |
81 $(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/ROOT.ML Trie/Trie.thy |
82 @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Trie |
82 @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Trie |
83 @rm -f tutorial.dvi |
83 @rm -f tutorial.dvi |
84 |
84 |
85 |
85 |
86 ## HOL-Recdef |
86 ## HOL-Recdef |
152 ## HOL-Misc |
152 ## HOL-Misc |
153 |
153 |
154 HOL-Misc: HOL $(LOG)/HOL-Misc.gz |
154 HOL-Misc: HOL $(LOG)/HOL-Misc.gz |
155 |
155 |
156 $(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \ |
156 $(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \ |
157 Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/types.thy \ |
157 Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/Option2.thy \ |
158 Misc/prime_def.thy Misc/case_exprs.thy \ |
158 Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \ |
159 Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy |
159 Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy |
160 @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Misc |
160 @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Misc |
161 @rm -f tutorial.dvi |
161 @rm -f tutorial.dvi |
162 |
162 |
163 |
163 |