NEWS
changeset 42502 13b41fb77649
parent 42484 2777a27506d0
child 42514 f32500b4bc23
     1.1 --- a/NEWS	Thu Apr 28 20:20:49 2011 +0200
     1.2 +++ b/NEWS	Thu Apr 28 21:06:04 2011 +0200
     1.3 @@ -44,6 +44,10 @@
     1.4  
     1.5    declare [[unique_names = false]]
     1.6  
     1.7 +* Literal facts `prop` may contain dummy patterns, e.g. `_ = _`.  Note
     1.8 +that the result needs to be unique, which means fact specifications
     1.9 +may have to be refined after enriching a proof context.
    1.10 +
    1.11  
    1.12  *** HOL ***
    1.13