HOL/record: now includes concrete syntax for record terms;
authorwenzelm
Wed May 13 10:21:28 1998 +0200 (1998-05-13)
changeset 49155ff99bd60da9
parent 4914 119d5f5767a4
child 4916 fe8b0c82691b
HOL/record: now includes concrete syntax for record terms;
NEWS
     1.1 --- a/NEWS	Tue May 12 18:07:03 1998 +0200
     1.2 +++ b/NEWS	Wed May 13 10:21:28 1998 +0200
     1.3 @@ -42,6 +42,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* HOL/record: now includes concrete syntax for record terms (still
     1.8 +lacks important theorems, like surjective pairing and split);
     1.9 +
    1.10  * new force_tac (and its derivations Force_tac, force): combines
    1.11  rewriting and classical reasoning (and whatever other tools) similarly
    1.12  to auto_tac, but is aimed to solve the given subgoal totally;