# HG changeset patch
# User wenzelm
# Date 939906078 -7200
# Node ID 8b0aca9bdc26dfbaa1367a23eac3ce8186c573c4
# Parent  3e75fbd4a46bb478d62eef0ad6c8e9a2cf40d3c4
document preparation based on (PDF)LaTeX;

diff -r 3e75fbd4a46b -r 8b0aca9bdc26 NEWS
--- a/NEWS	Thu Oct 14 12:47:54 1999 +0200
+++ b/NEWS	Thu Oct 14 15:01:18 1999 +0200
@@ -59,8 +59,9 @@
 tactical theorem proving; together with the ProofGeneral/isar user
 interface it offers an interactive environment for developing human
 readable proof documents (Isar == Intelligible semi-automated
-reasoning); see isatool doc isar-ref and
-http://isabelle.in.tum.de/Isar/ for more information;
+reasoning); actual document preparation based on (PDF)LaTeX is
+available as well; see isatool doc isar-ref, HOL/Isar_examples and
+http://isabelle.in.tum.de/Isar/ for more information.
 
 * native support for Proof General, both for classic Isabelle and
 Isabelle/Isar (the latter is slightly better supported and more