# HG changeset patch
# User wenzelm
# Date 909080001 -7200
# Node ID f84dc3b811e911685b18429d1aeb9169eea5a561
# Parent  82a7aa74a631244efbb8704591c247af106afdc7
current_goals_markers;

diff -r 82a7aa74a631 -r f84dc3b811e9 NEWS
--- a/NEWS	Thu Oct 22 20:11:19 1998 +0200
+++ b/NEWS	Thu Oct 22 20:13:21 1998 +0200
@@ -351,6 +351,12 @@
 
 * Display.print_goals function moved to Locale.print_goals;
 
+* standard print function for goals supports current_goals_markers
+variable for marking begin of proof, end of proof, start of goal; the
+default is ("", "", ""); setting current_goals_markers := ("<proof>",
+"</proof>", "<goal>") causes SGML like tagged proof state printing,
+for example;
+
 
 
 New in Isabelle98 (January 1998)