isabelle: Graph

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