merged

Tidied up more ancient, horrible proofs. Liberalised frac_le

clarified signature: more uniform ML vs. Scala;

clarified names;

clarified names;

proper use of flag;

clarified signature;

tuned names;

finally expose interrupt, similar to ML;

Standard_Thread for isabelle command-line tools;

tuned -- Command_Line.tool is already part of Isabelle_Tool;

clarified signature;

clarified signature;

thread pool with Standard_Thread workers; tuned signature;

clarified signature;

support for uninterruptible execution;

tuned -- prefer Config.T over Data;

proper "editor_tracing_messages=0" as in "isabelle dump";

tuned;

clarified build_options vs. job options;

more official handling of protocol messages, including export;

less redundant markup reports;

more accurate context position reports;

clarified signature;

clarified signature;

tuned;

clarified signature;

tuned signature;

proper treatment of startup errors, notably for Pure ROOT.ML;

proper treatment of protocol exceptions and prover termination: avoid session.stop while saving image;

merged

Added tag Isabelle2020-RC4 for changeset 1f3d9a9dd42a

more robust, notably wrt. interrupts;

merged

more NEWS;

clarified messages: indicate termination explicitly;

avoid vacous type variable, due to "potentially redundant" shyps in Thm.unconstrainT;

Added tag Isabelle2020-RC3 for changeset 7fe1a344404a

updated to current cygwin-20200323, after 3.1.4-1 from 19-Feb-2020;

avoid jdk-11.0.6+10: it shows problem "S8217731: Font rendering and glyph spacing changed from jdk-8 to jdk-11" https://bugs.openjdk.java.net/browse/JDK-8217731 even though the changelog claims to have resolved this;

clarified signature: more direct Isabelle_Process.EXIT;

proper arguments of protocol function;

merged

more robust: process stdout on Windows may contain CR;

clarified signature; more inlined protocol messages;

prefer system option: easier to make it default;

support multiple sessions, notably for "isabelle build -P -j2";

pretty formatting as in Isabelle/ML;

output prover messages;

clarified signature;

clarified signature: more robust;

proper parent base;

traditional print_mode for batch build;

proper support for "isabelle build -P Pure";

clarified signature: more robust bootstrap base;

proper startup for Pure: its use_prelude produces stdout before stderr protocol init;

proper context for loading Pure;

clarified signature of ML_Process vs. Isabelle_Process: proper support for "isabelle build -P -b";

close socket explicitly (idempotent);

more robust message_context and shutdown, e.g. after errors in protocol loop (see also 3f02bc5a5a03);

simplified code and proofs

automated proof

merged

cleaned proofs

clarified signature;

more accurate treatment of errors;

clarified modules: global quasi-scope for markers;

redunant simp rule

merged

more ugly old proofs

merged

tuned;

clarified modules;

clarified signature: more explicit type Protocol_Message.Marker;

tuned signature -- follow Scala;

tuned;

more explicit type Protocol_Message.Marker; tuned;

clarified protocol messages: explicitly use physical_writeln, always encode_lines;

tuned;

tuned whitespace;

more tidying up of old apply-proofs

merged

tuned;

tuned;

tuned;

eliminated pointless flag (see also 6533ceee4cd7);

tuned;

merged

structured a lot of ancient, horrible proofs

clarified Isabelle_Process phases;

clarified order: update syslog before handling exit;

tuned error message;

clarified signature: more robust startup_join;

merged

tuned;

misc tuning based on hints by IntelliJ IDEA;

clarified signature;

clarified signature;

clarified signature;

clarified signature;

tuned;

clarified signature: more accurate session_base_info.sessions_structure;

clarified signature;

added lemma

merged

updated to more modern style

updated to scala-2.12.11;

merged

put back Nat.le_diff_conv2 because AUTO2 doesn't work with Groups.le_diff_conv2

merged

new-style Greater lemmas

tidying up some horrible proofs

avoid jdk-11.0.6+10: it shows problem "S8217731: Font rendering and glyph spacing changed from jdk-8 to jdk-11" https://bugs.openjdk.java.net/browse/JDK-8217731 even though the changelog claims to have resolved this;

tuned;

merged;

more NEWS;

delete Isabelle distribution archive after use;

documentation for "isabelle build_docker";

updated for release;

tuned bib;

more documentation on view.antiAlias, not just NEWS;

more NEWS;

avoid premature crash due to missing session parents/imports;

avoid accidental update of base session sources (following documentation in "system" manual);

avoid duplicate stderr output in isabelle build -v, e.g. "Timing ..." (amending a829207b32a3);

prefer subpixel antialiasing by default: rendering of text is usually much faster, notably on Linux (see also 093ab1a99eb6 and f610115ca3d0);

slightly more explicit error, without going into the graph of proof futures;

more robust re-use of $ISABELLE_TMP_PREFIX (amending c1597167563e);

prefer strict qualification (default for 'interpretation', see 461ee3e49ad3) as proposed by Pedro Sánchez Terraf;

tuned documentation, based on hints by Pedro Sánchez Terraf;

backed out changeset 7eadccd4392c: too confusing wrt. text overview panel;

back to old-style names for uniform sorting of build_status (amending 138e8226961e);

support actual_host for lrzcloud2: the proxy_host/sshd cannot resolve invented hostname (amending 1d8b6c2253e6);

clarified connection parameters (again, after adjusting $HOME/.ssh configuration);

clarified output;

proper host for ssh.hg_url (required aliasing works via $HOME/.ssh/config);

clarified connection parameters;

clarified test;

remove Thm.transfer workaround made obsplete by cf2406e654cf

back to post-release mode;

Added tag Isabelle2020-RC2 for changeset 7eadccd4392c

claried error elements: include internalized errors of tokens/commands;

more robust connection via proxy_host;

more robust: proper transfer if Context.eq_thy_id;

merged

tuned;

tuned;

more robust hg_url; clarified signature;

proper usage (amending 8c7706b053c7);

proper escape for literal single quotes;

some uses of "' " as witness for this feature;

allow slightly odd "' " in mixfix as documented (introduced in 55754d6d399c, but broken in be8a8d60d962);

tidied up a few little proofs

updated for release;

more usable defaults for high resolution on Linux, where the desktop environment usually lacks automatic scaling;

tuned for Isabelle2020;

more explicit defaults;

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

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;