isabelle: Graph

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
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
adding documentation of some quickcheck options
2010-11-05, by bulwahn
merged
2010-11-05, by haftmann
Code.check_const etc.: reject too specific types
2010-11-04, by haftmann
corrected quoting
2010-11-04, by haftmann
added lemma length_alloc
2010-11-04, by haftmann
dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
2010-11-04, by haftmann
added note on countable types
2010-11-04, by haftmann
simulate more closely the behaviour of the tactic
2010-11-04, by boehmes
merged
2010-11-04, by wenzelm
merged
2010-11-04, by haftmann
merged
2010-11-04, by haftmann
dropped debug message
2010-11-03, by haftmann
more precise text
2010-11-03, by haftmann
SMLdummy target
2010-11-03, by haftmann
fixed typos
2010-11-03, by haftmann
moved theory Quicksort from Library/ to ex/
2010-11-03, by haftmann
Theory Multiset provides stable quicksort implementation of sort_key.
2010-11-03, by haftmann
added code lemmas for stable parametrized quicksort
2010-11-03, by haftmann
tuned proof
2010-11-03, by haftmann
moved file in makefile to reflect actual dependencies
2010-11-04, by blanchet
give E one more second, to prevent cases where it finds a proof but has no time to print it
2010-11-03, by blanchet
use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages;
2010-11-03, by blanchet
don't be overly verbose in Sledgehammer's minimizer
2010-11-03, by blanchet
standardize on seconds for Nitpick and Sledgehammer timeouts
2010-11-03, by blanchet
cleaned up
2010-11-03, by nipkow
added property "tooltip-margin";
2010-11-04, by wenzelm
clarified tooltips: message output by default, extra info via control/command;
2010-11-04, by wenzelm
warn in correlation with report -- avoid spurious message duplicates;
2010-11-04, by wenzelm
tuned;
2010-11-04, by wenzelm
feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);
2010-11-03, by wenzelm
merged
2010-11-03, by boehmes
updated SMT certificates
2010-11-03, by boehmes
standardize timeout value based on reals
2010-11-03, by boehmes
merged
2010-11-03, by wenzelm
merged
2010-11-03, by huffman
change default_sort of HOLCF from pcpo to bifinite; rename command 'new_domain' to 'domain'; rename 'domain' to 'domain (unsafe)'
2010-10-30, by huffman
merged
2010-10-30, by huffman
renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun
2010-10-29, by huffman
renamed lemma cont2cont_Rep_CFun to cont2cont_APP
2010-10-29, by huffman
simplify proof of typedef_cont_Abs
2010-10-29, by huffman
rename constant trifte to tr_case
2010-10-27, by huffman
add 'LAM (Def x). t' as alternative syntax for 'FLIFT x. t'
2010-10-27, by huffman
make syntax of continuous if-then-else consistent with HOL if-then-else
2010-10-27, by huffman
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
2010-10-27, by huffman
polyml_as_definition does not require explicit dependencies on external ML files
2010-11-03, by haftmann
explicit warning about opaque signature matching -- saves extra paragraph in implementation manual;
2010-11-03, by wenzelm
discontinued obsolete function sys_error and exception SYS_ERROR;
2010-11-03, by wenzelm
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
2010-11-03, by wenzelm
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
2010-11-03, by wenzelm
try_param_tac: plain user error appears more appropriate;
2010-11-03, by wenzelm
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
2010-11-03, by wenzelm
eliminated dead code;
2010-11-03, by wenzelm
more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR;
2010-11-03, by wenzelm
removed assumption
2010-11-03, by nipkow
more on naming tactics;
2010-11-02, by wenzelm