equal
deleted
inserted
replaced
1297 ## HOL-Quotient_Examples |
1297 ## HOL-Quotient_Examples |
1298 |
1298 |
1299 HOL-Quotient_Examples: HOL $(LOG)/HOL-Quotient_Examples.gz |
1299 HOL-Quotient_Examples: HOL $(LOG)/HOL-Quotient_Examples.gz |
1300 |
1300 |
1301 $(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL \ |
1301 $(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL \ |
1302 Quotient_Examples/FSet.thy \ |
1302 Quotient_Examples/FSet.thy Quotient_Examples/Quotient_Int.thy \ |
1303 Quotient_Examples/LarryInt.thy Quotient_Examples/LarryDatatype.thy |
1303 Quotient_Examples/Quotient_Message.thy |
1304 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples |
1304 @$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples |
1305 |
1305 |
1306 |
1306 |
1307 ## HOL-Predicate_Compile_Examples |
1307 ## HOL-Predicate_Compile_Examples |
1308 |
1308 |