proper state_panel exit;

Some facts about orders of zeros

Winding numbers for rectangular paths

misc tuning and modernization;

auto update;

prefer https for the sake of "npm run vscode:prepublish";

tuned;

fundamental_theorem_of_calculus_interior: more cleanup

more cleanup of fundamental_theorem_of_calculus_interior

added lemmas

merged

more cleanup of fundamental_theorem_of_calculus_interior

partly unravelled fundamental_theorem_of_calculus_interior

more unknotting

merged

misc tuning and modernization;

maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);

clarified signature;

tuned;

Merged

Merged

Merged

Removed unnecessary constant 'ball' from Formal_Power_Series

merged;

more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;

more synchronized Execution.snapshot;

tuned spelling;

tuned;

tuned;

merged

more Henstock_Kurzweil_Integration cleanup

tuning imports

use TFF0 with E 2.0 and above

E 2.0 component

updated remote Vampire version

merged

more integration cleanups

slightly generalized card_lists_distinct_length_eq; renamed specialized card_lists_distinct_length_eq to card_lists_distinct_length_eq'; tuned

merged

further cleanup of "guess"

towards a cleanup of Henstock_Kurzweil_Integration.thy

merged

proper check for active server;

clarified signature;

tuned signature;

handle server connections;

clarified database names;

more options; misc tuning and clarification;

support for resident Isabelle servers;

default according to Java API, instead of jEdit usage;

do not fall back on nbe if plain evaluation fails

final tidying up of lemma bounded_variation_absolutely_integrable_interval

finally rid of finite_product_dependent

more cleanup

trying to disentangle bounded_variation_absolutely_integrable_interval

merged

more horrible proofs disentangled

tuned

more structural sharing between common target Generic_Target.init

exit always refers to the bottom of a nested local theory stack, after_close always to all non-bottom elements

treat exit separate from regular local theory operations

provide explicit variant initializers for regular named target vs. almost-named target

prefer explicit datatype over implicit sum; given up separate implementation to pretty-print locale specifications

compactified output

lifting setup for char

one single plugin for code type declarations avoids problems when bootstrapping new plugins over types which have been both declared concrete and abstract in their code historiy

uniform namespace handling for both concrete and abstract types, following 32e0da92c786

clarified

corrected slip

tuned

work around weakness in export calculation when generating OCaml code

tuned

pass option recommended by Andy Reynolds to CVC4 1.5 (released) or better

updated CVC4 component to official 1.5 release

merged

eliminated more "guess", etc.

merged

more tidying

more tidying up

merged

merged

removed all "guess"

tuned

merged

added lemmas

simplified function specification history: each pending function specification is historized at the end of a theory, without additional bookkeeping; sufficient to keep history stamps rather than complete historized data; semantically conflicting specifications are temoprary blacklisted after theory merge but remain historized; clarified signature;

merged

generalized lemma

tuned references

fixed another horrible proof

misc tuning and modernization;

isabelle update_cartouches -c -t;

misc tuning and modernization;

new lemma

more explicit Argo proof traces; more correct proof replay for term applications

more cleanup of Tagged_Division

partial cleanup of the horrible Tagged_Division

introduced option for nat-as-int in SMT

polytopes: simplical subdivisions, etc.

New theory of Equiintegrability / Continuity of the indefinite integral / improper integration

moved transitive_stepwise_le into Nat, where it belongs

refactored some HORRIBLE integration proofs

merged

improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann

tuned code setup

strengthened tactic

Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike

strengthened tactic (for 'fun' BNF)

new material: Colinearity, convex sets, polytopes

poles and residues of the Gamma function

merged

new derived targets for evaluating Haskell and Scala programs

Printing natural numbers as numerals in evaluation

fmap is finite

facts about cardinality of vector type

Adapted Approximation_Bounds to changes in Multiset

Simprocs for roots of numerals

Updated NEWS

HOL-Analysis: Infinite products

More material on powers for HOL-Computational_Algebra/HOL-Number_Theory

additional lemmas for State_Monad, courtesy of Andreas Lochbihler

more material on finite maps

redundant since c6714a9562ae

store the unfolded definitions of the lifted bnf constants under "_def" name

state monad

State_Monad ~> Open_State_Syntax

more material on fmaps

canonical representation for fmaps is fmlookup

fmaps are countable

merged

card_0_eq ~> fcard_0_eq

material from $AFP/Formula_Derivatives/FSet_More

FSet is monadic

finite sets are countable

lift sum to finite sets

tuned

clarified

dropped superfluous theory imports

revised lemma

merged

generalized lemma

proper check wrt. distinct entry dates;

added lemma

some generalizations complex=>real_normed_field

proper concept of code declaration wrt. atomicity and Isar declarations

merged

complete on long name components as well;

added command 'alias' and 'type_alias';

tuned;

tuned signature;

unused;

qualify Complete_Partial_Order2.compact

tuned;

proper fonts (cf. 1d219d76873b);

all_known can cause timeout of VSCode server startup, notably on Windows;

tuned documentation; updated package version; updated screenshot reference;

clarified screenshot;

NEWS;

tuned;

more documentation;

retain symlinks in file names from VSCode: relevant for proper file locations in decorations etc.;

clarified platform file operations;

more operations;

clarified signature;

more robust: always package;

prefer explicit link;

updated package;

provide --baseImagesUrl for VSCode extensions marketplace;

tuned;

updated package;

tuned;

added screenshot;

clarified;

updated package;

tuned;

tuned output;

tuned spelling;

more documentation;

auto update;

clarified editor focus;

proper hyperlink_command, notably for locate_query; support bidirectional caret update;

tuned signature;

proper dynamic controls, notably for auto_update_enabled;

tuned signature;

HTML GUI actions via JavaScript;

more operations/options;

clarified signature;

merged

support for HTTP/POST method; more explict type HTTP.Arg;

clarified defaults;

tuned signature;

auto update;

added missing files (cf. 5aa9cb83e70e);

auto update;

GUI controls similar to Tools/jEdit/src/state_dockable.scala;

GUI layout similar to Pure/GUI/wrap_panel.scala;

Removed more "guess", etc.

more error checking

merged

some HTML GUI elements;

proper bootstrap_name (amending b42743f5b595);

clarified indentation;

More tidying of horrible proofs

A few renamings and several tidied-up proofs

back to scala-2.12.2, after a41435469559;

more direct construction of integer_of_num; code equations for integer_of_char may rely on pattern matching on Char

treat "undefined" constants internally as special form of case combinators

Improved error reporting when activating a locale instance (beyond syntax decls).

Additional corollary Knaster_Tarski_idem_inf_eq.

clarified indentation;

clarified indentation;

merged

tuned signature;

tuned;

NEWS;

indentation of keywords after input;

indent = 0 for blank lines: produce less whitespace by default;

clarified prev_line: stop at blank line;

more information;

tuned signature;

tuned;

avoid trailing spaces;

clarified modules; tuned;

Merged

distrib_lattice instance for filters

merged

keep original bottom-up order of proof forks, which potentially reduces thread congestion due to Proofterm.consolidate;

consolidate proofs more simultaneously;

more informative task_statistics;

more informative task_statistics;

Merge

New theorems and much tidying up of the old ones

added 'solvers' option to Nunchaku

Contravariant map on filters

merged

tuned granularity of parallel tasks;

more completion;

clarified modules;

tuned signature;

added -d option to Mirabelle