added useful library function

tuned

moved useful library functions upstream

merge

added fixme

more (co)datatype documentation

use nat_of_integer for term reconstruction instead of abstract constructor to allow reconstructed terms being fed back to the code generator

got rid of the dependency of Lifting_* on the function package; use the original rel constants for basic BNFs;

more work on (co)datatype docs

more symbolic notation;

Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);

merged

discontinued special treatment of \<^isub> and \<^isup> in rendering or editor front-end; document antiquotations: renamed term style "isub" to "sub";

merged

more general window_geometry;

added rail diagram

merged

disable old identifier syntax by default, legacy_isub_isup := true may be used temporarily as fall-back;

standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;

imported patch added_e_1_8

remove unnecessary dependencies on Library/Quotient_*

move Lifting/Transfer relevant parts of Library/Quotient_* to Main

introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local

move useful lemmas to Main

merged

indicate error-functions more prominently (by name prefix instead of suffix);

avoid low-level Same structure;

avoid misleading "instances" in function name;

move treatment of polymorphism to adhoc overloading command;

clarify function;

attempt to transfer focus back to main window after closing popups, which is potentially relevant for heavy-weight windows (cf. workaround in org/gjt/sp/jedit/gui/CompletionPopup.java);

imitate "noWordSep" of isabelle mode, e.g. relevant for word selection via double-click;

support somewhat standard "select all" by default;

more cleanup;

more explicit error, e.g. for sledgehammer query operation applied in non-HOL session;

tuned proofs;

added flag for jEdit/PIDE asynchronous mode

updated Vampire version numbers

Vampire 3.0 requires types to be declared -- make it happy (and get rid of "implicit" types since only Satallax seems to support them anymore)

whitepsace tuning

more robust parsing of Vampire proofs with "introduced" names

fixed "sorry"d proofs

repaired proofs (after change to xxx_case_def)

temporary sorry's for temporarily nonterminating (due to 2b430bbb5a1a) proofs

qualify intermediate typedefs

avoid double qualification for case constants

qualify more generated names with optional type name component

eliminated bogus assumption from theorem (that was instantiated with refl and resulted in flexflex pairs)

generalized library function

updated keywords;

merged

clarified Query_Operation.register: avoid hard-wired parallel policy; sledgehammer: more conventional parallel exception handling -- print just one interrupt;

moved generic module to its proper place;

manage hyperlinks via PIDE editor interface;

tuned whitespace;

prefer PIDE editor operations; apply_query: insist in non-outdated snapshot via editor.current_command; tuned signature;

central management of Document.Overlays, independent of Document_Model;

tuned -- use Multi_Map;

support for maps with multiple entries per key;

tuned signature;

tuned signature;

tuned signature;

tuned signature -- more abstract PIDE editor operations;

tuned messages

clarified option name (since case/fold/rec are also destructors)

define case constant from other 'free constructor' axioms

introduced case tactics

tuning

handle both TVars and TFrees -- necessary for 'wrap_free_constructors'

qualify map and rel names

reverted ill-advised naming scheme of 5a77edcdbe54

made (hopefully temporary) hack more robust

added warning

gracefully handle one more error condition

gracefully fail to define polymorphic (co)datatypes in local context

made code more robust

avoid DUP exception in local context (cf. 062aa11e98e1)

honor user tfree names

prefer local facts over global ones

use local context for name space

explicit "strict" flag for print functions (flipped internal meaning); non-strict query operations may operate on failed states;

avoid unnecessary case distinction

adjust tooltip for duplicates option

merged

NEWS;

Find is docked on startup;

sorted lines;

tuned GUI;

retain current task priority, to avoid distortion due to local forks (e.g. sledgehammer query operation);

removed "Locate" button, to avoid confusion about the slightly odd meaning of current_command with explicit theory context;

enable search in pre-loaded theory;

more GUI options;

tuned signature;

tuned;

tuned GUI;

tuned name generation code (to make it easier to adapt later)

honor user type names if possible

merged;

more abstract consume_status operation;

separate Process_Indicator -- simplified/clarified version of org.gjt.sp.jedit.gui.AnimatedIcon;

more active "provers" field, which increases chances that its history is stored;

removed command location is considered finished, and its overlay removed eventually; apply_query: empty output;

cancel_query via direct access to the exec_id of the running query process;

retain original messages properties, e.g. for retrieval via Command.Results;

clarified toplevel_error: absorb and print interrupts; tuned;

more explicit error;

tuned message;

removed unused YXML_Find_Theorems and Legacy_XML_Syntax;

more robust read_query; avoid pointless position, which is always line 1 for single-line input;

removed commented out declaration

tuned

merged

eliminate \<twosuperior> as well;

more strict identifier syntax: disallow superscripts, which tend to be used in notation such as \<^sup>\<omega>;

prefer plain subscript for identifiers;

proper low-level comparison -- heed warning by Scala compiler;

merged

prefer Code.abort with explicit error message

avoid re-inventing transitive closure

merged