removed prs / prs_fn;
authorwenzelm
Wed Nov 25 20:55:25 1998 +0100 (1998-11-25)
changeset 5973040f6d2af50d
parent 5972 2430ccbde87d
child 5974 6acf3ff0f486
removed prs / prs_fn;
NEWS
     1.1 --- a/NEWS	Wed Nov 25 15:55:00 1998 +0100
     1.2 +++ b/NEWS	Wed Nov 25 20:55:25 1998 +0100
     1.3 @@ -9,11 +9,17 @@
     1.4  
     1.5  * HOL: Removed the obsolete syntax "Compl A"; use -A for set complement
     1.6  
     1.7 -*** General ***
     1.8 +
     1.9 +*** Internal programming interfaces ***
    1.10  
    1.11  * tuned current_goals_markers semantics: begin / end goal avoids
    1.12  printing empty lines;
    1.13  
    1.14 +* removed prs and prs_fn hook, which was broken because it did not
    1.15 +include \n in its semantics, forcing writeln to add one
    1.16 +uncoditionally; replaced prs_fn by writeln_fn; consider std_output:
    1.17 +string -> unit if you really want to output text without newline;
    1.18 +
    1.19  
    1.20  New in Isabelle98-1 (October 1998)
    1.21  ----------------------------------