merged
authorwenzelm
Tue, 02 Apr 2019 16:55:56 +0200
changeset 70218 7ba769344550
parent 70212 042ae6ca2c40 (current diff)
parent 70217 30863adababa (diff)
child 70219 5863d6a8374a
merged
--- 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
--- 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
--- 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
--- 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
--- 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