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