# HG changeset patch
# User wenzelm
# Date 951252797 -3600
# Node ID 0a319c5746eb218fca219a54067381c11115234b
# Parent  58a33fd5b30c3710a057f038de087c73aa718580
* Pure now provides its own version of intro/elim/dest attributes;
useful for building new logics, but beware of confusion with the
Provers/classical ones!
* HOL: removed "case_split" thm binding, should use "cases" proof
method anyway;
* tuned syntax of "induct" method;
* new "cases" method for propositions, inductive sets and types;
* HOL/records: admit "r" as field name;

diff -r 58a33fd5b30c -r 0a319c5746eb NEWS
--- a/NEWS	Tue Feb 22 21:51:25 2000 +0100
+++ b/NEWS	Tue Feb 22 21:53:17 2000 +0100
@@ -16,8 +16,19 @@
 
 * intro/elim/dest attributes: changed ! / !! flags to ? / ??;
 
+* Pure now provides its own version of intro/elim/dest attributes;
+useful for building new logics, but beware of confusion with the
+Provers/classical ones!
+
 * new 'obtain' language element supports generalized existence proofs;
 
+* HOL: removed "case_split" thm binding, should use "cases" proof
+method anyway;
+
+* tuned syntax of "induct" method;
+
+* new "cases" method for propositions, inductive sets and types;
+
 
 *** HOL ***
 
@@ -25,7 +36,7 @@
 Ballarin;
 
 * HOL/record: fixed select-update simplification procedure to handle
-extended records as well;
+extended records as well; admit "r" as field name;