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

merged

stub for (later) correct deresolving of class method names

tuned serializer interface

private version of commas, cf. printmode

merged

merged

re-added accidental omission

tuned includes

prevent line breaks after Scala symbolic operators

corrected semantics of presentation_stmt_names; do not print includes on presentation selection

code_include Scala: qualify module nmae

merged