presburger_ss: proper context;

presburger_ss: proper context; Goal.prove: context;

tuned;

avoid Force_tac, which uses a different context;

Goal.prove: context;

tactic/method simpset: maintain proper context;

Goal.prove_global; SkipProof.prove: context;

Goal.prove_global;

simprocs: no theory argument -- use simpset context instead; tuned interfaces;

simprocs: no theory argument -- use simpset context instead;

updated;

updated Goal.prove, Goal.prove_global;

added some bits on variables;

* 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;