fixed a typo in a comment

tuned;

method: SelectGoals;

method: syntax for SelectGoals;

text: added SelectGoals;

tuned conj_curry;

added extract, retrofit;

added mk_conjunction; tuned conj_curry;

method: restriction to first n sub-goals;

minor changes

more examples

changed and retracted change of location of code lemmas.

ignore repeated vars on lhs, cleanup

improvements for nbe

reformatting

subset_refl now included using the atp attribute

moved the "use" directive

fixed the bugs itroduced by the previous commit

made some small changes to generate nicer latex-output

split the files - Iteration.thy contains the big proof of the iteration combinator - Recursion.thy derives from Iteration the recursion combinator - lam_substs.thy contains the examples (size, substitution and parallel substitution)

Added in a signature.

fixed a problem where a permutation is not analysed when the term is of the form (pi o f) x1...xn This was the case because the head of this term is the constant "nominal.perm". Now an applicability predicate decides the right behaviour of the simproc

streamlined the proof

refined representation of codegen intermediate language

some small tunings

added fresh_fun_eqvt theorem to the theorem collection

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