--- a/ANNOUNCE Tue Jan 05 17:54:10 2016 +0100
+++ b/ANNOUNCE Tue Jan 05 17:54:21 2016 +0100
@@ -20,8 +20,7 @@
* HOL tool enhancements: Sledgehammer, Nitpick, Quickcheck, Transfer.
-* Many HOL library improvements, including advanced topological concepts and
-integration theory ported from HOL Light.
+* Many HOL library improvements, notably HOL-Multivariate_Analysis.
* Upgrade to Poly/ML 5.6 with debugger IDE support (Isabelle/ML and Standard
ML), per-thread profiling, native Windows version (32bit and 64bit).
--- a/CONTRIBUTORS Tue Jan 05 17:54:10 2016 +0100
+++ b/CONTRIBUTORS Tue Jan 05 17:54:21 2016 +0100
@@ -8,40 +8,37 @@
* Winter 2015: Manuel Eberl, TUM
The radius of convergence of power series and various summability tests.
- Harmonic numbers and the Euler–Mascheroni constant.
+ Harmonic numbers and the Euler-Mascheroni constant.
The Generalised Binomial Theorem.
- The complex and real Gamma/log-Gamma/Digamma/Polygamma functions and
- their most important properties.
+ The complex and real Gamma/log-Gamma/Digamma/Polygamma functions and their
+ most important properties.
* Autumn 2015: Florian Haftmann, TUM
- Rewrite definitions for global interpretations and sublocale
- declarations.
+ Rewrite definitions for global interpretations and sublocale declarations.
* Autumn 2015: Andreas Lochbihler
- Bourbaki-Witt fixpoint theorem for increasing functions on
- chain-complete partial orders.
+ Bourbaki-Witt fixpoint theorem for increasing functions on chain-complete
+ partial orders.
* Autumn 2015: Chaitanya Mangla, Lawrence C Paulson, and Manuel Eberl
A large number of additional binomial identities.
* Summer 2015: Daniel Matichuk, NICTA and Makarius Wenzel
- Isar subgoal command for proof structure within unstructured proof
- scripts.
+ Isar subgoal command for proof structure within unstructured proof scripts.
* Summer 2015: Florian Haftmann, TUM
Generic partial division in rings as inverse operation of multiplication.
* Summer 2015: Manuel Eberl and Florian Haftmann, TUM
- Type class hierarchy with common algebraic notions of integral
- (semi)domains like units, associated elements and normalization
- wrt. units.
+ Type class hierarchy with common algebraic notions of integral (semi)domains
+ like units, associated elements and normalization wrt. units.
* Summer 2015: Florian Haftmann, TUM
Fundamentals of abstract type class for factorial rings.
* Summer 2015: Julian Biendarra, TUM and Dmitriy Traytel, ETH Zurich
- Command to lift a BNF structure on the raw type to the abstract type
- for typedefs.
+ Command to lift a BNF structure on the raw type to the abstract type for
+ typedefs.
Contributions to Isabelle2015
--- a/NEWS Tue Jan 05 17:54:10 2016 +0100
+++ b/NEWS Tue Jan 05 17:54:21 2016 +0100
@@ -642,7 +642,8 @@
* Library/Old_Recdef: discontinued obsolete 'defer_recdef' command.
Minor INCOMPATIBILITY, use 'function' instead.
-* Library/Periodic_Fun: a locale that provides convenient lemmas for periodic functions
+* Library/Periodic_Fun: a locale that provides convenient lemmas for
+periodic functions.
* Multivariate_Analysis/Cauchy_Integral_Thm: Contour integrals (=
complex path integrals), Cauchy's integral theorem, winding numbers and
@@ -653,9 +654,10 @@
components, homotopic paths and the inside or outside of a set.
* Multivariate_Analysis: radius of convergence of power series and
- various summability tests; Harmonic numbers and the Euler–Mascheroni constant;
- the Generalised Binomial Theorem; the complex and real Gamma/log-Gamma/Digamma/
- Polygamma functions and their most important properties;
+various summability tests; Harmonic numbers and the Euler–Mascheroni
+constant; the Generalised Binomial Theorem; the complex and real
+Gamma/log-Gamma/Digamma/ Polygamma functions and their most important
+properties.
* Data_Structures: new and growing session of standard data structures.
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Jan 05 17:54:10 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Jan 05 17:54:21 2016 +0100
@@ -52,7 +52,7 @@
lemma swap_apply2: "Fun.swap x y f y = f x"
by (simp add: Fun.swap_def)
-lemma (in -) lessThan_empty_iff: "{..< n::nat} = {} \<longleftrightarrow> n = 0"
+lemma lessThan_empty_iff: "{..< n::nat} = {} \<longleftrightarrow> n = 0"
by auto
lemma Zero_notin_Suc: "0 \<notin> Suc ` A"
--- a/src/Tools/jEdit/src/jedit_editor.scala Tue Jan 05 17:54:10 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Tue Jan 05 17:54:21 2016 +0100
@@ -196,8 +196,10 @@
try { Doc.view(path) }
catch {
case exn: Throwable =>
- GUI.error_dialog(view,
- "Documentation error", GUI.scrollable_text(Exn.message(exn)))
+ GUI_Thread.later {
+ GUI.error_dialog(view,
+ "Documentation error", GUI.scrollable_text(Exn.message(exn)))
+ }
}
}
}
@@ -224,7 +226,9 @@
try { Isabelle_System.open(name) }
catch {
case exn: Throwable =>
- GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
+ GUI_Thread.later {
+ GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
+ }
}
}
override def toString: String = "URL " + quote(name)
--- a/src/Tools/jEdit/src/plugin.scala Tue Jan 05 17:54:10 2016 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Tue Jan 05 17:54:21 2016 +0100
@@ -146,7 +146,7 @@
/* current document content */
- def snapshot(view: View): Document.Snapshot =
+ def snapshot(view: View): Document.Snapshot = GUI_Thread.now
{
val buffer = view.getBuffer
document_model(buffer) match {
@@ -293,8 +293,10 @@
delay_load.invoke()
case Session.Shutdown =>
- PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
- delay_load.revoke()
+ GUI_Thread.later {
+ delay_load.revoke()
+ PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
+ }
case _ =>
}