global declaration of abstract syntax for proof terms, with qualified names;
clarified modules;

more operations: support type classes within the logic;

support abstract syntax for proof terms (see src/Pure/Proofs/proof_syntax.ML);

more Pure theory content;

Pure theory content;