equal
deleted
inserted
replaced
101 Tools/datatype_rep_proofs.ML Tools/induct_attrib.ML Tools/induct_method.ML \ |
101 Tools/datatype_rep_proofs.ML Tools/induct_attrib.ML Tools/induct_method.ML \ |
102 Tools/inductive_package.ML Tools/inductive_codegen.ML Tools/meson.ML Tools/numeral_syntax.ML \ |
102 Tools/inductive_package.ML Tools/inductive_codegen.ML Tools/meson.ML Tools/numeral_syntax.ML \ |
103 Tools/primrec_package.ML Tools/recdef_package.ML \ |
103 Tools/primrec_package.ML Tools/recdef_package.ML \ |
104 Tools/record_package.ML Tools/split_rule.ML \ |
104 Tools/record_package.ML Tools/split_rule.ML \ |
105 Tools/svc_funcs.ML Tools/typedef_package.ML \ |
105 Tools/svc_funcs.ML Tools/typedef_package.ML \ |
106 Transitive_Closure.thy Transitive_Closure_lemmas.ML Wellfounded_Recursion.ML \ |
106 Transitive_Closure.thy Transitive_Closure_lemmas.ML Typedef.thy \ |
107 Wellfounded_Recursion.thy Wellfounded_Relations.ML \ |
107 Wellfounded_Recursion.ML Wellfounded_Recursion.thy Wellfounded_Relations.ML \ |
108 Wellfounded_Relations.thy arith_data.ML blastdata.ML cladata.ML \ |
108 Wellfounded_Relations.thy arith_data.ML blastdata.ML cladata.ML \ |
109 equalities.ML equalities.thy hologic.ML meson_lemmas.ML mono.ML \ |
109 equalities.ML hologic.ML meson_lemmas.ML mono.ML \ |
110 mono.thy simpdata.ML subset.ML subset.thy thy_syntax.ML |
110 simpdata.ML subset.ML thy_syntax.ML |
111 @$(ISATOOL) usedir -b $(OUT)/Pure HOL |
111 @$(ISATOOL) usedir -b $(OUT)/Pure HOL |
112 |
112 |
113 |
113 |
114 ## HOL-Real |
114 ## HOL-Real |
115 |
115 |