equal
deleted
inserted
replaced
209 Library/Coinductive_List.thy Library/AssocList.thy \ |
209 Library/Coinductive_List.thy Library/AssocList.thy \ |
210 Library/Parity.thy Library/GCD.thy Library/Binomial.thy \ |
210 Library/Parity.thy Library/GCD.thy Library/Binomial.thy \ |
211 Library/Graphs.thy Library/Kleene_Algebras.thy Library/SCT_Misc.thy \ |
211 Library/Graphs.thy Library/Kleene_Algebras.thy Library/SCT_Misc.thy \ |
212 Library/SCT_Definition.thy Library/SCT_Theorem.thy Library/SCT_Interpretation.thy \ |
212 Library/SCT_Definition.thy Library/SCT_Theorem.thy Library/SCT_Interpretation.thy \ |
213 Library/SCT_Implementation.thy Library/Size_Change_Termination.thy \ |
213 Library/SCT_Implementation.thy Library/Size_Change_Termination.thy \ |
214 Library/SCT_Examples.thy Library/sct.ML |
214 Library/SCT_Examples.thy Library/sct.ML \ |
|
215 Library/Pure_term.thy Library/Eval.thy |
215 @cd Library; $(ISATOOL) usedir $(OUT)/HOL Library |
216 @cd Library; $(ISATOOL) usedir $(OUT)/HOL Library |
216 |
217 |
217 |
218 |
218 ## HOL-Subst |
219 ## HOL-Subst |
219 |
220 |
616 HOL-ex: HOL $(LOG)/HOL-ex.gz |
617 HOL-ex: HOL $(LOG)/HOL-ex.gz |
617 |
618 |
618 $(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy \ |
619 $(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy \ |
619 ex/Abstract_NAT.thy ex/Antiquote.thy ex/BT.thy ex/BinEx.thy \ |
620 ex/Abstract_NAT.thy ex/Antiquote.thy ex/BT.thy ex/BinEx.thy \ |
620 ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy \ |
621 ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy \ |
621 ex/CodeEmbed.thy ex/CodeRandom.thy ex/CodeRevappl.thy \ |
622 ex/Eval_examples.thy ex/CodeRandom.thy ex/CodeRevappl.thy \ |
622 ex/Codegenerator.thy ex/Codegenerator_Rat.thy \ |
623 ex/Codegenerator.thy ex/Codegenerator_Rat.thy \ |
623 ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy \ |
624 ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy \ |
624 ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy \ |
625 ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy \ |
625 ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy ex/Binary.thy \ |
626 ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy ex/Binary.thy \ |
626 ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy ex/InSort.thy \ |
627 ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy ex/InSort.thy \ |