tuned;
authorwenzelm
Mon Jan 13 18:47:48 2014 +0100 (2014-01-13)
changeset 55006ea9fc64327cb
parent 55005 38ea5ee18a06
child 55007 0c07990363a3
tuned;
NEWS
     1.1 --- a/NEWS	Mon Jan 13 14:11:02 2014 +0100
     1.2 +++ b/NEWS	Mon Jan 13 18:47:48 2014 +0100
     1.3 @@ -34,9 +34,10 @@
     1.4  *** Pure ***
     1.5  
     1.6  * More thorough check of proof context for goal statements and
     1.7 -attributed fact expressions: background theory, declared hyps,
     1.8 -declared variable names.  Potential INCOMPATIBILITY, tools need to
     1.9 -observe standard context discipline.
    1.10 +attributed fact expressions (concerning background theory, declared
    1.11 +hyps).  Potential INCOMPATIBILITY, tools need to observe standard
    1.12 +context discipline.  See also Assumption.add_assumes and the more
    1.13 +primitive Thm.assume_hyps.
    1.14  
    1.15  
    1.16  *** HOL ***