removed prs / prs_fn;
authorwenzelm
Wed, 25 Nov 1998 20:55:25 +0100
changeset 5973 040f6d2af50d
parent 5972 2430ccbde87d
child 5974 6acf3ff0f486
removed prs / prs_fn;
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)
 ----------------------------------