# HG changeset patch
# User wenzelm
# Date 912023725 -3600
# Node ID 040f6d2af50d28bacbbc7d1fa588721619021538
# Parent  2430ccbde87d66de62e66ecc21e01bec3319821b
removed prs / prs_fn;

diff -r 2430ccbde87d -r 040f6d2af50d NEWS
--- a/NEWS	Wed Nov 25 15:55:00 1998 +0100
+++ b/NEWS	Wed Nov 25 20:55:25 1998 +0100
@@ -9,11 +9,17 @@
 
 * HOL: Removed the obsolete syntax "Compl A"; use -A for set complement
 
-*** General ***
+
+*** Internal programming interfaces ***
 
 * tuned current_goals_markers semantics: begin / end goal avoids
 printing empty lines;
 
+* removed prs and prs_fn hook, which was broken because it did not
+include \n in its semantics, forcing writeln to add one
+uncoditionally; replaced prs_fn by writeln_fn; consider std_output:
+string -> unit if you really want to output text without newline;
+
 
 New in Isabelle98-1 (October 1998)
 ----------------------------------