# HG changeset patch
# User wenzelm
# Date 895047688 -7200
# Node ID 5ff99bd60da9462e1fb861fd19cd077acc83e977
# Parent  119d5f5767a4877d16bafcc6b242d66ac08396e6
HOL/record: now includes concrete syntax for record terms;

diff -r 119d5f5767a4 -r 5ff99bd60da9 NEWS
--- a/NEWS	Tue May 12 18:07:03 1998 +0200
+++ b/NEWS	Wed May 13 10:21:28 1998 +0200
@@ -42,6 +42,9 @@
 
 *** HOL ***
 
+* HOL/record: now includes concrete syntax for record terms (still
+lacks important theorems, like surjective pairing and split);
+
 * new force_tac (and its derivations Force_tac, force): combines
 rewriting and classical reasoning (and whatever other tools) similarly
 to auto_tac, but is aimed to solve the given subgoal totally;