* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables; * Pure: Goal.prove, Goal.prove_global; tuned;

"solver" reference added to make the SAT solver configurable

Some tidying. Fixed a problem where the DFG file did not declare some TFrees as 0-ary functions. Frees no longer have types attached.

Fixed erroneous check-in.

made evaluation_conv and normalization_conv visible.

Internal restructuring: identify no longer computes syntax.

Modified comment.

added support for MiniSat 1.14

removed obsolete locale view;

apply_text: support Method.Source_i;

added method_i and Source_i;

thm parsers: include Args.internal_fact;

add/del_simps: warning for inactive simpset (no context); tuned;

updated;

Local variables;

Isar.context ();

tuned;

added Isar.context;

some tidying; fixed the output of theorem names

def_export: Drule.generalize;

matchers: fall back on plain first_order_matchers, not pattern;

make sure $DISTPREFIX exists before calling makedist

removed the "tagging" feature

made the conversion of elimination rules more robust

Literals aren't sorted any more.

Literals aren't sorted any more. Output overloaded constants' type var instantiations.

fixed let-simproc ----------------------------------------------------------------------

Isar: 'print_facts' prints all local facts;

print_lthms: include unnamed facts from index; tuned;

added content;