more uniform descriptions, which end up in the collective output of 'print_attributes' for example;

Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;

slightly more abstract data handling in Fast_Lin_Arith;

theory data merge: prefer left side uniformly;

tuned;

simplification/standardization of some theory data;

misc tuning and simplification, notably theory data;

renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;

renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;

standardized Context.copy_thy to Theory.copy alias, with slightly more direct way of using it;