summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 18 Aug 2005 11:17:32 +0200 | |

changeset 17097 | 78f1b66f70a4 |

parent 17096 | 8327b71282ce |

child 17098 | dd769bd4d056 |

* Proper output of proof terms within a proof context;
* Proper output of antiquotations for theory commands involving a proof context;
* 'print_theorems': in theory mode print difference of facts, in proof mode print local facts;

--- 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 ***