Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
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
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
Merged res_atp_setup.ML into res_atp.ML.
2006-03-07, by mengj
SELECT_GOAL: fixed trivial case;
2006-03-05, by wenzelm
fixed a typo in a comment
2006-03-05, by webertj
tuned;
2006-03-04, by wenzelm
method: SelectGoals;
2006-03-04, by wenzelm
method: syntax for SelectGoals;
2006-03-04, by wenzelm
text: added SelectGoals;
2006-03-04, by wenzelm
tuned conj_curry;
2006-03-04, by wenzelm
added extract, retrofit;
2006-03-04, by wenzelm
added mk_conjunction;
2006-03-04, by wenzelm
method: restriction to first n sub-goals;
2006-03-04, by wenzelm
minor changes
2006-03-03, by nipkow
more examples
2006-03-03, by nipkow
changed and retracted change of location of code lemmas.
2006-03-03, by nipkow
ignore repeated vars on lhs, cleanup
2006-03-03, by nipkow
improvements for nbe
2006-03-03, by haftmann
reformatting
2006-03-02, by paulson
subset_refl now included using the atp attribute
2006-03-02, by paulson
moved the "use" directive
2006-03-02, by paulson
fixed the bugs itroduced by the previous commit
2006-03-02, by urbanc
made some small changes to generate nicer latex-output
2006-03-02, by urbanc
split the files
2006-03-02, by urbanc
Added in a signature.
2006-03-02, by mengj
fixed a problem where a permutation is not analysed
2006-03-01, by urbanc
streamlined the proof
2006-03-01, by urbanc
refined representation of codegen intermediate language
2006-03-01, by haftmann
some small tunings
2006-03-01, by urbanc
added fresh_fun_eqvt theorem to the theorem collection
2006-03-01, by urbanc
added initialisation-code for finite_guess
2006-03-01, by urbanc
made some small tunings in the decision-procedure
2006-03-01, by urbanc
Added setup for "atpset" (a rule set for ATPs).
2006-03-01, by mengj
Added file Tools/res_atpset.ML.
2006-03-01, by mengj
Merged HOL and FOL clauses and combined some functions.
2006-03-01, by mengj
less
more
|
(0)
-10000
-3000
-1000
-300
-100
-60
+60
+100
+300
+1000
+3000
+10000
+30000
tip