* Delimiters of outer tokens now produce separate LaTeX macros;
Wed, 31 Aug 2005 15:46:30 +0200
changeset 17193 83708f724822
parent 17192 0cfbf76ed313
child 17194 70d96933c210
* Delimiters of outer tokens now produce separate LaTeX macros; * isatool usedir: option -C (default true) controls copying of document directory;
--- a/NEWS	Wed Aug 31 09:37:12 2005 +0200
+++ b/NEWS	Wed Aug 31 15:46:30 2005 +0200
@@ -99,6 +99,13 @@
 * Proper output of antiquotations for theory commands involving a
 proof context (such as 'locale' or 'theorem (in loc) ...').
+* Delimiters of outer tokens (string etc.) now produce separate LaTeX
+macros (\isachardoublequoteopen, isachardoublequoteclose etc.).
+* isatool usedir: new option -C (default true) controls whether option
+-D should include a copy of the original document directory; -C false
+prevents unwanted effects such as copying of administrative CVS data.
 *** Pure ***
@@ -593,6 +600,8 @@
 etc.) as well as the sign field in Thm.rep_thm etc. have been retained
 for convenience -- they merely return the theory.
+* Pure: type Type.tsig is superceded by theory in most interfaces.
 * Pure: the Isar proof context type is already defined early in Pure
 as Context.proof (note that ProofContext.context and Proof.context are
 aliases, where the latter is the preferred name).  This enables other