NEWS
changeset 48792 4aa5b965f70e
parent 48736 292b97e17fb7
child 48844 6408fb6f7d81
     1.1 --- a/NEWS	Tue Aug 14 11:37:58 2012 +0200
     1.2 +++ b/NEWS	Tue Aug 14 11:43:08 2012 +0200
     1.3 @@ -29,6 +29,12 @@
     1.4  operators like COMP, INCR_COMP, COMP_INCR, which need to be applied
     1.5  with some care where this is really required.
     1.6  
     1.7 +* Command 'typ' supports an additional variant with explicit sort
     1.8 +constraint, to infer and check the most general type conforming to a
     1.9 +given given sort.  Example (in HOL):
    1.10 +
    1.11 +  typ "_ * _ * bool * unit" :: finite
    1.12 +
    1.13  
    1.14  *** HOL ***
    1.15