isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -10000 -3000 -1000 -300 -100 -14 +14 +100 +300 +1000 +3000 +10000 +30000 tip

Tidying. clausify_rules_pairs_abs now returns clauses in the same order as before.
2006-03-07, by paulson
Tidying. New invoke_atp_ml for top-level debugging. Flag to force FOL mode.
2006-03-07, by paulson
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
2006-03-07, by paulson
Added HOL-ZF to Isabelle.
2006-03-07, by obua
substantial improvement in codegen iml
2006-03-07, by haftmann
Function get_clasimp_atp_lemmas gets all lemmas from claset, simpet and atpset.
2006-03-07, by mengj
relevance_filter takes input axioms as Term.term.
2006-03-07, by mengj
Proof reconstruction now only takes names of theorems as input.
2006-03-07, by mengj
Added tptp_write_file to write all necessary ATP input clauses to one file.
2006-03-07, by mengj
tptp_write_file now takes goals and axioms as Term.term and writes them to a file.
2006-03-07, by mengj
Added functions to retrieve local and global atpset rules.
2006-03-07, by mengj
Moved the settings for ATP time limit to res_atp.ML
2006-03-07, by mengj
Merged res_atp_setup.ML into res_atp.ML.
2006-03-07, by mengj
When ATP methods call ATPs, all input clauses from one subgoal are written to one file.
2006-03-07, by mengj

less more | (0) -10000 -3000 -1000 -300 -100 -14 +14 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle