From f73319e84af2003fc8cb1070198d8d4ab5d6ef08 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 5 Sep 2020 14:56:25 +0200
Subject: [PATCH] Add BI notation for negation.

---
 theories/bi/interface.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 52d8ed704..ba41b1898 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -244,6 +244,7 @@ Notation "(∧)" := bi_and (only parsing) : bi_scope.
 Infix "∨" := bi_or : bi_scope.
 Notation "(∨)" := bi_or (only parsing) : bi_scope.
 Infix "→" := bi_impl : bi_scope.
+Notation "¬ P" := (P → False)%I : bi_scope.
 Infix "∗" := bi_sep : bi_scope.
 Notation "(∗)" := bi_sep (only parsing) : bi_scope.
 Notation "P -∗ Q" := (bi_wand P Q) : bi_scope.
-- 
GitLab