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

prefer non-strict Execution.print, e.g relevant for redirected ML compiler reports after error (see also e79f76a48449 and 40274e4f5ebf);
2014-08-01, by wenzelm
careful when calling 'Thm.proof_body_of' -- it can throw exceptions
2014-08-01, by blanchet
removed unused stuff;
2014-08-01, by wenzelm
agree on keyword categories with ML;
2014-08-01, by wenzelm
more keyword categories (as in ML);
2014-08-01, by wenzelm
prefer dynamic ML_print_depth if context happens to be available;
2014-07-31, by wenzelm
completion popup supports both ENTER and TAB (default);
2014-07-31, by wenzelm
clarified compile-time use of ML_print_depth;
2014-07-31, by wenzelm
more general notion of "user error" including empty message -- NB: Output.error_message needs non-empty string to emit anything;
2014-07-31, by wenzelm
correctly resolve selector names in default value equations
2014-07-30, by blanchet
update documentation for Lifting/Transfer
2014-07-30, by kuncar
add Isabelle Datatype Manual to the bibliography
2014-07-30, by kuncar
CONTRIBUTORS;
2014-07-30, by wenzelm
NEWS
2014-07-30, by kuncar
better ordering of positive_integral renaming to nn_integral in NEWS
2014-07-29, by hoelzl
made tactic more robust w.r.t. dead variables; tuned;
2014-07-28, by desharna
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
2014-07-27, by blanchet
some actual workaround to remove document nodes;
2014-07-28, by wenzelm
Added tag Isabelle2014-RC1 for changeset c0fd03d13d28
2014-07-27, by wenzelm
tuned;
2014-08-09, by wenzelm
tuned
2014-08-09, by nipkow
add complete_lattice instances for Enum.finite_* types such that quickcheck deals with lattice class operations
2014-08-08, by Andreas Lochbihler
tuned
2014-08-08, by nipkow
no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
2014-08-07, by blanchet
generate nicer 'set' theorems for (co)datatypes
2014-08-07, by blanchet
compile
2014-08-07, by blanchet
took out test driver
2014-08-07, by blanchet
make TPTP tools work on polymorphic (TFF1) problems as well
2014-08-07, by blanchet
put comments between TPTP lines to comply with TPTP BNF
2014-08-07, by blanchet
test driver
2014-08-07, by blanchet

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

isabelle