merged

more careful parsing of nested argument tokens -- avoid Parse.RESET_VALUE on still uninterpreted material;

proper exhaustive match (cf. e9beabf045ab);

proper context;

merged

renamed theory Mrec to Legacy_Mrec, no longer included by default

replaced use of obsolete MREC by partial_function (heap)

more document antiquotations (for proper theorem names);

moved derivation of strong coinduction to sugar

simpler (forward) derivation of strong (up-to equality) coinduction properties

don't derive unused low-level theorem

tuned example

doc tuning

adapted ML code to new version of MaSh tool

new version of MaSh tool -- experimental server

adapted to new MaSh syntax

tuning

merged

Inserted footnote under match_tac

learn MaSh facts on the fly

allow MaSh query to do some learning as well

tuning

merged

removed french option to manuals

treat frees as both consts and vars, for more hits

keep long names to stay on the safe side

tuned;

tuned signature;

MaSh tweaking: shorter names + killed (broken) SNoW

handle Bounds as well in MaSh features

add subtypes as well as features in MaSh

generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)

generate deep type patterns in MaSh

improved ad hoc success detection in Mirabelle -- if the metis call fails and the structured proof succeeds, remember only the success

tuned;

tuned proofs;

more static simpsets, which also avoids spurious warnings due to duplicate rules provided here;

more symbols;

more symbols;

merged

load_theories if continuous_checking;

discontinued redundant abbreviations -- Isabelle/jEdit provides keyboard shortcuts already;

prefer plain subscript;

tuned;

spelling and typos

execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs

relaxed preconditions

type class for generic division algorithm on numerals

added lemma

added lemma

generalized sort constraint of lemmas

explicit conversion from and to bool, and into algebraic structures with 0 and 1

some vague grouping of related theorems, with slight tuning of headings and sorting out of dubious lemmas into separate theory

more markup;

tuned;

updated identifier syntax;

Sledgehammer is docked on startup;

prefer system option sledgehammer_timeout, with standard GUI in jEdit Plugin Options;

more robust startup;

some protocol to determine provers according to ML;

public access for protocol handlers and protocol commands -- to be used within reason;

always enable "minimize" to simplify interaction model; override params more directly -- they are no longer echoed in minimize command;

sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel; back to Normal mode: with output_result it is sufficient to determine TTY vs. PIDE operation;

recovered Locale.intern from d51bac27d4a0 (still used in AFP/Simp);

NEWS;

eliminated pointless subgoal argument;

more direct sledgehammer configuration via mode = Normal_Result and output_result; retain standard sledgehammer parallelization policies;

more explicit sendback propertries based on mode;

tuned;

check_tool wrt. official ISABELLE_TOOLS; added Path.split (cf. Scala version);

more markup via Name_Space.check; tuned signature;

more standard attribute_setup / method_setup -- export key ML operations instead of parsers;

standardized aliases;

more markup -- avoid old Locale.extern; removed obsolete Locale.intern -- prefer Locale.check;

renamed function

eliminate quasi-duplicate function

generalized "mk_permute"

tuning

added more functions to BNF library

moved function to where it seems to belong

moved library function where it belongs, and used Dmitriy's inside-out implementation

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)