diff -r c48becd96398 -r a7664ca9ffc5 src/HOL/TPTP/CASC/ReadMe
--- a/src/HOL/TPTP/CASC/ReadMe	Wed Dec 14 18:52:17 2016 +0100
+++ b/src/HOL/TPTP/CASC/ReadMe	Thu Dec 15 15:05:35 2016 +0100
@@ -1,4 +1,4 @@
-Notes from Geoff:
+Notes from Geoff Sutcliffe:
 
 I added a few lines to the top of bin/isabelle ...
 
@@ -48,10 +48,11 @@
 		STAREXEC_WALLCLOCK_LIMIT=300 ./bin/starexec_run_isabelle_hot $TPTP/Problems/CSR/CSR150^3.p
 		STAREXEC_WALLCLOCK_LIMIT=300 ./bin/starexec_run_isabelle_hot $TPTP/Problems/SYO/SYO304^5.p
 
-  The first problem is unprovable; the second one is proved by Satallax.
+  The first problem is unprovable; the second one is proved by Satallax (after
+  some delay).
 
-  All the tools accept CNF, FOF, TFF0, or THF0 problems and output SZS
-  statuses of the form
+  All the tools accept CNF, FOF, TFF0, TFF1, THF0, or THF1 problems and output
+  SZS statuses of the form
 
   	% SZS status XXX
 
@@ -60,43 +61,32 @@
     {Unknown, TimedOut, Unsatisfiable, Theorem, Satisfiable, CounterSatisfiable}
 
   Nitpick also output a model within "% SZS begin" and "% SZS end" tags, in
-  its idiosyncratic syntax.
-
-  In 2011, there were some problems with Java (needed for Nitpick), because it
-  required so much memory at startup. I doubt there will be any problems this
-  year, because Isabelle now includes its own version of Java, but the solution
-  back then was to replace
-
-  	exec isabelle java
-
-  in the last line of the "contrib/kodkodi-1.5.2/bin/kodkodi" script with
-
-  	/usr/lib64/jvm/java-1.5.0-gcj-4.5-1.5.0.0/jre/bin/java
-
-  See the emails we exchanged on 18 July 2011, with the subject "No problem on
-  my Linux 64-bit".
+  its idiosyncratic syntax. For TFF0 and THF0, phantom type arguments are not
+  supported, and type quantifiers are only allowed at the outermost position
+  in a formula, as "forall".
 
   Enjoy!
 
 
 Notes to myself:
 
-  I downloaded the official Isabelle2015 Linux package from
+  I downloaded the official Isabelle2016-1 Linux package from
 
-    http://isabelle.in.tum.de/dist/Isabelle2015_linux.tar.gz
+    http://isabelle.in.tum.de/dist/Isabelle2016-1_linux.tar.gz
 
-  on "macbroy21" and renamed the directory "Isabelle2015-CASC". I modified
+  on "macbroy21" and renamed the directory "Isabelle2016-1-CASC". I modified
 
-    src/HOL/TPTP/atp_problem_import.ML
+    src/HOL/TPTP
 
   to include changes backported from the development version of Isabelle. I
-  then built a "HOL-TPTP" image:
+  also modified "bin/isabelle" as suggested by Geoff above. I then built a
+  "HOL-TPTP" image:
 
     ./bin/isabelle build -b HOL-TPTP
 
-  I copied the heaps over to "./heaps":
+  I moved the heaps over to "./heaps":
 
-    mv ~/.isabelle/Isabelle2015/heaps .
+    mv ~/.isabelle/Isabelle2016-1/heaps .
 
   I created some wrapper scripts in "./bin":
 
@@ -117,7 +107,7 @@
       http://page.mi.fu-berlin.de/cbenzmueller/leo/leo2_v1.6.2.tgz
 
     I did "make opt". I copied "bin/leo.opt" to
-    "~/Isabelle2015-CASC/contrib/leo".
+    "~/Isabelle2016-1-CASC/contrib/leo".
 
     I added this line to "etc/settings":
 
@@ -141,19 +131,19 @@
 
       SATALLAX_HOME=$ISABELLE_HOME/contrib
 
-  Vampire (2.6):
+  Vampire 4.0 (commit 2fedff6)
 
-    I copied the file "vampire", which I probably got from the 2013 CASC
-    archive and moved it to "~/Isabelle2013-CASC/contrib/vampire".
+    I copied the file "vampire", which I got from Giles Reger on 23 September
+    2015.
 
     I added these lines to "etc/settings":
 
       VAMPIRE_HOME=$ISABELLE_HOME/contrib
-      VAMPIRE_VERSION=3.0
+      VAMPIRE_VERSION=4.0
 
   Z3 TPTP (4.3.2.0 postrelease):
 
-    I cloned out the git repository:
+    For Isabelle2015, I cloned out the git repository:
 
       git clone https://git01.codeplex.com/z3
 
@@ -173,9 +163,11 @@
   "/tmp/T.thy" with the following content:
 
     theory T imports Main begin
+
     lemma "a = b ==> [b] = [a]"
-    sledgehammer [cvc4 e leo2 satallax spass vampire z3 z3_tptp] ()
-    oops
+      sledgehammer [cvc4 e leo2 satallax spass vampire z3 (*z3_tptp*)] ()
+      oops
+
     end
 
   Then I ran
@@ -196,4 +188,4 @@
 
 
                 Jasmin Blanchette
-                10 June 2015
+                15 December 2016