merged

merged

tidying and structured proofs

refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.; actually make "raw_def" internal (cf. 80123a220219);

tuned proofs;

simultaneous read_fields -- e.g. relevant for sort assignment;

added Syntax.read_typs; tuned parallelism for syntax operations;

renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;

tuned message;

tuned proofs;