equal
deleted
inserted
replaced
329 |
329 |
330 * New "case_product" attribute (see HOL). |
330 * New "case_product" attribute (see HOL). |
331 |
331 |
332 |
332 |
333 *** ML *** |
333 *** ML *** |
|
334 |
|
335 * Renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in |
|
336 conformance with similar operations in structure Term and Logic. |
334 |
337 |
335 * Antiquotation @{attributes [...]} embeds attribute source |
338 * Antiquotation @{attributes [...]} embeds attribute source |
336 representation into the ML text, which is particularly useful with |
339 representation into the ML text, which is particularly useful with |
337 declarations like Local_Theory.note. |
340 declarations like Local_Theory.note. |
338 |
341 |