# HG changeset patch # User wenzelm # Date 1554216956 -7200 # Node ID 7ba769344550840aa489619e3f5c0226949bcdcd # Parent 042ae6ca2c408d83aeaf4fea794b548292176f9f# Parent 30863adababaeb1f4d3af9e3cb6c5a51725ad413 merged diff -r 042ae6ca2c40 -r 7ba769344550 .hgtags --- a/.hgtags Tue Apr 02 15:23:12 2019 +0100 +++ b/.hgtags Tue Apr 02 16:55:56 2019 +0200 @@ -35,3 +35,4 @@ 7aa3c52f27aade2cada22206cf0477b30a25f781 Isabelle2016-1 64b47495676d5d6bdec02032a7a90fe6e1ff6c50 Isabelle2017 91162dd89571fb9ddfa36844fdb1a16aea13adcf Isabelle2018 +6f2ab7f150f6bb27d9e59229035324ce1f94e4ac Isabelle2019-RC0 diff -r 042ae6ca2c40 -r 7ba769344550 ANNOUNCE --- a/ANNOUNCE Tue Apr 02 15:23:12 2019 +0100 +++ b/ANNOUNCE Tue Apr 02 16:55:56 2019 +0200 @@ -1,37 +1,37 @@ Subject: Announcing Isabelle2018 To: isabelle-users@cl.cam.ac.uk -Isabelle2018 is now available. +Isabelle2019 is now available. -This version introduces many changes over Isabelle2017: see the NEWS +This version introduces many changes over Isabelle2018: see the NEWS file for further details. Here are some notable points: -* Improved infix notation within terms. +* Improved "Isabelle DejaVu" font collection, suitable for text and GUI. -* Improved syntax for formal comments, within terms and other languages. +* Various Isabelle/jEdit improvements, with virtual file-system access to +sessions and exports. -* Improved management of ROOT files and session-qualified theories. +* Improved headless PIDE session (and server). -* Various improvements of document preparation. - -* Many Isabelle/jEdit improvements, including semantic IDE for BibTeX. +* HOL: 'export_code' now generates logical files in the theory and session +context, e.g. browsable as "isabelle-export:" in Isabelle/jEdit. -* Numerous HOL library improvements, including HOL-Algebra. +* HOL: various syntax and library improvements. -* Substantial additions to HOL-Analysis. +* HOL-Analysis: more material and better organization. -* HOL-Library.Code_Lazy: code generation for lazy evaluation. +* Isabelle/ML environments for separate SML applications. -* HOL-Real_Asymp: tools for semi-automatic real asymptotics. +* Isabelle/Haskell library for implementation of Isabelle/PIDE backends. -* Isabelle server for reactive communication with other programs. +* Installation management for Haskell (Stack) and OCaml (OPAM). -* More uniform 64-bit platform support: smaller Isabelle application. +* Update to current Java 11 and Poly/ML 5.8 with better scalability. -You may get Isabelle2018 from the following mirror sites: +You may get Isabelle2019 from the following mirror sites: Cambridge (UK) https://www.cl.cam.ac.uk/research/hvg/Isabelle Munich (Germany) https://isabelle.in.tum.de - Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle + Sydney (Australia) https://mirror.cse.unsw.edu.au/pub/isabelle Potsdam, NY (USA) https://mirror.clarkson.edu/isabelle diff -r 042ae6ca2c40 -r 7ba769344550 NEWS --- a/NEWS Tue Apr 02 15:23:12 2019 +0100 +++ b/NEWS Tue Apr 02 16:55:56 2019 +0200 @@ -9,8 +9,8 @@ *** General *** -* The font family "Isabelle DejaVu" is systematically derived from the -existing "DejaVu" collection, with variants "Sans Mono", "Sans", "Serif" +* The font collection "Isabelle DejaVu" is systematically derived from +the existing "DejaVu" fonts, with variants "Sans Mono", "Sans", "Serif" and styles "Normal", "Bold", "Italic/Oblique", "Bold-Italic/Oblique". The DejaVu base fonts are retricted to well-defined Unicode ranges and augmented by special Isabelle symbols, taken from the former @@ -78,9 +78,9 @@ storage directory for "isabelle build". Option "-n" is now clearly separated from option "-s". -* Update to OpenJDK 11, which is the current long-term support line -after Java 8. It provides a very different font renderer, with improved -sub-pixel font rendering. +* OpenJDK 11 has quite different font rendering, with better glyph +shapes and improved sub-pixel anti-aliasing. In some situations results +might be *worse* than Oracle Java 8, though. *** Document preparation *** @@ -210,6 +210,8 @@ * Session HOL-Number_Theory: More material on residue rings in Carmichael's function, primitive roots, more properties for "ord". +* Session HOL-Analysis: More material and better organization. + * Session HOL-SPARK: .prv files are no longer written to the file-system, but exported to the session database. Results may be retrieved via "isabelle build -e HOL-SPARK-Examples" on the @@ -282,7 +284,7 @@ *** System *** -* Update to Java 11: the current long-term support version of OpenJDK. +* Update to OpenJDK 11: the current long-term support version of Java. * Update to Poly/ML 5.8 allows to use the native x86_64 platform without the full overhead of 64-bit values everywhere. This special x86_64_32 diff -r 042ae6ca2c40 -r 7ba769344550 src/HOL/Analysis/Homotopy.thy --- a/src/HOL/Analysis/Homotopy.thy Tue Apr 02 15:23:12 2019 +0100 +++ b/src/HOL/Analysis/Homotopy.thy Tue Apr 02 16:55:56 2019 +0200 @@ -3815,9 +3815,9 @@ apply (rule_tac x=a in bexI) apply (rule_tac x=b in bexI) using homotopic_with_prod_topology [OF a b] - apply (metis (no_types, lifting) case_prod_Pair case_prod_beta' eq_id_iff) - apply auto - done + apply (metis (no_types, lifting) case_prod_Pair case_prod_beta' eq_id_iff) + apply auto + done qed with False show ?thesis by auto diff -r 042ae6ca2c40 -r 7ba769344550 src/Tools/jEdit/src/Isabelle.props --- a/src/Tools/jEdit/src/Isabelle.props Tue Apr 02 15:23:12 2019 +0100 +++ b/src/Tools/jEdit/src/Isabelle.props Tue Apr 02 16:55:56 2019 +0200 @@ -5,7 +5,7 @@ #identification plugin.isabelle.jedit.Plugin.name=Isabelle plugin.isabelle.jedit.Plugin.author=Johannes Hölzl, Lars Hupel, Fabian Immler, Markus Kaiser, Makarius Wenzel -plugin.isabelle.jedit.Plugin.version=10.0 +plugin.isabelle.jedit.Plugin.version=11.0 plugin.isabelle.jedit.Plugin.description=Isabelle Prover IDE #system parameters