tuned error -- allow user to click on hyperlink to open remote file;

no comment -- File.read_stream already enforces UTF8 (like HTML5) and HTTP servers often produce a wrong charset encoding;

improved support for external URLs, based on standard Java network operations;

basic URL operations (with Isabelle/Scala error handling);

proper Args.name vs. Args.text as documented (in contrast to adhoc union in 75aaee32893d, which had to cope with more limited Args.T);

allow text cartouches in regular outer syntax categories "text" and "altstring";

tuned comments (see Scala version);

dismiss popups more carefully (amending 7e8c11011fdf), notably allow mouse dragging within some tooltip, e.g. for text selection;

clarifed results range;

more explicit message discrimination;

avoid confusion about pointless cursor movement with external links;

prefer regular Goal_Display.pretty_goals, without censorship of options;

more standard names;

proper context for print_tac;

more conventional tactic programming; tuned;

tuned;

reintroduce example (cf. 39281b3e4fac)

use mutual clique information (cf. c451cf8b29c8) to make N2M more robust

made N2M tactic more robust

generate cliques for 'prim(co)rec' N2M

thread mutual cliques through

generalize ln/log_powr; add log_base_powr/pow

parametricity transfer rule for INFIMUM, SUPREMUM

add divide_simps

field_simps: better support for negation and division, and power

revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules

merged

more native rm_tree, using Java 7 facilities;

expose more bad cases;

tuned signature;