fixed infinite loop with trivial rel_O_Gr + tuning

adapted FP code to new relator approach

tuning

renamed "bnf_fp_util.ML" to "bnf_fp.ML"

adapted BNF composition to new relator approach

don't define relators unless necessary

moved predicator definition before after_qed

add rel as first-class citizen of BNF

renamed "rel_def" to "rel_O_Gr"

renamed "sum_setl" to "setl" and similarly for r

tuned ID/DEADID setup

JavaFX is inactive by default;

reactivate HOL-Mirabelle-ex with increased chances that it works most of the time (cf. bec1add86e79, a93d920707bb, be27a453aacc);

universal component exec_process -- avoids special Admin/components/windows and might actually improve stability of forked processes (without using perl);

more direct GUI component;

earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);

made SML/NJ happy;

tuned;

merged

recording elapsed time in mutabelle for more detailed evaluation

Added missing predicators (for multisets and countable sets)

added top-level theory for Cardinals

group "simps" together

register induct attributes

further tuned simpset

bnf_note_all mode for "pre_"-BNFs

separated registration of BNFs from bnf_def (BNFs are now stored only for bnf_def and (co)data commands)

tuned

beautified names

proved all upper bounds