equal
deleted
inserted
replaced
260 * Document antiquotation @{verbatim} prints ASCII text literally in "tt" |
260 * Document antiquotation @{verbatim} prints ASCII text literally in "tt" |
261 style. |
261 style. |
262 |
262 |
263 |
263 |
264 *** ML *** |
264 *** ML *** |
|
265 |
|
266 * The main operations to certify logical entities are Thm.ctyp_of and |
|
267 Thm.cterm_of with a local context; old-style global theory variants are |
|
268 available as Thm.global_ctyp_of and Thm.global_cterm_of. |
|
269 INCOMPATIBILITY. |
265 |
270 |
266 * Elementary operations in module Thm are no longer pervasive. |
271 * Elementary operations in module Thm are no longer pervasive. |
267 INCOMPATIBILITY, need to use qualified Thm.prop_of, Thm.cterm_of, |
272 INCOMPATIBILITY, need to use qualified Thm.prop_of, Thm.cterm_of, |
268 Thm.term_of etc. |
273 Thm.term_of etc. |
269 |
274 |