explicit indication of some remaining violations of the Isabelle/ML interrupt model;

updated generated file, overwriting 55a1693affb6 whose content appears to be in the thy source already;

proper spelling; proper format;

merged

Extend convex analysis by Bogdan Grechuk

merged

fixed handling of theorem references such as "foo bar" (with quotes), "foo bar(2)", and "foo bar(2)"(2)

make Mirabelle work correctly if the prover (e.g. the SMT solver) returns no timing information

pass proper type to SMT_Builtin.is_builtin

remove " s" suffix since seconds are now implicit

ignore facts with only theory constants in them

cosmetics

use the SMT integration's official list of built-ins

added class relation group_add < cancel_semigroup_add

merged

changing timeout to real value; handling Interrupt and Timeout more like nitpick does

added two lemmas about injectivity of concat to the list theory

adding documentation of some quickcheck options

merged

Code.check_const etc.: reject too specific types

corrected quoting

added lemma length_alloc

dropped return abbreviation for Pair -- confusing if combined with monad syntax; tuned document

added note on countable types

simulate more closely the behaviour of the tactic

merged

merged

merged

dropped debug message

more precise text