2006-03-07 haftmann 2006-03-07 substantial improvement in codegen iml
2006-03-07 mengj 2006-03-07 Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset. The hash table (for removing duplicate) now stores clauses as Term.term with names.
2006-03-07 mengj 2006-03-07 relevance_filter takes input axioms as Term.term.
2006-03-07 mengj 2006-03-07 Proof reconstruction now only takes names of theorems as input.
2006-03-07 mengj 2006-03-07 Added tptp_write_file to write all necessary ATP input clauses to one file.
2006-03-07 mengj 2006-03-07 tptp_write_file now takes goals and axioms as Term.term and writes them to a file.
2006-03-07 mengj 2006-03-07 Added functions to retrieve local and global atpset rules. cnf thms to Term.term format.
2006-03-07 mengj 2006-03-07 Moved the settings for ATP time limit to res_atp.ML
2006-03-07 mengj 2006-03-07 Merged res_atp_setup.ML into res_atp.ML. HOL translation is integrated with background Isabelle-ATP linkup. Both ATP methods and background linkup retrieve lemmas stored in claset, simpset and atpset.
2006-03-07 mengj 2006-03-07 When ATP methods call ATPs, all input clauses from one subgoal are written to one file.
2006-03-07 mengj 2006-03-07 Merged res_atp_setup.ML into res_atp.ML.
2006-03-05 wenzelm 2006-03-05 SELECT_GOAL: fixed trivial case;
2006-03-05 webertj 2006-03-05 fixed a typo in a comment
2006-03-04 wenzelm 2006-03-04 tuned;
2006-03-04 wenzelm 2006-03-04 method: SelectGoals;
2006-03-04 wenzelm 2006-03-04 method: syntax for SelectGoals;
2006-03-04 wenzelm 2006-03-04 text: added SelectGoals;
2006-03-04 wenzelm 2006-03-04 tuned conj_curry;
2006-03-04 wenzelm 2006-03-04 added extract, retrofit;
2006-03-04 wenzelm 2006-03-04 added mk_conjunction; tuned conj_curry;
2006-03-04 wenzelm 2006-03-04 method: restriction to first n sub-goals;
2006-03-03 nipkow 2006-03-03 minor changes
2006-03-03 nipkow 2006-03-03 more examples
2006-03-03 nipkow 2006-03-03 changed and retracted change of location of code lemmas.
2006-03-03 nipkow 2006-03-03 ignore repeated vars on lhs, cleanup
2006-03-03 haftmann 2006-03-03 improvements for nbe
2006-03-02 paulson 2006-03-02 reformatting
2006-03-02 paulson 2006-03-02 subset_refl now included using the atp attribute
2006-03-02 paulson 2006-03-02 moved the "use" directive
2006-03-02 urbanc 2006-03-02 fixed the bugs itroduced by the previous commit
2006-03-02 urbanc 2006-03-02 made some small changes to generate nicer latex-output
2006-03-02 urbanc 2006-03-02 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)
2006-03-02 mengj 2006-03-02 Added in a signature.
2006-03-01 urbanc 2006-03-01 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
2006-03-01 urbanc 2006-03-01 streamlined the proof
2006-03-01 haftmann 2006-03-01 refined representation of codegen intermediate language
2006-03-01 urbanc 2006-03-01 some small tunings
2006-03-01 urbanc 2006-03-01 added fresh_fun_eqvt theorem to the theorem collection
2006-03-01 urbanc 2006-03-01 added initialisation-code for finite_guess
2006-03-01 urbanc 2006-03-01 made some small tunings in the decision-procedure (in the order how the "small" tactics are called)
2006-03-01 mengj 2006-03-01 Added setup for "atpset" (a rule set for ATPs).
2006-03-01 mengj 2006-03-01 Added file Tools/res_atpset.ML.
2006-03-01 mengj 2006-03-01 Merged HOL and FOL clauses and combined some functions.
2006-03-01 mengj 2006-03-01 A new file that sets up rules set used by ATPs. Rules are added to and removed from the set using "atp" attribute.
2006-03-01 urbanc 2006-03-01 some minor tuning on the proofs
2006-02-28 urbanc 2006-02-28 initial commit (especially 2nd half needs to be cleaned up)
2006-02-28 paulson 2006-02-28 removal of theory blacklist
2006-02-28 paulson 2006-02-28 new order for arity clauses
2006-02-28 paulson 2006-02-28 fixed but in freeze_spec
2006-02-28 paulson 2006-02-28 splitting up METAHYPS into smaller functions
2006-02-28 paulson 2006-02-28 typos
2006-02-27 urbanc 2006-02-27 added a finite_guess tactic, which solves automatically finite-support goals
2006-02-27 haftmann 2006-02-27 class package and codegen refinements
2006-02-27 haftmann 2006-02-27 added nbe
2006-02-27 nipkow 2006-02-27 added temp. nbe test
2006-02-27 nipkow 2006-02-27 added nbe, updated neb_*
2006-02-27 nipkow 2006-02-27 added nbe
2006-02-27 ballarin 2006-02-27 Typo.
2006-02-27 urbanc 2006-02-27 added support for arbitrary atoms in the simproc
2006-02-26 wenzelm 2006-02-26 put_thms: do_index;