reenable Nitpick on Cygwin; we'll see tomorrow if there's still a failure, and if so I'll investigate

merged;

Proof.pretty_state: print everything in the foreground context to give users a chance to configure options, e.g. via "using [[show_consts]]";

turned show_consts into proper configuration option;

prefer regular Proof.context over background theory; misc tuning and simplification;

just one refute.ML;

use existing Integer.pow, despite its slightly odd argument order;

tuned whitespace and indentation, emphasizing the logical structure of this long text;

inner parsing: refrain from too many nested position reports to achieve more precise error feedback in the source;

Document_View: squiggly underline for messages; tuned;

added gfx_range convenience;

Isar_Document.reported_positions: more precise include/exclude, include root as last resort only;

Position.Range: exclude singularity (again);

merged

merged

FIXME -> TODO (nothing is broken)

Let MESON take an additional "preskolemization tactic", which can be used to put the goal in definitional CNF

use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd; this *really* speeds up things -- HOL now builds 12% faster on my machine

make definitional CNF translation code more robust in the presence of existential quantifiers in the "literals"

formal framework for presentation of selected statements

merged

Table.map replaces Table.map'

dropped dead code; tuned

include names need not be considered as reserved any longer

skip empty name bunches; fill up trailing positions with NONEs

use code_namespace module for SML and OCaml code

Table.map replaces Table.map'

avoid cyclic modules

merged

simultaneous modification of statements: statement names