From c34a49df5ffd3f3975ab3327817d448e638f03d3 Mon Sep 17 00:00:00 2001
From: Enrico
Date: Tue, 22 Jan 2019 10:25:32 +0100
Subject: Update CHANGES.md

---
 CHANGES.md | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/CHANGES.md b/CHANGES.md
index 3ef0043672..a1ef849d92 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -156,23 +156,23 @@ Misc
 SSReflect
 
 - New intro patterns:
-  - temporary introduction: => +
-  - block introduction: => [^ prefix ] [^~ suffix ]
-  - fast introduction: => >
-  - tactics as views: => /ltac:mytac
-  - replace hypothesis: => {}H
+  - temporary introduction: `=> +`
+  - block introduction: `=> [^ prefix ] [^~ suffix ]`
+  - fast introduction: `=> >`
+  - tactics as views: `=> /ltac:mytac`
+  - replace hypothesis: `=> {}H`
   See the reference manual for the actual documentation.
 
 - Clear discipline made consistent across the entire proof language.
-  Whenever a clear switch {x..} comes immediately before an existing proof
+  Whenever a clear switch `{x..}` comes immediately before an existing proof
   context entry (used as a view, as a rewrite rule or as name for a new
   context entry) then such entry is cleared too.
 
   E.g. The following sentences are elaborated as follows (when H is an existing
   proof context entry):
-  - "=> {x..} H"       ->  "=> {x..H} H"
-  - "=> {x..} /H"      ->  "=> /v {x..H}"
-  - "rewrite {x..} H"  ->  "rewrite E {x..H}"
+  - `=> {x..} H`       ->  `=> {x..H} H`
+  - `=> {x..} /H`      ->  `=> /v {x..H}`
+  - `rewrite {x..} H`  ->  `rewrite E {x..H}`
 
 Changes from 8.8.2 to 8.9+beta1
 ===============================
-- 
cgit v1.2.3