From 260e0593a8887b1e985300444057db2c04386d25 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 22 Mar 2021 20:19:33 +0100
Subject: [PATCH] extend proof_mode.md
---
docs/proof_mode.md | 3 +++
1 file changed, 3 insertions(+)
diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index b383aed63..b1a84922b 100644
--- a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ -328,6 +328,9 @@ _introduction patterns_:
+ Either the proposition `P` or `Q` should be persistent.
+ Either `ipat1` or `ipat2` should be `_`, which results in one of the
conjuncts to be thrown away.
+- `[% ipat]` : existential elimination. Falls back to (separating) conjunction
+ elimination in case the hypothesis is not an existential, so this pattern also
+ works for (separating) conjunctions with a pure left-hand side.
- `(pat1 & pat2 & ... & patn)` : syntactic sugar for `[pat1 [pat2 .. patn ..]]`
to destruct nested (separating) conjunctions.
- `[ipat1|ipat2]` : disjunction elimination.
--
GitLab