* 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. Makarius