equal
deleted
inserted
replaced
200 "System/system_channel.ML" |
200 "System/system_channel.ML" |
201 "Thy/html.ML" |
201 "Thy/html.ML" |
202 "Thy/latex.ML" |
202 "Thy/latex.ML" |
203 "Thy/present.ML" |
203 "Thy/present.ML" |
204 "Thy/term_style.ML" |
204 "Thy/term_style.ML" |
205 "Thy/thm_deps.ML" |
|
206 "Thy/thy_header.ML" |
205 "Thy/thy_header.ML" |
207 "Thy/thy_info.ML" |
206 "Thy/thy_info.ML" |
208 "Thy/thy_output.ML" |
207 "Thy/thy_output.ML" |
209 "Thy/thy_syntax.ML" |
208 "Thy/thy_syntax.ML" |
210 "Tools/build.ML" |
209 "Tools/build.ML" |