NEWS
changeset 11241 61b21aacf04a
parent 11181 d04f57b91166
child 11307 891fbd3f4881
     1.1 --- a/NEWS	Sat Apr 07 19:38:50 2001 +0200
     1.2 +++ b/NEWS	Mon Apr 09 10:10:21 2001 +0200
     1.3 @@ -15,6 +15,10 @@
     1.4  
     1.5  *** Overview of INCOMPATIBILITIES ***
     1.6  
     1.7 +* HOL: please note that theories in the Library and elsewhere often use the
     1.8 +new-style (Isar) format; to refer to their theorems in an ML script you must
     1.9 +bind them to ML identifers by e.g.	val thm_name = thm "thm_name";
    1.10 +
    1.11  * HOL: inductive package no longer splits induction rule aggressively,
    1.12  but only as far as specified by the introductions given; the old
    1.13  format may be recovered via ML function complete_split_rule or attribute