clarified HTML presentation, e.g. avoid bulky jobs like HOL or HOL-Analysis in applications;