NEWS
changeset 15454 4b339d3907a0
parent 15436 d059da8434a5
child 15475 fdf9434b04ea
     1.1 --- a/NEWS	Mon Jan 24 12:40:52 2005 +0100
     1.2 +++ b/NEWS	Mon Jan 24 12:41:06 2005 +0100
     1.3 @@ -34,6 +34,10 @@
     1.4  * Provers/blast.ML:  new reference depth_limit to make blast's depth
     1.5    limit (previously hard-coded with a value of 20) user-definable.
     1.6  
     1.7 +* Pure: thin_tac now works even if the assumption being deleted contains !! or ==>. 
     1.8 +  More generally, erule now works even if the major premise of the elimination rule
     1.9 +  contains !! or ==>.
    1.10 +
    1.11  * Pure: considerably improved version of 'constdefs' command.  Now
    1.12    performs automatic type-inference of declared constants; additional
    1.13    support for local structure declarations (cf. locales and HOL