New lemmas about improper integrals and other things

prefer sign-agnostic conversion following bit structure

tuned for readability and got small performance improvement

bring some code equations into natural order

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