added initialisation-code for finite_guess

made some small tunings in the decision-procedure (in the order how the "small" tactics are called)

Added setup for "atpset" (a rule set for ATPs).

Added file Tools/res_atpset.ML.

Merged HOL and FOL clauses and combined some functions.

A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.

some minor tuning on the proofs

initial commit (especially 2nd half needs to be cleaned up)

removal of theory blacklist

new order for arity clauses

fixed but in freeze_spec

splitting up METAHYPS into smaller functions

typos

added a finite_guess tactic, which solves automatically finite-support goals

class package and codegen refinements

added nbe

added temp. nbe test

added nbe, updated neb_*

added nbe

Typo.

added support for arbitrary atoms in the simproc

put_thms: do_index;

rewrite_goals_rule_aux: actually use prems if present;

add_local: do_index;

replaced the lemma at_two by at_different; this lemma now proves EX b. a != b

improved the decision-procedure for permutations; now uses a simproc FIXME: the simproc still needs to be adapted for arbitrary atom types

improved codegen bootstrap

change in codegen syntax

some refinements

added more detailed data to consts