diff --git a/lib/Etanercept.thy b/lib/Etanercept.thy
index 2ebe26e89..4dfeda36a 100644
--- a/lib/Etanercept.thy
+++ b/lib/Etanercept.thy
@@ -23,7 +23,8 @@ text {*
   that exhaustively explores the state space of your proposition.
 
   Usage:
-    Run the "word_refute" command in a proof.
+    Run the "word_refute" command in a proof. The proof goal should involve only word
+    and boolean expressions.
   Options:
     These are config options which can be set using "declare" or "using".
     - word_refute_debug        enable verbose debugging output
@@ -39,8 +40,6 @@ text {*
      with GNU statement expressions, but I'm unsure if it's worth it.
    - We currently only support 8-, 16-, 32-, and 64-bit words. It would be straightforward to
      support other non-standard widths if required.
-   - Much of the pattern matching in this theory was generated by a script and is quite verbose. It
-     could probably be simplified.
 
   The tool is named after etanercept, an ill-advised treatment for primary progressive aphasia, a
   condition who's symptoms include an inability to find the right words for things. Amusingly the