From daba18d53f031f209638c7adf0935b6a7a4bcb8a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 1 Aug 2016 12:40:22 +0200
Subject: [PATCH] Remark that many proofmode tactics work with other
 connectives too.

---
 ProofMode.md | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/ProofMode.md b/ProofMode.md
index 9f14322c5..ed7f78881 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
 ------------------------------
 
-- 
GitLab