isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

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

tuning whitespace
2014-08-05, by blanchet
tuned skolemization
2014-08-05, by blanchet
rationalize Skolem names
2014-08-05, by blanchet
tuning
2014-08-05, by blanchet
tuned code
2014-08-05, by blanchet
don't rename variables which will be renamed later anyway
2014-08-05, by blanchet
normalize skolem argument variable names so that they coincide when taking the conjunction
2014-08-05, by blanchet
tuning
2014-08-05, by blanchet
tuned comments
2014-08-04, by blanchet
deal with E definitions
2014-08-04, by blanchet
updated 'compress' docs
2014-08-04, by blanchet
cleaner 'compress' option
2014-08-04, by blanchet
renamed 'sh_minimize' to 'minimize'; compile;
2014-08-04, by blanchet
restored more sorting
2014-08-04, by blanchet
tuned terminology (cf. 'isar_proofs' option)
2014-08-04, by blanchet
sort facts in minimizer as well
2014-08-04, by blanchet
default on 'metis' for ATPs if preplaying is disabled
2014-08-04, by blanchet
more informative preplay failures
2014-08-04, by blanchet
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
2014-08-04, by blanchet
slightly earlier exit from preplaying
2014-08-04, by blanchet
honor 'dont_minimize' option when preplaying one-liner proof
2014-08-04, by blanchet
Metis is being used to emulate E steps;
2014-06-22, by sultana
updated application of print_tac to take context parameter;
2014-06-22, by sultana
better duplicate detection
2014-08-02, by blanchet
normalize conjectures vs. negated conjectures when comparing terms
2014-08-01, by blanchet
tweaked 'clone' formula detection
2014-08-01, by blanchet
fine-tuned Isar reconstruction, esp. boolean simplifications
2014-08-01, by blanchet
centralized boolean simplification so that e.g. LEO-II benefits from it
2014-08-01, by blanchet
careful when compressing 'obtains'
2014-08-01, by blanchet
better handling of variable names
2014-08-01, by blanchet
try to get rid of skolems first
2014-08-01, by blanchet
nicer generated variable names
2014-08-01, by blanchet
tuning
2014-08-01, by blanchet
tuning
2014-08-01, by blanchet
no need to 'obtain' variables not in formula
2014-08-01, by blanchet
more precise handling of LEO-II skolemization
2014-08-01, by blanchet
beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
2014-08-01, by blanchet
tuning
2014-08-01, by blanchet
peek instead of joining -- is perhaps less risky
2014-08-01, by blanchet
export ML function
2014-08-01, by blanchet
compile
2014-08-01, by blanchet
removed 'metisFT' support in Mirabelle
2014-08-01, by blanchet
removed Mirabelle minimization code
2014-08-01, by blanchet
modernized Mirabelle (a bit) and made it compile
2014-08-01, by blanchet
restored a bit of laziness
2014-08-01, by blanchet
reorder quantifiers to ease Z3 skolemization
2014-08-01, by blanchet
tuned order of arguments
2014-08-01, by blanchet
tuned name context code
2014-08-01, by blanchet
tuned whitespace
2014-08-01, by blanchet
more rational unskolemizing of names
2014-08-01, by blanchet
added appropriate method for skolemization of Z3 steps to the mix
2014-08-01, by blanchet
pushing skolems under 'iff' sometimes breaks things further down the proof (as was to be feared)
2014-08-01, by blanchet
honor 'try0' also for one-liners
2014-08-01, by blanchet
tentatively took out 'fastforce' from the set of tried methods -- it seems to be largely subsumed and is hard to silence
2014-08-01, by blanchet
further minimize one-liner
2014-08-01, by blanchet
tuning
2014-08-01, by blanchet
eliminated needlessly complex message tail
2014-08-01, by blanchet
updated NEWS
2014-08-01, by blanchet
update documentation after removal of 'min' subcommand
2014-08-01, by blanchet
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
2014-08-01, by blanchet

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

isabelle