* 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