clarified prepare_positions: always retain source positions to allow using it as formal information, not just markup reports;

merged

renewing Executable_Relation

tuned;

more direct Name_Space.defined_entry; tuned Variable.export_inst: avoid keeping full contexts within the gen_fixesT closure (NB: locale infrastructure stores morphisms persistently);

eliminated old-fashioned 'constrains' element;

modernized locale expression, with some fluctuation of arguments;

simplified span class in conformance to Scala version;

discontinued specific entity markup, which causes confusion with "kind" names with spaces (e.g. "type name"); uniform treatment of "class" entities in input and output;

merged

adding tags to quickcheck's result

clarified idents for activated locales, with subtle change of semantics: insert/merge wrt. term equality, but avoid redundant_ident on retrieval; avoid confusing quasiorder ident_le as "eq" for member/merge;

eliminated dead code;

clarified total_ident_ord, swapping first argument back to normal (unlike e464f84f3680) -- NB: "fast" ord is erratic anyway;

misc tuning and simplification;

tuned;

clarified Pattern.matchess;

tuned;

more precise alignment of begin/end, proof/qed; improved English;

merged

beautified

more precise checking for wellformedness of mapper, before and after morphism application

reject mapper terms with type variables not contained in the term's type

always bracket case expressions in Scala

tuned signature;

merges

More calculation-based cardinality proofs

split make_tptp_parser into two scripts, for parser and lib respectively;

added ml-yacc library sources;

added tptp parser;