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

merged
2010-11-08, by huffman
merged
2010-11-06, by huffman
(infixl "<<" 55) -> (infix "<<" 50)
2010-11-05, by huffman
simplify some proofs
2010-11-03, by huffman
remove unnecessary stuff from Discrete.thy
2010-11-03, by huffman
remove some unnecessary lemmas; move monofun_LAM to Cfun.thy
2010-11-03, by huffman
add lemma eq_imp_below
2010-11-03, by huffman
discontinue a bunch of legacy theorem names
2010-11-03, by huffman
move a few admissibility lemmas into FOCUS/Stream_adm.thy
2010-11-03, by huffman
simplify some proofs
2010-11-03, by huffman
compile -- 7550b2cba1cb broke the build
2010-11-08, by blanchet
merge
2010-11-08, by blanchet
recognize Vampire error
2010-11-08, by blanchet
return the process return code along with the process outputs
2010-11-08, by boehmes
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

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

isabelle