include Document.History in Document.State -- just one universal session state maintained by main actor; Session.command_change_buffer: thread actor ensures asynchronous dispatch; misc tuning;

volatile variables (in Scala);

non-critical output primitives -- depending on thread-safe TextIO, while races wrt. flushing should not matter;

modernized specifications;

discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;

discontinued broken no_warnings_CRITICAL -- global output channels must not be changed after startup initialization;

eliminated broken Output.no_warnings_CRITICAL -- context visibility does the job; modernized attribute setup;

more careful treatment of context visibility flag wrt. spurious warnings; misc tuning;

eliminated obsolete Output.no_warnings, where no warnings were produced anyway;

eliminated broken Output.no_warnings_CRITICAL -- context visibility does the job;

more careful treatment of context visibility flag wrt. spurious warnings;

merged

merged

turn off experimental feature per default + avoid exception on "theory constant"

extended relevance filter with first-order term matching

drop chained facts

rename and simplify

cosmetics

renaming + treat "TFree" better in "pattern_for_type"

fix threshold computation + remove "op =" from relevant constants

avoid needless "that" fact

add nameless chained facts to the pool of things known to Sledgehammer

if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem

improve SPASS hack, when a clause comes from several facts

fix Vampire version numbers

lower penalty for Skolem constants

merged

official support for Scala

updated generated files

tuned whitespace

more xsymbols

re-added accidental omission

proper namespace administration for hierarchical modules

more antiquotations;

eliminated Unsynchronized.ref in favour of configuration option; proper naming of thy: theory vs. ctxt: Proof.context; recovered some Isabelle/ML indendation style;

more appropriate name for configuration option "meson_max_clauses" (cf. output of 'pront_configs');

Sum_Of_Squares: proper configuration options;

tuned printed type names, according to ML;

eliminated unnecessary ref;

clarified iter_deepen_limit vs meson (cf. 7c5896919eb8) -- eliminated global ref;

disposed some old debugging tools;

proper configuration option "show_proofs"; modernized syntax translation;

structure Unsynchronized is never opened and set/reset/toggle have been discontinued; retain Unsynchronized.change alias for Proof General;

expanded some aliases from structure Unsynchronized;

merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML;

merged

formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj

tuned fact reference

merged

added support for yet another prolog system (yap); generate has only one option ensure_groundness; added one example of yap invocation in example theory

adapted examples; tuned

moving options; tuned

added generation of predicates for size-limited enumeration of values

NEWS

merged

formerly unnamed infix impliciation now named HOL.implies

merged

proper passing of optional module name

For sublocale it is sufficient to reconsider ancestors of the target.

only print qualified implicits