HomeIsabelle/Phabricator

tuned signature (again): latex_output is likely to depend on context;