proper transfer for Thm.derivation_name;

tuned OS names;

standard tests for macOS 10.15 Catalina;

updated NEWS w.r.t. e0237f2eb49d

more frugal simp rules for bit operations; more pervasive use of bit selector

more scalable output of YXML files;

proper grounding of free types produced by reconstruct_proof/infer_type, e.g. relevant for Lattices_Big.semilattice_set.infinite;

tuned;

tuned whitespace;

more thorough strip_shyps for proof boxes (but types are usually stripped and reconstructed later);

clarified;

tuned signature;

tuned signature;

tuned signature;

tuned;

copy jEdit sources instead of jar, for better browsing experience;

proper option;

tuned;

formally depend on Java 11 --- discontinue Java 8 workaround;

support Java/VM monitoring via jconsole;

escape some special chars, notably for URL#NAME form;

library theory for extractions of equations x = t into premises

tuned

rebuild x86_64-linux on Ubuntu 14.04.6 LTS; rebuild x86_64-cygwin on cygwin-20200116;

merged

include actions for jEdit dockables, e.g. "vfs.browser";

misc tuning and clarification;

infrastructure for extraction of equations x = t from premises beneath meta-all

avoid conflict with isabelle.next-error, resulting in odd startup dialog;

updated for release;

Added tag Isabelle2020-RC1 for changeset a8849ac415cc

follow Phabricator update 2020 Week 6;

tuned signature;

VSCode extension for official Isabelle release;

more documentation;

tuned GUI;

clarified command line;

proper navigation wrt. caret; tuned signature;

clarified modifier: avoid confusion of CS+a as C+a;

tuned -- avoid deprecated operations;

more Isabelle/jEdit actions;

updated for release;

more Isabelle/jEdit actions;

tuned signature;

tuned;

tuned lift_bnf's user interface for quotients

NEWS;

updated to polyml-5.8.1-20200228 test version (Poly/ML 6025c250b4f1);

tuned;

more complete signature;

more complete signature;

clarified versions -- more reproducible build;

removed dead lemma

simplified proofs

updated for release;

updated for release;

merged

updated for release;

updated version;

obsolete;

less ambitious preview: discontinued preview-update / preview-source which did not work on the spot via WebviewPanel;

misc tuning and clarification;

obsolete;

proper message passing -- discontinued obsolete auxiliary commands;

clarified Panel; discontinued intermediate Content_Provider;

removed duplicate (amending 5763d9a2f47d, 5aa9cb83e70e);

update to WebviewPanel API, following initial version by Peter Zeller;

Moved a number of general-purpose lemmas into HOL

more robust shutdown while Isabelle_Process is starting up, e.g. quit after dialog Isabelle version for testing";

merged

lift BNF witnesses for quotients (unless better ones are specified by the user)

more robust (amending add9a9f6a290): proper syntax error instead of exception for grammar with unreachable nonterminals, e.g. nonterminal f1 syntax "_F" :: "f1 ⇒ 'b" ("F _" 10);

merged

tuned var names (avoid h)

more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;

a few new lemmas

tuned deletion

merged

additional lemmas about alw and suntil (by Michael Foster)

proper print mode for function_space notation (amending d68b705719ce);

proper file name (amending ce3409dfb18c);

merged

tuned proof

more robust pretty printing of broken YXML, e.g. single "\^E";

merged

proper sort constraints for strip_shyps, for sort relations used in minimization;

merged

a few new lemmas

tuned;

merged

lemmas about "card A = 2"; prefer iff to implications

NEWS;

proper sort constraints for strip_shyps, which implicitly performs type instantiation; include solve_constraints in strip_shyps to avoid later conflicts with Thm.transfer;

NEWS;

Added tag Isabelle2020-RC0 for changeset 21c0b3a9d2f8

added lemmas

canonical approach towards lifting

more instances

tuned proof

afford newer Mercurial version, just before odd problems in 4.0 and 4.1;

afford more logging (following defaults on Ubuntu);

updated for release;

tuned;

updated for release;

some lemmas about the lex ordering on lists, etc.

proper symbols;

NEWS;

recover from Unicode accident in 4abd07cd034f;

updated for release;

NEWS;

NEWS;

tuned;

tuned;

easy abstraction over pointwise bit operations

more rules for natural deduction from inequalities

rule concerning bit (push_bit ...)

more lemmas

allow to override repository versions at runtime;

follow Phabricator update 2020 Week 5;

simplified logical constructions