src/HOL/TPTP/CASC/SysDesc_Isabelle.html

 <HR><!------------------------------------------------------------------------>
-<H2>Isabelle/HOL 2013</H2>
+<H2>Isabelle/HOL 2015</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>
 <sup>2</sup>University of Cambridge, United Kingdom <BR>
 <sup>3</sup>Universit&eacute; Paris Sud, France <BR>
 
 <H3>Architecture</H3>
 
-Isabelle/HOL 2013 [<A HREF="#References">NPW13</A>] is the higher-order 
+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/">Isabelle2013</A>.
+<A HREF="http://www.cl.cam.ac.uk/research/hvg/Isabelle/">Isabelle2015</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
 HREF="#References">Pau99</A>]. It also integrates external first- and
 higher-order provers via its subsystem Sledgehammer [<A

     <A HREF="http:////www.cl.cam.ac.uk/research/hvg/Isabelle/">http://www.cl.cam.ac.uk/research/hvg/Isabelle</A></PRE>
 
 <H3>Expected Competition Performance</H3>
 
 <P>
-Isabelle won last year by a thin margin. This year: first or second place.
+Thanks to the addition of CVC4 and a new version of Vampire,
+Isabelle might have become now strong enough to take on Satallax
+and its various declensions. But we expect Isabelle to end in
+second or third place, to be honest.
 
 <H3>References</H3>
 <DL>
 
 <DT> BBP11