equal
deleted
inserted
replaced
336 *** ML *** |
336 *** ML *** |
337 |
337 |
338 * Antiquotation @{assert} inlines a function bool -> unit that raises |
338 * Antiquotation @{assert} inlines a function bool -> unit that raises |
339 Fail if the argument is false. Due to inlining the source position of |
339 Fail if the argument is false. Due to inlining the source position of |
340 failed assertions is included in the error output. |
340 failed assertions is included in the error output. |
|
341 |
|
342 * Discontinued antiquotation @{theory_ref}, which is obsolete since ML |
|
343 text is in practice always evaluated with a stable theory checkpoint. |
|
344 Minor INCOMPATIBILITY, use (Theory.check_thy @{theory}) instead. |
341 |
345 |
342 * Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its |
346 * Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its |
343 meaning. |
347 meaning. |
344 |
348 |
345 * Renamed structure PureThy to Pure_Thy and moved most of its |
349 * Renamed structure PureThy to Pure_Thy and moved most of its |