--- a/src/HOL/TPTP/CASC/SysDesc_Refute.html	Wed Dec 14 18:52:17 2016 +0100
+++ b/src/HOL/TPTP/CASC/SysDesc_Refute.html	Thu Dec 15 15:05:35 2016 +0100
@@ -1,12 +1,12 @@
 <HR><!------------------------------------------------------------------------>
-<H2>Refute 2015</H2>
+<H2>Refute 2016-1</H2>
 Jasmin C. Blanchette<sup>1</sup>, Tjark Weber<sup>2</sup><BR>
 <sup>1</sup>Technische Universit&auml;t M&uuml;nchen, Germany <BR>
 <sup>2</sup>Uppsala Universitet, Sweden <BR>
 
 <H3>Architecture</H3>
 
-Refute [<A HREF="#References">Web08</A>] is an open source counterexample 
+Refute [<A HREF="#References">Web08</A>] is an open source counterexample
 generator for Isabelle/HOL [<A HREF="#References">NPW13</A>] based on a
 SAT solver, and Nitpick's [<A HREF="#References">BN10</A>] precursor.