moving preprocessing to values in prolog generation

invocation of values for prolog execution does not require invocation of code_pred anymore

adding hotel keycard example for prolog generation

improving output of set comprehensions; adding style_check flags

improving ensure_groundness in prolog generation; added further example

adding very basic transformation to ensure groundness before negations

Markup_Tree.select: uniform treatment of root_range wrt. singularities, yielding empty result stream;

tuned signature;

Pretty: tuned markup objects;

tuned;

organized markup properties via apply/unapply patterns;

added some proof state markup, notably number of subgoals (e.g. for indentation); tuned;

ML_Context.eval: produce antiquotation environment preferably in invisible context, to avoid displaced report messages from ML_Compiler;

merged

tuned code

quotient package: deal correctly with frees in lifted theorems