Added in four control flags for HOL and FOL translations. Changed functions that perform HOL/FOL translations, and write ATP input to files. Removed some functions that are no longer needed.

Slight modification to trace information.

Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs. Still have old verions of "vampireH","vampireF", "eproverH", "eproverF", which can be called to handle HOL or FOL problems.

Only output arities and class relations if !ResClause.keep_types is true.

some small tuning

ISAR-fied two proofs about equality for abstraction functions.

* Provers/induct: obtain pattern;

added an authors section (please let me know if somebody is left out or unhappy)

some minor tunings

added the version of nominal.thy that contains all properties about support of finite sets

cleaned up all examples so that they work with the current nominal-setting.

finished cleaning up the parts that collect lemmas (with instantiations) under some general names

Corrected treatment of non-recursive abstraction types.

tuned induct proofs;

induct: insert defs in object-logic form; export guess_instance;

tuned induct proofs;

tuned induct proofs;

consume: unfold defs in all major prems;

revert_skolem: fall back on Syntax.deskolem;

forall_conv ~1;

added dummy_pattern;

tuned names;

forall_conv: limit prefix;

fix_tac: proper treatment of major premises in goal; export atomize/rulify interface; tuned;

removed obsolete dummy paragraphs;

tuned;

code generator: case expressions, improved name resolving

added fsub.thy (poplmark challenge) to the examples directory.

Fixed problem with strong induction theorem for datatypes containing no atom types (ind_sort was the empty sort in this case).

send more information with test-takes-too-long message (which tests are still running)

fixed spelling of 'case_conclusion';

tuned induct proofs;

tuned induction proofs;

more robust revert_skolem; tuned;

tuned;

Provers/induct: definitional insts and fixing;

consume: proper treatment of defs; simplified case_conclusion;

added case_conclusion attribute;

(co)induct: taking; induct set: proper treatment of defs;

RuleCases.case_conclusion;

tuned;

added case_conclusion attribute; added coinduct method/attribute; induct method: definsts/fixing/taking; tuned;

improved failure tracking

Datatype_Universe: hide base names only;

added type cases/cases_tactic, and CASES, SUBGOAL_CASES; added consume rule; support named case conclusions; tuned interfaces;

cases_tactic;

moved multi_resolve(s) to drule.ML; cases_tactic;

find_xxxS: term instead of thm;

export map_tags; added multi_resolve(s) -- from Isar/method.ML;

make coinduct actually work; moved some generic code to Pure/Isar/rule_cases.ML; tuned;

Drule.multi_resolves;

declare coinduct rule; tuned;

added code generator syntax

added codegenerator

added code generator syntax

new treatment of polymorphic types, using Sign.const_typargs

added codegen package

added serializer

tweak

fixed some inconveniencies in website

CONJUNCTS;

tuned;

Goal.norm_hhf_protected;

added coinduct attribute; tuned;

added CONJUNCTS: treat conjunction as separate sub-goals;

simpset: added reorient field, set_reorient;

tuned norm_hhf_protected;

removed conj_mono; added conj_curry; tuned;

induct: CONJUNCTS for multiple goals; added coinduct method; tuned;

tuned induct syntax;

FOL: -p 2;

presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy

-- changed the interface of functions vampire_oracle and eprover_oracle.

-- terms are fully typed. -- only the top-level boolean terms are predicates.

-- before converting axiom and conjecture clauses into ResClause.clause format, perform "check_is_fol_term" first.

-- combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.

-- added combinator reduction axioms (typed and untyped) for HOL goals. -- combined make_nnf functions for HOL and FOL goals. -- hypothesis of goals are now also skolemized by inference.

-- split up inputs to ATPs into two groups: temporary files (axioms and goals) and permanent helper files (e.g. combinator reduction axioms).

-- combined "make_nnf" functions for both FOL and HOL vampire/eprover methods.

-- removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL. -- added "check_is_fol_term", which is the same as "check_is_fol", but takes a "term" as input. -- added "check_is_fol" and "check_is_fol_term" into the signature.

tuned document;

tuned;

improved induction proof: local defs/fixes;

tuned Pattern.match/unify; tuned fold;

added deskolem;

added THEN_ALL_NEW_CASES; Syntax.deskolem;

added revert_skolem, mk_def, add_def; export: Goal.norm_hhf'; tuned;

ProofContext.mk_def;

Term.betapplys;

tuned Pattern.match/unify;

added betapplys;

tuned interfaces to support incremental match/unify (cf. versions in type.ML);

tuned;

norm_hhf: no normalization of protected props;

added protect_cong, cong_mono_thm; outer_params: Syntax.deskolem;

induct: support local definitions to be passed through the induction; deprecate open rule cases; misc cleanup;