common context menu for Isabelle/jEdit;

tuned;

tuned;

tuned spelling;

tuned menu;

NEWS;

tuned spelling;

proper signature for dynamic BeanShell action;

tuned;

added context menu for spell checker actions;

full repaint after dictionary update;

some actions to maintain spell-checker dictionary;

more explicit user declarations for main dictionary; support non-permanent declarations;

Removed old experiment (broken since b458b4ac570f resp 4159caa18f85)

added divide_nonneg_nonneg and co; made it a simp rule

support for persistent user dictionaries;

tuned;

eliminated somewhat pointless locale parameter;

tuned;

clarified complete: participate in case-mangling of check;

tuned;

added spell-checker completion dialog, without counting frequency of items due to empty name; tuned signature;

tuned signature;

special treatment for '' ligature in TeX, which counts as word separator

more elementary notion of "word" (similar to VoxSpell) -- treat hyphen as separator;

tuned rendering -- avoid overlap with squiggly underline;

added dictionaries_selector GUI; tuned;

tuned signature -- explicit Spell_Checker_Variable;

updated to jortho-1.0-1: dictionaries from SCOWL 7.1, with parameters like aspell; simplified dictionary file format; tuned signature;

clarified according to ML version;

merged

NEWS;

more spell_checker_elements; tuned color;

some case-mangling; clarified use of locale;

more general spell_checker_elements;

added spell-checker options; support for rendering bad words;

added bad_words; more explicit language and locale;

markup for prose words within formal comments;

added spell-checker based on jortho-1.0;

prefere standard Isabelle/Scala operation, with fixed locale;

more operations and lemmas

made mult_pos_pos a simp rule

bi_unique and co. rules from the BNF hook must be introduced after bi_unique op= and co. rules are introduced

merged

made divide_pos_pos a simp rule

fix the reflexivity prover

merged

observe also DEADID BNFs and associate the conjunction in rel_inject to the right

made ereal_add_nonneg_nonneg a simp rule

made mult_nonneg_nonneg a simp rule

merged

more formal dependencies via 'document_files';

explicit 'document_files' in session ROOT specifications; clarified Isabelle_System.copy_file(_base): preserve file-attributes and local directory hierarchy;

tuned message, to accommodate extra brackets produced by Scala parsers;

tuned;

removed obsolete doc_dump option (see also 892061142ba6);

restoring notion of primitive vs. derived operations in terms of generated code; established _paramatric suffix for parametricity rules

removed duplication and tuned

make list_all an abbreviation of pred_list - prevent duplication

add pred_inject for product and sum because these theorems are not generated automatically because prod and sum are not in FP sugar for bootstrapping reasons

simplify and fix theories thanks to 356a5efdb278

setup for Transfer and Lifting from BNF; tuned thm names

revert idiomatic handling of namings from 5a93b8f928a2 because in combination with Named_Target.theory_init global names are sometimes created

don't forget to init Interpretation and transfer theorems in the interpretation hook

export theorems

abstract Domainp in relator_domain rules => more natural statement of the rule

more appropriate name (Lifting.invariant -> eq_onp)

left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)

tuned

more accurate type arguments for intermeadiate typedefs

merged

ignore other_id reports for now (see 8eda56033203): massive amounts of redirections to 'class' etc. makes it difficult to edit main HOL; silently ignore excessive reports -- no ambition to detect that situation accurately;

more standard names;

modernized simproc_setup; modernized theory setup;

modernized theory setup;

added simproc markup, which also indicates legacy simprocs outside the name space;

modernized simproc_setup;

misc tuning;

more contributors;

tuned;

NEWS;

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;