[isabelle-dev] NEWS

Makarius makarius at sketis.net
Tue Aug 14 17:16:42 CEST 2012

* Command 'typ' supports an additional variant with explicit sort
constraint, to infer and check the most general type conforming to a
given given sort.  Example (in HOL):

   typ "_ * _ * bool * unit" :: finite

This refers to Isabelle/4aa5b965f70e.


More information about the isabelle-dev mailing list