diff --git a/ProofMode.md b/ProofMode.md
index 9f14322c5ad413bc73bdb32a14a429f8e12fe0a8..ed7f788813bfa06bec042d9bace9c9b1b2bc26cd 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -1,6 +1,13 @@
 Tactic overview
 ===============
 
+Many of the tactics below apply to more goals than described in this document
+since the behavior of these tactics can be tuned via instances of the type
+classes in the file `proofmode/classes`. Most notable, many of the tactics can
+be applied when the to be introduced or to be eliminated connective appears
+under a later, a primitive view shift, or in the conclusion of a weakest
+precondition connective.
+
 Applying hypotheses and lemmas
 ------------------------------