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 +30000 tip

tuned signatures;
2011-04-04, by wenzelm
streamlined token list operations, assuming that the order of union does not matter;
2011-04-04, by wenzelm
misc tuning and clarification;
2011-04-04, by wenzelm
merged
2011-04-04, by wenzelm
document "nitpick(_params)", "refute(_params)", "try", "sledgehammer(_params)", and "solve_direct"
2011-04-04, by blanchet
refactoring generator definition in quickcheck and removing clone
2011-04-04, by bulwahn
use the proper contexts/simpsets/etc. in the TPTP proof method
2011-04-04, by blanchet
merged
2011-04-04, by blanchet
make sure that Nitpick problem generation for cardinality 50 doesn't cause problems for lower cardinality by specifying the "batch_size" option
2011-04-04, by blanchet
merged
2011-04-04, by paulson
Deletion of all semicolons, because they interfere with Proof General
2011-04-04, by paulson
raised timeouts further, for SML/NJ -- because of variations in machines/compilers, fixed timeouts can merely prevent non-termination, not enforce particular performance characteristics.
2011-04-04, by krauss
tuned proofs
2011-04-03, by haftmann
tuned proof
2011-04-02, by haftmann
direct pretty printing of parsetrees -- prevent diagnostic output from crashing due to undeclared entities;
2011-04-04, by wenzelm
added Position.reports convenience;
2011-04-03, by wenzelm
show more tooltip/sub-expression markup;
2011-04-03, by wenzelm
show tooltip/sub-expression for entity markup;
2011-04-03, by wenzelm
merged
2011-04-01, by wenzelm
remove unnecessary prob_preserving
2011-04-01, by hoelzl
add prob_space_vimage
2011-04-01, by hoelzl
use Unsynchronized.change convenience, which also emphasizes the raw access to these references (which happen to be local here);
2011-04-01, by wenzelm
fixed accidental redefinition
2011-04-01, by krauss
save reflexivity steps in discharging Z3 Skolemization hypotheses
2011-04-01, by boehmes
adding an exhaustive validator for quickcheck's batch validating; moving strip_imp; minimal setup for bounded_forall
2011-04-01, by bulwahn
adding general interface for batch validators in quickcheck
2011-04-01, by bulwahn
remove workaround 8f25605e646c, which is no longer necessary thanks to 173b0f488428
2011-04-01, by blanchet
scheduler for judgement day
2011-04-01, by krauss
re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
2011-04-01, by boehmes
make configuration of (SMT) full monomorphization more flexible: turn boolean argument into a configuration option
2011-04-01, by boehmes
merged
2011-04-01, by bulwahn
adding time profiling in quickcheck's batch testing for further diagnosis in IsaCoSy
2011-04-01, by bulwahn
raised timeouts further, for SML/NJ
2011-04-01, by krauss
adapted parsing of session timing (cf. e86b10c68f0b)
2011-04-01, by krauss
merged
2011-03-31, by bulwahn
adapting Quickcheck_Narrowing (overseen in 234ec7011e5d); commenting out some examples temporarily
2011-03-31, by bulwahn
provide a flag controlling whether all provided facts should be instantiated, possibly inventing new types (which does not work well with Sledgehammer)
2011-03-31, by boehmes
start monomorphization process with subgoal, not entire goal, to avoid needless instances (and only print monomorphization messages in debug mode)
2011-03-31, by blanchet
temporary workaround: filter out spurious monomorphic instances
2011-03-31, by blanchet
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
2011-03-31, by blanchet
added support for "dest:" to "try"
2011-03-31, by blanchet
corrected infix precedence for boolean operators in Haskell
2011-03-31, by haftmann
merged
2011-03-31, by bulwahn
removing dead code in exhaustive_generators
2011-03-30, by bulwahn
removing junk that should not have been committed
2011-03-30, by bulwahn
modernized specifications;
2011-03-30, by wenzelm
accomodate autofix discipline of non-body context;
2011-03-30, by wenzelm
session timing: show pseudo-speedup factor;
2011-03-30, by wenzelm
visualize skolem and hilite (undeclared frees);
2011-03-30, by wenzelm
more informative markup_free;
2011-03-30, by wenzelm
inline lemmas instead of accidental physical addressing -- explicit is better than implicit;
2011-03-30, by wenzelm
tuned white space and indentation;
2011-03-30, by wenzelm
actually check list comprehension examples;
2011-03-30, by wenzelm
products of probability measures are probability measures
2011-03-30, by hoelzl
real multiplication is continuous
2011-03-30, by hoelzl
add lebesgue_real_affine
2011-03-30, by hoelzl
renewing specifications in HOL: replacing types by type_synonym
2011-03-30, by bulwahn
moved TimeLimit.timeLimit closure to limit time of compilation and execution to avoid the strange, occasional occuring message Exception trace for exception - Interrupt -- probably due to race conditions of a fast execution within the TimeLimit.timelimit closure
2011-03-30, by bulwahn
adding a regression test for SML_Quickcheck; putting SML_Quickcheck back in shape
2011-03-30, by bulwahn
NEWS
2011-03-30, by bulwahn

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

isabelle