HomeIsabelle/Phabricator

proper context for norm_hhf and derived operations;

Description

proper context for norm_hhf and derived operations;
clarified tool context in some boundary cases;

Details

Provenance
makariusAuthored on
Parents
rISABELLE61276a7fc369: made SML/NJ happy;
Branches
Unknown
Tags
Unknown