From a47465bdbbb8d59d2bae92e94754fbbdb53cc829 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 4 Oct 2016 10:24:15 +0200
Subject: [PATCH] Links in ProofMode.md.

---
 ProofMode.md | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/ProofMode.md b/ProofMode.md
index 34ca2dd1e..5bb0a5440 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -3,10 +3,10 @@ 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.
+classes in the file [proofmode/classes](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