equal
deleted
inserted
replaced
255 * Document antiquotation @{verbatim} prints ASCII text literally in "tt" |
255 * Document antiquotation @{verbatim} prints ASCII text literally in "tt" |
256 style. |
256 style. |
257 |
257 |
258 |
258 |
259 *** ML *** |
259 *** ML *** |
|
260 |
|
261 * Elementary operations in module Thm are no longer pervasive. |
|
262 INCOMPATIBILITY, need to use qualified Thm.prop_of, Thm.cterm_of, |
|
263 Thm.term_of etc. |
260 |
264 |
261 * Former combinators NAMED_CRITICAL and CRITICAL for central critical |
265 * Former combinators NAMED_CRITICAL and CRITICAL for central critical |
262 sections have been discontinued, in favour of the more elementary |
266 sections have been discontinued, in favour of the more elementary |
263 Multithreading.synchronized and its high-level derivative |
267 Multithreading.synchronized and its high-level derivative |
264 Synchronized.var (which is usually sufficient in applications). Subtle |
268 Synchronized.var (which is usually sufficient in applications). Subtle |