added missing colon

clarified signature;

clarified signature;

more direct support for "command_span" markup property "is_begin";

clarified signature;

misc tuning and clarification;

clarified signature;

clarified code setup

moved / rearranged lemma

eliminate code drop: declarations where none needed

internal setting to identify pointless code drop: declarations

clarified colors, following d6a14ed060fb;

more comments;

tuned;

tuned;

back to more basic defaults, independently on the accidental L&F: e.g. relevant for editor_style=false, and session_graph.pdf;

proper default colors (amending e840461d5370): e.g. relevant for session_graph.pdf;

eliminate odd Unicode characters (amending e9f3b94eb6a0, b69e4da2604b, 8f0b2daa7eaa, 8d1e295aab70);

clarified natural decl_ord vs. slightly odd merge_decl_ord, following the historic status-quo of 53e56e6a67c3, which originally stems from c06d01f75764;

clarified merge order: accurately reproduce the stable status-quo from 53e56e6a67c3 --- e.g. relevant for smt proof reconstruction in (line 6705 of "$AFP/Modular_arithmetic_LLL_and_HNF_algorithms/HNF_Mod_Det_Soundness.thy") of AFP/f1299d4f896c;

clarified decl_ord wrt. kind_ord;

more diagnostic operations;

more robust treatment of impossible case;

clarified name and status of auxiliary operation

moved lemma

added lemma

merged

Complex analysis lemmas

merged

merged

more robust, for typical error message prefix/suffix;

tuned messages;

NEWS;

clarified signature: more uniform;

clarified messages;

more accurate warning;

clarified signature;

tuned (see also 9e7d1c139569);

tuned;

clarified signature;

tuned;

explicit "dest" rules: no longer declare [elim_format, elim];

more accurate declarations;

avoid redundant argument (amending af6f55b15749);

tuned;

clarified output;

tuned;

added lemmas

A few more lemmas

A number of basic and unaccountably missing lemmas about complex exponentiation

Lemmas about integrals and vector-valued functions

always use proper context when parsing constants

tuned

merged

proper thm ord that conforms to Thm.eq_thm_prop (amending f5fd9b41188a): relevant for declarations in a locale contex with assumptions, e.g. "locale test = assumes True begin declare refl [rule del] end";

clarified declaration equivalence --- follow original classical.ML, before 8aa1c98b948b;

tuned source structure;

tuned comments: more formal sections;

proper "plain" rule for extra_netpair (amending 8aa1c98b948b): need to avoid flat_rule / Object_Logic.atomize_prems for the sake of "standard" Isar proof, e.g. (line 34 of "$AFP/AWN/Qmsg_Lifting.thy);

more robust: no failure on bad rule;

tuned;

more accurate delete operation via authentic index --- minor performance tuning;

minor performance tuning;

clarified signature: do not expose internal data structures;

clarified signature;

clarified signature: prefer canonical order (latest declarations first);

clarified print order: follow original classical.ML, before 8aa1c98b948b;

maintain collective rule declarations via type Bires.decls, with netpair operations derived from it;

tuned: order does not matter here;

clarified modules;

clarified signature: rule declarations work via "info" as internal rule (which coincides with external rule);

more accurate "next" counter for each insert operation: subtle change of semantics wrt. Item_Net.length, due to delete operation; avoid costly Item_Net.length, which is linear in size;

tuned proof;

clarified modules;

redundant: Net.DELETE already handled;

tuned;

clarified signature: more explicit types, notably (thm option) instead of (thm list);

more robust: unique result expected, otherwise index calculations will go wrong;

tuned;

tuned;

clarified signature: anticipate use in src/Provers/classical.ML;

clarified signature;

tuned source structure;

efficient rule declarations in canonical order, for update of netpairs and print operation;

added option `-S` to Mirabelle to specify the subgoal classes to consider

moved to more appropriate theory

more correct lemma name

merged

added basic support for persistent prover data to Sledgehammer

merged

tuned comments;

tuned messages;

clarified signature: more explicit type Bires.kind;

tuned;

tuned;

tuned signature;

proper weight, instead of magic number 1000000 (see b3f190995bc9);

just one type Bires.netpair, based on Bires.tag with explicit weight; more general order_list operations;

misc tuning and clarification;

tuned signature: do not expose private operation;

minor performance tuning;

clarified modules; more direct operations for sort/filter;

clarified signature;

tuned signature: more explicit types;

clarified modules: explicit structure Bires;

minor performance tuning;

Two lemmas and a comment

removed duplicate lemma; added the notion of the kernel of a function

isabelle regenerate_cooper

NEWS;

obsolete (see 09904d5ef1f0);

inline errors as "bad" markup; reload_theory: proper node2;

more robust result of migrate_file: retain full src_path (in contrast to d5d0e36eda16);

clarified signature: more explicit operations;

more robust: avoid crash on session database errors;

tuned signature: more operations;

basic support to reload theory markup from session store;

tuned;

tuned;

tuned;

clarified signature;

eliminate odd workaround from Aug-2012 (see 393a37003851);

tuned;

clarified signature;

tuned signature;

clarified signature: avoid Session with accidental Resources.bootstrap, which is mostly undefined;

clarified signature: prefer private operation (see also 803731b62180);

tuned (see also 5c7652e9bc01);

tuned signature: more generic operations;

clarified signature;

clarified signature: omit pointless object-oriented indirection;

clarified signature; clarified modules;

tuned: avoid overlapping scopes;

tuned;

typo

append (rather than prepend) code equations: the order within a theory is maintained in the resulting code

scope pending code equations to theories

merged

tuned

enforce rebuild of Isabelle/ML;

proper build_context.store, instead of circular null value (amending 0e36478a1b6a and e891ff63e6db);

merged

more operations (e.g. for testing);

tuned;

tuned signature: more explicit operations;

more accurate ML_Settings from underlying Session;

more accurate ML_Settings from underlying Session;

tuned signature;

clarified signature;

more robust session startup, notably Isabelle/jEdit with session build (amending 0e36478a1b6a);

clarified signature: more accurate ML_Settings;

clarified modules;

clarified signature: avoid duplicate ML_Settings.system;

clarified signature: general Session.open_session_context;

tuned;

tuned;

tuned;

clarified modules;

more uniform options for session build/start (coincides with PIDE.options.value initially);

clarified signature: Session always provides Store (with Rich_Text.Cache);

clarified signature: prefer implicit PIDE.options, which correspond to PIDE.session;

clarified modules;

tuned signature;

clarified signature;

tuned;

clarified signature: more explicit subtypes of Session, with corresponding subtypes of Resources;

re-use cache from Main_Plugin.start;

clarified signature, following c3793899b880;

more robust: assertion holds, because session.finished_theories provides Snapshot from Document.State.end_theory;

clarified signature;

clarified signature;

tuned comments;

tuned;

added lemmas

added lemmas

treat map_filter similar to list_all, list_ex, list_ex1

reinstated intersection of lists as inter_list_set

merged

defined mset in terms of its list-versin count_list instead of the ugly length of filter.

more explicit theorem names for list quantifiers

support for explicit ML platform identifier;

more robust;

proper SSH operation (amending 956ecf2c07a0);

more robust;

tuned errors;

merged

tuned message;

more NEWS;

clarified signature;

more flexible ML_Settings in Isabelle/Scala, depending on system options and some default settings; update polyml-5.9.1-1: only settings;

support dynamic usage_text, after some options have been processed already;

clarified signature: more modular, avoid adhoc mixins;

tuned signature: more operations;

clarified signature: more explicit types;

proper support for old versions before 0e41f26a0250;

tuned whitespace;

proper Java command-line for desktop application (amending a3e7732b0393);

more robust: inspect true ML environment instead of reconstructing it externally;

clarified signature;

discontinue unused parameter (better done as system option);

discontinued ML_IDENTIFIER settings variable;

clarified modules;

tuned;

clarified signature;

removed pointless leftovers

more minus_list lemmas (incl code via fold instead of foldr)

make canonical homomorphism [simp]

the canonical homomorphism should be [simp]

merged

added minus functions on lists

more robust GUI setup via Java, instead of shell script; support for automatic / approximative GDK_SCALE for Linux;

merged

clarified modules;

avoid legacy infixes;

discontinue old infixes;

eliminated transitional lemma

tuned whitespace

reorganized more code-only operations

more qualified auxiliary operations

Sylvestre's correction to ex_least_nat_le and other tidying

New lemmas for floor/ceiling/round, plus tidying

prefer already existing operation to calculate minimum

some more lemmas

tuned syntax

latex error

HOL: minor additions regarding linear algebra

HOL-Combinatorics: more lemmas about permutations

merged

tuned;

obsolete (see 22d65e375c01);

more generic parsing of command spans; support for Thy_Info.get_theories_elements;

tuned;

support for Thy_Info.get_theories_segments, depending on system option "record_theories";

tuned;

another default code_unfold rule

generic executable ranges

clarified signature;

explicit abort for big lattice operations over non-empty sets

prefer explicit operation to make generated code more abstract

tuned theory structure

qualify can_select auxiliary operations

tuned

added lemma

annotate auxiliary operations explicitly

more correct language

more modern qualification of auxiliary operations

move legacy simplifier interfaces into separate file

added lemmas

tuned

merged

merged

update jedit component;

clarified colors for "dark" theme -- requires to update jedit component;

suppress other icon themes: always use default "tango" (which includes "idea-icons") -- requires to update jedit component;

clarified patches: this is hardly modular anymore;

redundant;