added template diff against newer mercurials, where the 'ago' duplication has been fixed

use unified diff format (diff -Naur), which is much more robust and generally preferred -- previous patch failed to apply even in simple situations

hg template diff: renamed to reflect the base version (which silently changed in caf19101073d, by accident?)

standardized some ML aliases;

avoid Display.string_of_thm_without_context; tuned readability of sources;

eliminated global references / critical sections via context data; misc tuning and modernization;

explicit context for Codegen.eval_term etc.;

added Theory.nodes_of convenience;

updated reference machines;

migrated macbroy6 to macbroy30, which is the new "mobile" server (2 cores, 4 GB, Mac OS 10.5);

merged

increase "auto"'s timeout in example to help SML/NJ

making the evaluation of HOL.implies lazy even in strict languages by mapping it to an if statement

merged

avoid relying on "Thm.definitionK" to pick up definitions -- this was an old hack related to locales (to avoid expanding locale constants to their low-level definition) that is no longer necessary

merged

- renamed enum type class to spark_enum, to avoid confusion with enum type class defined in Enum theory - renamed theorem ..._card_UNIV to ..._card

use "Spec_Rules" for finding axioms -- more reliable and cleaner

optimize trivial equalities early in Nitpick -- it shouldn't be the job of the peephole optimizer

remove a few Nitpick calls in examples -- another step toward making them run faster

check arity of bound variables to avoid generating too large Kodkod problems -- an issue that arose in the context of TPTP/CASC

eliminated Codegen.mode in favour of explicit argument;

less bulky "_position", for improved readability of parse trees;

added more elementary Skip_Proof.make_thm_cterm;

explicit markup for loose bounds;

prefer internal types, via Simple_Syntax.read_typ;

eliminated obsolete Proof_Syntax.strip_sorts_consttypes;

split Type_Infer into early and late part, after Proof_Context; added Type_Infer_Context.const_sorts option, which allows NBE to use regular Syntax.check_term;

minor tuning and modernization;

slightly more special eq_list/eq_set, with shortcut involving pointer_eq;

simplified check/uncheck interfaces: result comparison is hardwired by default; tuned;

updated some theory primitives, which now depend on auxiliary context;

more precise treatment of existing type inference parameters; tuned;

pretty_abbrev: read abbreviation more directly;

tuned signature;

raised timeouts further, for SML/NJ!

Package prefix is now taken into account when looking up user-defined types and proof functions.

merged

recovered Theory.check_def: full name needs to be determined from background thy, not auxiliary ctxt (broken in 774df7c59508, caused Nitpick.all_axioms_of to produce bad results);

scheduler for Mutabelle regression

tool for importing nightly isatest logs

adding bounded_forall tester

creating generic test_term function; corrected instantiate_exhaustive_datatype; tuned

pass plain Proof.context for pretty printing;

standardized aliases of operations on tsig;

pass plain Proof.context for pretty printing;

tuned;

simplified Sorts.class_error: plain Proof.context; tuned;

pass plain Proof.context for pretty printing;

simplified pretty printing context, which is only required for certain kernel operations; disentangled dependencies of structure Pretty;

provide structure Syntax early (before structure Type), back-patch check/uncheck later;

added Binding.print convenience, which includes quote already;

markup attributes/methods via name space; eliminated obsolete markup;

tuned signature;

markup facts via name space; eliminated obsolete markup;

tuned -- order in memory according to variance;

eliminated obsolete markup -- superseded by generic "entity" markup;

report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;

clarified pretty_parsetree: suppress literal tokens;

PARALLEL_GOALS for simplification within auto_tac;

PARALLEL_GOALS for method "simp_all";

enable PARALLEL_GOALS more liberally, unlike forked proofs (cf. 34b9652b2f45);

refined PARALLEL_GOALS;

tuned blast: navigate to subgoal only once;

proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way; tuned;

more direct Thm.cprem_of (with exception THM instead of Subscript); modernized thy;

more direct Thm.cprem_of (with exception THM instead of Subscript);

more direct Logic.dest_implies (with exception TERM instead of Subscript);

eliminated old List.nth; tuned;

do not open ML structures;

observe firm naming convention ctxt: Proof.context;

modernized structure Proof_Context;

modernized structure Proof_Context;

prefer local name spaces; tuned signatures; tuned;

Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;

tuned signature, disentangled dependencies;

Added command for associating user-defined types with SPARK types.

turn YXML.parse_file into a fold

nicer error message from Metis for know failure that isn't the user's fault

correctly handle TFrees that occur in (local) facts -- Metis did the right thing here but Sledgehammer was incorrectly generating spurious preconditions such as "dense_linorder(t_a)"

tuning

remove needless export

more clausification tests

make 48170228f562 work also with "HO_Reas" examples

improve on 0b05cc14c2cb: make sure that a literal variable "?foo" isn't accidentally renamed "?Q", which might be enough to confuse the new Skolemizer (cf. "Clausify.thy" example)

properly implemented definitional CNF for the new Skolemizer (and moved the code for the old Skolemizer -- tuning), removing big chunks for experimental/debugging code

remove experimental code added in 85bb6fbb8e6a

added examples of definitional CNF facts

"unify_first_prem_with_concl" (cf. 9ceb585c097a) sometimes throws an exception, but it is very rarely needed -- catch the exception for now

compile

handle case where the same Skolem name is given different types in different subgoals in the new Skolemizer (this can happen if several type-instances of the same fact are needed by Metis, cf. example in "Clausify.thy") -- the solution reintroduces old code removed in a6725f293377

removed obsolete Skolem counter in new Skolemizer

added outstanding issue to Metis example

use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms

started clausifier examples

make new Skolemizer work also for "metisFT"