equal
deleted
inserted
replaced
229 |
229 |
230 *** ML *** |
230 *** ML *** |
231 |
231 |
232 * Configuration option show_question_marks only affects regular pretty |
232 * Configuration option show_question_marks only affects regular pretty |
233 printing of types and terms, not raw Term.string_of_vname. |
233 printing of types and terms, not raw Term.string_of_vname. |
|
234 |
|
235 * ML_Context.thm and ML_Context.thms are no longer pervasive. Rare |
|
236 INCOMPATIBILITY, superseded by static antiquotations @{thm} and |
|
237 @{thms} for most purposes. |
234 |
238 |
235 * ML structure Unsynchronized never opened, not even in Isar |
239 * ML structure Unsynchronized never opened, not even in Isar |
236 interaction mode as before. Old Unsynchronized.set etc. have been |
240 interaction mode as before. Old Unsynchronized.set etc. have been |
237 discontinued -- use plain := instead. This should be *rare* anyway, |
241 discontinued -- use plain := instead. This should be *rare* anyway, |
238 since modern tools always work via official context data, notably |
242 since modern tools always work via official context data, notably |