| changeset 4915 | 5ff99bd60da9 |
| parent 4899 | 447d6b2956ba |
| child 4930 | 89271bc4e7ed |
--- 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;