--- a/src/HOL/TPTP/CASC/SysDesc_Isabelle.html	Wed Dec 14 18:52:17 2016 +0100
+++ b/src/HOL/TPTP/CASC/SysDesc_Isabelle.html	Thu Dec 15 15:05:35 2016 +0100
@@ -1,5 +1,5 @@
 <HR><!------------------------------------------------------------------------>
-<H2>Isabelle/HOL 2015</H2>
+<H2>Isabelle/HOL 2016-1</H2>
 Jasmin C. Blanchette<sup>1</sup>, Lawrence C. Paulson<sup>2</sup>,
 Tobias Nipkow<sup>1</sup>, Makarius Wenzel<sup>3</sup> <BR>
 <sup>1</sup>Technische Universit&auml;t M&uuml;nchen, Germany <BR>
@@ -8,9 +8,9 @@
 
 <H3>Architecture</H3>
 
-Isabelle/HOL 2015 [<A HREF="#References">NPW13</A>] is the higher-order 
-logic incarnation of the generic proof assistant 
-<A HREF="http://www.cl.cam.ac.uk/research/hvg/Isabelle/">Isabelle2015</A>.
+Isabelle/HOL 2016-1 [<A HREF="#References">NPW13</A>] is the higher-order
+logic incarnation of the generic proof assistant
+<A HREF="http://www.cl.cam.ac.uk/research/hvg/Isabelle/">Isabelle2016-1</A>.
 Isabelle/HOL provides several automatic proof tactics, notably an equational
 reasoner [<A HREF="#References">Nip89</A>], a classical reasoner [<A
 HREF="#References">Pau94</A>], and a tableau prover [<A