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 -50 -24 +24 +50 +100 +300 +1000 +3000 +10000 +30000 tip

tuned;
2006-03-08, by wenzelm
Isar/method: goal restriction;
2006-03-08, by wenzelm
constdecl: always allow 'where';
2006-03-08, by wenzelm
deleted some proofs "on comment"
2006-03-08, by urbanc
tuned some proofs
2006-03-08, by urbanc
tuned some of the proofs about fresh_fun
2006-03-08, by urbanc
first running version of type classes
2006-03-08, by haftmann
first running version of type classes
2006-03-08, by haftmann
first running version of type classes
2006-03-08, by haftmann
Frequency strategy. Revised indentation, etc.
2006-03-08, by paulson
*** empty log message ***
2006-03-08, by nipkow
added ROOT.ML
2006-03-07, by obua
Indentation
2006-03-07, by paulson
Tidying and restructuring.
2006-03-07, by paulson
Tidying and tracing. Handling exn CLAUSE so that errors don't reach top-level.
2006-03-07, by paulson
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

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

isabelle