2010-11-07 wenzelm 2010-11-07 updated generated file;
2010-11-07 wenzelm 2010-11-07 more literal appearance of antiqopen/antiqclose;
2010-11-07 wenzelm 2010-11-07 '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-06 wenzelm 2010-11-06 continue after failed commands;
2010-11-06 wenzelm 2010-11-06 added Keyword.is_heading (cf. Scala version); tuned;
2010-11-06 wenzelm 2010-11-06 updated keywords;
2010-11-06 wenzelm 2010-11-06 mark 'cd' and 'commit' as control command -- not usable in asynchronous document model, likely to cause confusion in Proof General;
2010-11-06 wenzelm 2010-11-06 somewhat more uniform timing markup in ML vs. Scala;
2010-11-06 wenzelm 2010-11-06 somewhat more uniform timing in ML vs. Scala;
2010-11-06 wenzelm 2010-11-06 added Markup.Double, Markup.Double_Property; tuned;
2010-11-06 wenzelm 2010-11-06 explicit "timing" status for toplevel transactions;
2010-11-06 wenzelm 2010-11-06 tuned;
2010-11-06 wenzelm 2010-11-06 tuned comments;
2010-11-06 krauss 2010-11-06 abolished obscure goal variant of [split_format] -- unused (cf. d1c14898fd04), unrelated to '(complete)' variant, and not at all canonical
2010-11-05 wenzelm 2010-11-05 moved ISABELLE_IDENTIFIER from ISABELLE_OUTPUT further up to ISABELLE_HOME_USER;
2010-11-05 wenzelm 2010-11-05 updated keywords;
2010-11-05 wenzelm 2010-11-05 reflect actual content of /home/isabelle/.html-data/cgi-bin/hgwebdir.cgi;
2010-11-05 wenzelm 2010-11-05 eliminated spurious "firstline" filters for improved display of Isabelle history logs: one item per line, without special headline; more uniform shortlogentry and filelogentry;
2010-11-05 wenzelm 2010-11-05 reflect actual content of /home/isabelle-repository/hgweb-templates/isabelle by krauss;
2010-11-05 wenzelm 2010-11-05 obsolete -- python installation on www4 is not modified (despite remaining "firstline" in graph and syndication views);
2010-11-05 wenzelm 2010-11-05 explicit indication of some remaining violations of the Isabelle/ML interrupt model;
2010-11-05 wenzelm 2010-11-05 updated generated file, overwriting 55a1693affb6 whose content appears to be in the thy source already;
2010-11-05 wenzelm 2010-11-05 proper spelling; proper format;
2010-11-05 hoelzl 2010-11-05 merged
2010-11-05 hoelzl 2010-11-05 Extend convex analysis by Bogdan Grechuk
2010-11-05 blanchet 2010-11-05 merged
2010-11-05 blanchet 2010-11-05 fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
2010-11-05 blanchet 2010-11-05 make Mirabelle work correctly if the prover (e.g. the SMT solver) returns no timing information
2010-11-04 blanchet 2010-11-04 pass proper type to SMT_Builtin.is_builtin
2010-11-04 blanchet 2010-11-04 remove " s" suffix since seconds are now implicit
2010-11-04 blanchet 2010-11-04 ignore facts with only theory constants in them
2010-11-04 blanchet 2010-11-04 cosmetics
2010-11-04 blanchet 2010-11-04 use the SMT integration's official list of built-ins
2010-11-05 haftmann 2010-11-05 added class relation group_add < cancel_semigroup_add
2010-11-05 bulwahn 2010-11-05 merged
2010-11-05 bulwahn 2010-11-05 changing timeout to real value; handling Interrupt and Timeout more like nitpick does
2010-11-05 bulwahn 2010-11-05 added two lemmas about injectivity of concat to the list theory
2010-11-05 bulwahn 2010-11-05 adding documentation of some quickcheck options
2010-11-05 haftmann 2010-11-05 merged
2010-11-04 haftmann 2010-11-04 Code.check_const etc.: reject too specific types
2010-11-04 haftmann 2010-11-04 corrected quoting
2010-11-04 haftmann 2010-11-04 added lemma length_alloc
2010-11-04 haftmann 2010-11-04 dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
2010-11-04 haftmann 2010-11-04 added note on countable types
2010-11-04 boehmes 2010-11-04 simulate more closely the behaviour of the tactic
2010-11-04 wenzelm 2010-11-04 merged
2010-11-04 haftmann 2010-11-04 merged
2010-11-04 haftmann 2010-11-04 merged
2010-11-03 haftmann 2010-11-03 dropped debug message
2010-11-03 haftmann 2010-11-03 more precise text
2010-11-03 haftmann 2010-11-03 SMLdummy target
2010-11-03 haftmann 2010-11-03 fixed typos
2010-11-03 haftmann 2010-11-03 moved theory Quicksort from Library/ to ex/
2010-11-03 haftmann 2010-11-03 Theory Multiset provides stable quicksort implementation of sort_key.
2010-11-03 haftmann 2010-11-03 added code lemmas for stable parametrized quicksort
2010-11-03 haftmann 2010-11-03 tuned proof
2010-11-04 blanchet 2010-11-04 moved file in makefile to reflect actual dependencies
2010-11-03 blanchet 2010-11-03 give E one more second, to prevent cases where it finds a proof but has no time to print it
2010-11-03 blanchet 2010-11-03 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages; updated docs
2010-11-03 blanchet 2010-11-03 don't be overly verbose in Sledgehammer's minimizer