--- a/NEWS Sat Apr 07 19:38:50 2001 +0200
+++ b/NEWS Mon Apr 09 10:10:21 2001 +0200
@@ -15,6 +15,10 @@
*** Overview of INCOMPATIBILITIES ***
+* HOL: please note that theories in the Library and elsewhere often use the
+new-style (Isar) format; to refer to their theorems in an ML script you must
+bind them to ML identifers by e.g. val thm_name = thm "thm_name";
+
* HOL: inductive package no longer splits induction rule aggressively,
but only as far as specified by the introductions given; the old
format may be recovered via ML function complete_split_rule or attribute