summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

NEWS

changeset 17097 | 78f1b66f70a4 |

parent 17095 | 669005f73b81 |

child 17117 | e2bed9e82454 |

--- a/NEWS Wed Aug 17 17:04:15 2005 +0200 +++ b/NEWS Thu Aug 18 11:17:32 2005 +0200 @@ -90,6 +90,12 @@ interface for introducing further styles. See also the "LaTeX Sugar" document practical applications. +* Proper output of proof terms (@{prf ...} and @{full_prf ...}) within +a proof context. + +* Proper output of antiquotations for theory commands involving a +proof context (such as 'locale' or 'theorem (in loc) ...'). + *** Pure *** @@ -187,6 +193,10 @@ * More efficient treatment of intermediate checkpoints in interactive theory development. +* 'print_theorems': in theory mode, really print the difference +wrt. the last state (works for interactive theory development only), +in proof mode print all local facts (cf. 'print_facts'); + *** Locales ***