2010-11-05 wenzelm explicit indication of some remaining violations of the Isabelle/ML interrupt model;
2010-11-05 wenzelm updated generated file, overwriting 55a1693affb6 whose content appears to be in the thy source already;
2010-11-05 wenzelm proper spelling;
2010-11-05 hoelzl merged
2010-11-05 hoelzl Extend convex analysis by Bogdan Grechuk
2010-11-05 blanchet merged
2010-11-05 blanchet fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)
2010-11-05 blanchet make Mirabelle work correctly if the prover (e.g. the SMT solver) returns no timing information
2010-11-04 blanchet pass proper type to SMT_Builtin.is_builtin
2010-11-04 blanchet remove " s" suffix since seconds are now implicit
2010-11-04 blanchet ignore facts with only theory constants in them
2010-11-04 blanchet cosmetics
2010-11-04 blanchet use the SMT integration's official list of built-ins
2010-11-05 haftmann added class relation group_add < cancel_semigroup_add
2010-11-05 bulwahn merged
2010-11-05 bulwahn changing timeout to real value; handling Interrupt and Timeout more like nitpick does
2010-11-05 bulwahn added two lemmas about injectivity of concat to the list theory
2010-11-05 bulwahn adding documentation of some quickcheck options
2010-11-05 haftmann merged
2010-11-04 haftmann Code.check_const etc.: reject too specific types
2010-11-04 haftmann corrected quoting
2010-11-04 haftmann added lemma length_alloc
2010-11-04 haftmann dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document
2010-11-04 haftmann added note on countable types
2010-11-04 boehmes simulate more closely the behaviour of the tactic
2010-11-04 wenzelm merged
2010-11-04 haftmann merged
2010-11-04 haftmann merged
2010-11-03 haftmann dropped debug message
2010-11-03 haftmann more precise text
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip