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

simplified logical constructions

more theorems

Simplified, generalised version of Constructible due to E. Gunther, M. Pagano and P. Sánchez Terraf

tuned

tuned

added Interval_Tree.thy

more specific class assumptions

more theorems

ignore generated dependency files (see 91d5a8255c98, fd5cd1daf6a9);

Tidied up some messy proofs

sketches of ideas still to come

more theorems

generalized

tuned

Two lemmas about nsets

A few lemmas connected with orderings

tuned

tuned

dropped dead code

merged

added lemma

Removed multiplicativity assumption from normalization_semidom

clarified file names;

clarified build_polyml_component: include IDE entry point for ML compiler;

merged

tuned spelling;

new examples of BNF lifting across quotients using a new theory of confluence, which simplifies the relator subdistributivity proof obligation (a few new useful notions were added to HOL; notably the symmetric and equivalence closures of a relation)

Removed unnecessary and problematic trivial lemma from HOL-Algebra

proper executable file;

more documentation: odd option for special situations;

tuned;

updated to sumatra_pdf-3.1.2-1: x86_64-windows;

updated to stack-2.1.3, stackage lts-13.19, ghc-8.6.4;

updated to opam-2.0.6;

updated to current cygwin, after 3.1.2-1 from 21-Dec-2019;

updated to jdk-11.0.6+10;

misc tuning, following hint by IntelliJ;

tuned;

tuned -- avoid deprecated constructors;

proper comparison of Option values, following hint by IntelliJ;

unused -- clone of Option.apply;

added "isabelle scala_project" to support e.g. IntelliJ IDEA;

unused;

more antiquotations;

tuned messages;

tuned;

clarified output channel;

clarified option -f: avoid accidental target_clean for proper release snapshot;

more robust;

updated to sqlite-jdbc-3.30.1;

updated to postgresql-42.2.9;

build in $ISABELLE_HOME; clarified build dependencies;

build in $ISABELLE_HOME; clarified build dependencies;

clarified fresh build;

tuned documentation;

tuned;

clarified script name;

prefer mercurial-2.8.2 for more robustness (i.e. the version used by the hosting service https://admin.phacility.com);

proper name;

more Isabelle fonts, notably for File Browser title in GTK L&F;

eliminated deprecated scala.collection.JavaConversions;

unused;

tuned -- more direct java.util.Map.of;

added lemma

merged

eliminated one redundant proof obligation in lift_bnf for quotients

removed experimental option to SPASS

alternative deletion in Red-Black trees

generalized thm (as suggested by Christian Weinz)

tunded

tuned

tuned

more examples;

tuned

tuned

tuned;

NEWS;

updated platform situation: 32bit variants are marginal or absent;

repackage as csdp-6.1-1, with proper platform names;

proper File.platform_path for Windows;

updated csdp-6.1: Linux and Windows executables are as before, but macOS has been rebuilt for x86_64 (to accommodate Catalina); NOTE: current version 6.2.0 caused odd problems with parallel invocations (e.g. on Ubuntu 18.04);

updated linux_app-20191223: x86_64-linux; clarified location of lib/scripts/Isabelle.run;

tuned;

improved Markdown-like display in Phabricator;

improved Markdown-like display in Phabricator;

somewhat irrelevant -- defaults are OK;

obsolete;

clarified signature -- more operations;

clarified signature;

proper search with multiple "pages" of results;

tuned documentation;

tuned messages;

more robust;

tuned message;

NEWS;

more documentation;

tuned documentation;

more documentation;

added option -r: support more robust consolidation of local clones with varying names;

clarified backup;

removed somewhat pointless option -R: more careful inspection of hgrc is required in practice;

proper proof body context for Simplifier plugins (solvers, loopers, ...) -- avoid crash due to Subgoal.FOCUS (before e58bc223f46c);

more robust bound_fixes: external name does appear in "fixes" name space and could clash with direct fixes (e.g. via Subgoal.FOCUS within a global context);

tuned signature;

proper backup;

clarified signature;

more ambitious edit_hgrc;

added command hg_setup: setup remote vs. local Mercurial repository;

clarified signature;

clarified signature;

tuned;

clarified signature; tuned;

tuned;

more repository information;

more permissive string fields;

tuned proof (by Thomas Sewell)

tuned;

clarified signature: error_code may contain low-level message instead of proper "ERR-" code;

clarified signature; more operations;

tuned signature;

support for conduit API;

tuned whitespace;

more robust: support /usr/local/bin/hg;

tuned documentation;

eliminated pointless option -T: it merely tests ssh config of root, which is not required later;

slicker proofs (used in CPP paper)

tuned NEWS;

more rebust setup for Subversion -- assuming that diffusion.ssh-port is only set in phabricator/conf/local/local.json, not in the database;

tuned;

tuned documentation;

more checks for release;

more packages: required for svn;

more robust setup: avoid blind shot at "the latest" version;

more documentation;

proper default;

more robust: avoid accidental use of stdin;

support for Phabricator upgrade;

tuned signature;

tuned message;

avoid odd (harmless) problem with Mercurial 4.5.3 provided by Ubuntu 18.04 on first push: "couldn't write revision branch cache names";

more documentation;

more documentation;

proper support for multiple installations;

clarified "isabelle phabricator -l": avoid surprise with non-existent default installation;

tuned index.html;

more robust;

more robust;

clarified website: redirect to isabelle-dev Phabricator Overview;

more documentation;

tuned;

support database dump;

proper check of Linux version;

tuned;

proper mysql user setup: avoid superuser powers in production; specific phabricator.cache-namespace, following standard cluster configuration by Phacility;

support for pwgen;

NEWS, CONTRIBUTORS, and documentation

an extensive example for lift_bnf across quotients

extension of lift_bnf to support quotient types

unfold intermediate (internal) pred definitions

corrected some confusing terminology / notation

Ramsey with multiple colours and arbitrary exponents

a few new and tidier proofs (mostly about finite sets)

clarified signature: store full theory name;

merged

moved lemmas

merged

suppress record types: not working properly;

removed junk;

discontinued somewhat pointless options;

tuned signature;

clarified signature;

export datatypes;

clarified modules;

misc tuning and clarification: proper check of datatype kind;

clarified modules;

cleaning

tuned

separated Affine theory from Convex

merged

tuned

proper table data structure

removed some vain declarations

merged

made Starlike independent of Abstract_Limits

more direct accessors for simpset

regular merge with no historization, in accordance with regular update

moved starlike where it belongs

merged

clarified messages streaming (again, amending 5ea3ed3c52b3): avoid too many small messages stacking up, e.g. when loading HOL-Analysis.Analysis.thy into Isabelle/jEdit;

moved segment lemmas where they belong

merged

moved lemmas

merged

two new theorems