equal
deleted
inserted
replaced
215 * Document antiquotation @{verbatim} prints ASCII text literally in "tt" |
215 * Document antiquotation @{verbatim} prints ASCII text literally in "tt" |
216 style. |
216 style. |
217 |
217 |
218 |
218 |
219 *** ML *** |
219 *** ML *** |
|
220 |
|
221 * Cartouches within ML sources are turned into values of type |
|
222 Input.source (with formal position information). |
220 |
223 |
221 * Proper context for various elementary tactics: assume_tac, |
224 * Proper context for various elementary tactics: assume_tac, |
222 match_tac, compose_tac, Splitter.split_tac etc. Minor |
225 match_tac, compose_tac, Splitter.split_tac etc. Minor |
223 INCOMPATIBILITY. |
226 INCOMPATIBILITY. |
224 |
227 |