refined Cooper.tac / "presburger" method: Subgoal.FOCUS_PARAMS allows to solve more problems with outer quantifiers, e.g "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2";
clarified thin_prems_tac: fail as tactic without error;
#!/usr/bin/env bash
#
# Author: Makarius
#
# Default Isabelle application wrapper.
exec "$(dirname "$0")"/bin/isabelle jedit "$@"