more uses of define_time_fun

translation to time functions now with canonical let.

merged

A few new results (mostly brought in from other developments)

merged

Added time function automation

streamlined type class specification

consolidated lemma name

support Phabricator on Ubuntu 22.04 LTS with PHP 8.1, using community form we.phorge.it version "2023 week 49";

merged

tuned;

update links;

follow post-maintenance updates of original Phabricator, as base-line for Phorge;

refer to "localhost" as pro-forma domain;

simplified specification of type class

consolidated name of lemma analogously to nat/int/word_bit_induct

more accurate syntax: 'obtain' vars are optional;

clarified order, disregard structure of proof;

minor performance tuning;

tuned;

more thorough treatment of hidden type variables within zproof;

more uniform treatment of "hyps" within zproof;

clarified order: follow Thm.fold_terms;

merged

clarified signature;

clarified signature;

tuned signature;

tuned;

clarified test: no exception yet;

tuned;