NEWS
changeset 15011 35be762f58f9
parent 14972 51f95648abad
child 15012 28fa57b57209
     1.1 --- a/NEWS	Tue Jun 29 11:18:34 2004 +0200
     1.2 +++ b/NEWS	Wed Jun 30 00:42:59 2004 +0200
     1.3 @@ -6,6 +6,11 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Pure: Simplification procedures can now take the current simpset as
     1.8 +  an additional argument; This is useful for calling the simplifier
     1.9 +  recursively.  See the functions MetaSimplifier.full_{mk_simproc,
    1.10 +  simproc,simproc_i}.
    1.11 +
    1.12  * Pure: considerably improved version of 'constdefs' command.  Now
    1.13    performs automatic type-inference of declared constants; additional
    1.14    support for local structure declarations (cf. locales and HOL