diff -r 0cfbf76ed313 -r 83708f724822 NEWS --- 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