changeset 67718 | 17874d43d3b3 |
parent 67702 | 2d9918f5b33c |
child 67740 | b6ce18784872 |
--- a/NEWS Sat Feb 24 17:21:35 2018 +0100 +++ b/NEWS Sun Feb 25 12:59:08 2018 +0100 @@ -176,6 +176,12 @@ (e.g. use 'find_theorems' or 'try' to figure this out). +*** Pure *** + +* The inner syntax category "sort" now includes notation "_" for the +dummy sort: it is effectively ignored in type-inference. + + *** HOL *** * Clarifed theorem names: