spurious set/pred correction

explicit locations for import_theory and setup_theory, for better user interface conformance; spurious set/pred correction

explicit locations for import_theory and setup_theory, for better user interface conformance

discontinued obsolete Library.foldl_map and Library.apply (NB: apply = fold I);

tuned;

tuned;

tuned;

canonical argument order for attribute application;

clarified terminology of raw protocol messages;

tuned;

tuned signature -- emphasize Isabelle_Process Input vs. Output;

explicit syslog_limit reduces danger of low-level message flooding; tuned;

retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided); tuned;

clarified scope of exception handlers;

relevant timing as in ML; more PIDE modules;

more fundamental pred-to-set conversions for range and domain by means of inductive_set

merged

tuned whitespace

tuned import

dropped dead code

terminate after first exception -- avoid syslog flooding;

avoid buffer loading overrun; tuned;

merged

collecting all axioms in a locale context in quickcheck; adding some verbose output;

choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing

removing finiteness goals

adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets

Symbol.encode header edits;

merged

tuned whitespace