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

better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
2010-11-08, by boehmes
merged
2010-11-08, by haftmann
corrected slip: must keep constant map, not type map; tuned code
2010-11-08, by haftmann
constructors to datatypes in code_reflect can be globbed; dropped unused code
2010-11-08, by haftmann
adding code and theory for smallvalue generators, but do not setup the interpretation yet
2010-11-08, by bulwahn
make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice
2010-11-08, by blanchet
better detection of completely irrelevant facts
2010-11-08, by blanchet
always use a hard timeout in Mirabelle
2010-11-07, by blanchet
use "smt" (rather than "metis") to reconstruct SMT proofs
2010-11-07, by blanchet
don't pass too many facts on the first iteration of the SMT solver
2010-11-07, by blanchet
catch TimeOut exception
2010-11-07, by blanchet
ensure the SMT solver respects the timeout -- Mirabelle revealed cases where "smt_filter" apparently never returns
2010-11-07, by blanchet
if SMT used as a filter in a loop fails at each iteration, returns the first error, not the last, since it is more informative -- the first error typically says "out of memory", whereas the last might well be "the SMT problem is unprovable", which should be no surprise if too many facts were removed
2010-11-07, by blanchet
removed explicit "Interrupt" handling for conformity with async model -- unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway
2010-11-07, by blanchet
make Nitpick datatype tests faster to make timeout less likely
2010-11-06, by blanchet
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
2010-11-06, by blanchet
always honor the max relevant constraint
2010-11-06, by blanchet
more robust treatment of suppressed quotes concerning replacement text -- for improved copy/paste behaviour;
2010-11-08, by wenzelm
updated generated files;
2010-11-08, by wenzelm
tweaked pdf setup to allow modification of \pdfminorversion;
2010-11-07, by wenzelm
merged;
2010-11-07, by wenzelm
updated generated files;
2010-11-07, by wenzelm
basic setup for literal replacement text in PDF, to support copy/paste of Isabelle symbols;
2010-11-07, by wenzelm
updated generated file;
2010-11-07, by wenzelm
more literal appearance of antiqopen/antiqclose;
2010-11-07, by wenzelm
'example_proof' is treated as non-schematic statement with irrelevant proof (NB: even regular proofs can contain unreachable parts wrt. the graph of proof promises);
2010-11-07, by wenzelm
continue after failed commands;
2010-11-06, by wenzelm
added Keyword.is_heading (cf. Scala version);
2010-11-06, by wenzelm
updated keywords;
2010-11-06, by wenzelm
mark 'cd' and 'commit' as control command -- not usable in asynchronous document model, likely to cause confusion in Proof General;
2010-11-06, by wenzelm
somewhat more uniform timing markup in ML vs. Scala;
2010-11-06, by wenzelm
somewhat more uniform timing in ML vs. Scala;
2010-11-06, by wenzelm
added Markup.Double, Markup.Double_Property;
2010-11-06, by wenzelm
explicit "timing" status for toplevel transactions;
2010-11-06, by wenzelm
tuned;
2010-11-06, by wenzelm
tuned comments;
2010-11-06, by wenzelm
abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical
2010-11-06, by krauss
moved ISABELLE_IDENTIFIER from ISABELLE_OUTPUT further up to ISABELLE_HOME_USER;
2010-11-05, by wenzelm
updated keywords;
2010-11-05, by wenzelm
reflect actual content of /home/isabelle/.html-data/cgi-bin/hgwebdir.cgi;
2010-11-05, by wenzelm
eliminated spurious "firstline" filters for improved display of Isabelle history logs: one item per line, without special headline;
2010-11-05, by wenzelm
reflect actual content of /home/isabelle-repository/hgweb-templates/isabelle by krauss;
2010-11-05, by wenzelm
obsolete -- python installation on www4 is not modified (despite remaining "firstline" in graph and syndication views);
2010-11-05, by wenzelm
explicit indication of some remaining violations of the Isabelle/ML interrupt model;
2010-11-05, by wenzelm
updated generated file, overwriting 55a1693affb6 whose content appears to be in the thy source already;
2010-11-05, by wenzelm
proper spelling;
2010-11-05, by wenzelm
merged
2010-11-05, by hoelzl
Extend convex analysis by Bogdan Grechuk
2010-11-05, by hoelzl
merged
2010-11-05, by blanchet
fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
2010-11-05, by blanchet
make Mirabelle work correctly if the prover (e.g. the SMT solver) returns no timing information
2010-11-05, by blanchet
pass proper type to SMT_Builtin.is_builtin
2010-11-04, by blanchet
remove " s" suffix since seconds are now implicit
2010-11-04, by blanchet
ignore facts with only theory constants in them
2010-11-04, by blanchet
cosmetics
2010-11-04, by blanchet
use the SMT integration's official list of built-ins
2010-11-04, by blanchet
added class relation group_add < cancel_semigroup_add
2010-11-05, by haftmann
merged
2010-11-05, by bulwahn
changing timeout to real value; handling Interrupt and Timeout more like nitpick does
2010-11-05, by bulwahn
added two lemmas about injectivity of concat to the list theory
2010-11-05, by bulwahn

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

isabelle