equal
deleted
inserted
replaced
86 Accessible_Part.thy Arith_Tools.thy Datatype.thy \ |
86 Accessible_Part.thy Arith_Tools.thy Datatype.thy \ |
87 Dense_Linear_Order.thy Divides.thy Equiv_Relations.thy Extraction.thy \ |
87 Dense_Linear_Order.thy Divides.thy Equiv_Relations.thy Extraction.thy \ |
88 Finite_Set.thy FixedPoint.thy Fun.thy FunDef.thy HOL.thy \ |
88 Finite_Set.thy FixedPoint.thy Fun.thy FunDef.thy HOL.thy \ |
89 Hilbert_Choice.thy Inductive.thy IntArith.thy IntDef.thy IntDiv.thy \ |
89 Hilbert_Choice.thy Inductive.thy IntArith.thy IntDef.thy IntDiv.thy \ |
90 Lattices.thy List.thy Main.thy Map.thy Nat.thy NatBin.thy \ |
90 Lattices.thy List.thy Main.thy Map.thy Nat.thy NatBin.thy \ |
91 Numeral.thy Option.thy OrderedGroup.thy Orderings.thy Power.thy PreList.thy \ |
91 Numeral.thy OrderedGroup.thy Orderings.thy Power.thy PreList.thy \ |
92 Predicate.thy Product_Type.thy ROOT.ML Recdef.thy \ |
92 Predicate.thy Product_Type.thy ROOT.ML Recdef.thy \ |
93 Record.thy Refute.thy Relation.thy Relation_Power.thy \ |
93 Record.thy Refute.thy Relation.thy Relation_Power.thy \ |
94 Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy Sum_Type.thy \ |
94 Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy Sum_Type.thy \ |
95 Groebner_Basis.thy Tools/ATP/reduce_axiomsN.ML Tools/watcher.ML \ |
95 Groebner_Basis.thy Tools/ATP/reduce_axiomsN.ML Tools/watcher.ML \ |
96 Tools/Groebner_Basis/groebner.ML Tools/Groebner_Basis/misc.ML \ |
96 Tools/Groebner_Basis/groebner.ML Tools/Groebner_Basis/misc.ML \ |
221 Library/SCT_Definition.thy Library/SCT_Theorem.thy \ |
221 Library/SCT_Definition.thy Library/SCT_Theorem.thy \ |
222 Library/SCT_Interpretation.thy \ |
222 Library/SCT_Interpretation.thy \ |
223 Library/SCT_Implementation.thy Library/Size_Change_Termination.thy \ |
223 Library/SCT_Implementation.thy Library/Size_Change_Termination.thy \ |
224 Library/SCT_Examples.thy Library/sct.ML \ |
224 Library/SCT_Examples.thy Library/sct.ML \ |
225 Library/Pure_term.thy Library/Eval.thy Library/Pretty_Int.thy \ |
225 Library/Pure_term.thy Library/Eval.thy Library/Pretty_Int.thy \ |
226 Library/Pretty_Char.thy Library/Pretty_Char_chr.thy |
226 Library/Pretty_Char.thy Library/Pretty_Char_chr.thy Library/Abstract_Rat.thy |
227 @cd Library; $(ISATOOL) usedir $(OUT)/HOL Library |
227 @cd Library; $(ISATOOL) usedir $(OUT)/HOL Library |
228 |
228 |
229 |
229 |
230 ## HOL-Subst |
230 ## HOL-Subst |
231 |
231 |
646 $(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy \ |
646 $(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy \ |
647 ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy \ |
647 ex/Abstract_NAT.thy ex/Antiquote.thy ex/Arith_Examples.thy \ |
648 ex/BT.thy ex/BinEx.thy ex/CTL.thy \ |
648 ex/BT.thy ex/BinEx.thy ex/CTL.thy \ |
649 ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy ex/Dense_Linear_Order_Ex.thy \ |
649 ex/Chinese.thy ex/Classical.thy ex/Classpackage.thy ex/Dense_Linear_Order_Ex.thy \ |
650 ex/Eval_Examples.thy ex/Groebner_Examples.thy ex/Random.thy \ |
650 ex/Eval_Examples.thy ex/Groebner_Examples.thy ex/Random.thy \ |
651 ex/Codegenerator.thy ex/Codegenerator_Rat.thy \ |
651 ex/Codegenerator.thy ex/Codegenerator_Pretty.thy \ |
652 ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy \ |
652 ex/Commutative_RingEx.thy ex/Hex_Bin_Examples.thy \ |
653 ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy \ |
653 ex/Commutative_Ring_Complete.thy ex/ExecutableContent.thy \ |
654 ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy ex/Binary.thy \ |
654 ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy ex/Binary.thy \ |
655 ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy ex/InSort.thy \ |
655 ex/Higher_Order_Logic.thy ex/Hilbert_Classical.thy ex/InSort.thy \ |
656 ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \ |
656 ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \ |