tuned GUI;

tuned GUI;

proper tooltip (amending fd8a65b026f1);

updated to scala-2.12.3;

auto update;

updated to jdk-8u144;

tuned GUI;

more explicit failure;

explicit indication of consolidated nodes;

further tidying

general rationalisation of Analysis

merged

cleanup of integral_norm_bound_integral

be more explicit on type dlist

code generation for Gcd and Lcm when sets are implemented by red-black trees

merged

more Henstock_Kurzweil_Integration cleanup

merged

even more horrible proofs disentangled

merged

fmap :: size

avoid spurious output after exit;

updated package version;

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