equal
deleted
inserted
replaced
105 Tools/function_package/context_tree.ML \ |
105 Tools/function_package/context_tree.ML \ |
106 Tools/function_package/fundef_common.ML \ |
106 Tools/function_package/fundef_common.ML \ |
107 Tools/function_package/fundef_datatype.ML \ |
107 Tools/function_package/fundef_datatype.ML \ |
108 Tools/function_package/fundef_lib.ML \ |
108 Tools/function_package/fundef_lib.ML \ |
109 Tools/function_package/fundef_package.ML \ |
109 Tools/function_package/fundef_package.ML \ |
110 Tools/function_package/fundef_prep.ML \ |
110 Tools/function_package/fundef_core.ML \ |
111 Tools/function_package/fundef_proof.ML \ |
|
112 Tools/function_package/inductive_wrap.ML \ |
111 Tools/function_package/inductive_wrap.ML \ |
113 Tools/function_package/lexicographic_order.ML \ |
112 Tools/function_package/lexicographic_order.ML \ |
114 Tools/function_package/mutual.ML \ |
113 Tools/function_package/mutual.ML \ |
115 Tools/function_package/pattern_split.ML \ |
114 Tools/function_package/pattern_split.ML \ |
116 Tools/function_package/sum_tools.ML \ |
115 Tools/function_package/sum_tools.ML \ |