From 456696acbd298872c9f6e9dd26791832ee0dc336 Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Wed, 19 Jul 2017 21:39:36 +0100
Subject: [PATCH] fixes to README and index

---
 README.md | 54 +++++++++++++++++++++++++++++-------------------------
 index.md  | 25 +++++++++++--------------
 2 files changed, 40 insertions(+), 39 deletions(-)

diff --git a/README.md b/README.md
index d1c20225..8b452fef 100644
--- a/README.md
+++ b/README.md
@@ -4,26 +4,22 @@ title: About
 permalink: /about/
 ---
 
-This is a rewrite of the text
+This is a rewrite of the text [Software Foundations](
+https://softwarefoundations.cis.upenn.edu/current/index.html
+)
+from Coq to Agda. The authors are 
+[Wen Kokke](
+https://github.com/wenkokke
+)
+and
+[Philip Wadler](
+http://homepages.inf.ed.ac.uk/wadler/
+).
 
-* [Software Foundations](
-  https://softwarefoundations.cis.upenn.edu/current/index.html
-  )
 
-from Coq to Agda. The authors are
+## How to host literate code
 
-* [Wen Kokke](
-  https://github.com/wenkokke
-  )
-* [Philip Wadler](
-  http://homepages.inf.ed.ac.uk/wadler/
-  )
-
-## Instructions
-
-_How to host literate code_
-
-In directory `sf/` the following:
+In directory `sf/` run the following:
 
 	$ make clobber
     $ make
@@ -33,19 +29,20 @@ The visible page appears at
 
     localhost:4000/sf/<permalink>
 
+## Markdown
+
 For markdown commands see [Daring Fireball](
 https://daringfireball.net/projects/markdown/syntax
 ).
 
-_Important git commands_
+## Important git commands
 
     git pull
     git commit -am "message"
     git push
 
-_[Unicode abbreviations](
-https://github.com/agda/agda/blob/master/src/data/emacs-mode/agda-input.el#L194
-)_
+## Unicode abbreviations
+
 
     \to    →
     \u+    ⊎
@@ -54,13 +51,20 @@ https://github.com/agda/agda/blob/master/src/data/emacs-mode/agda-input.el#L194
 	x\_1   x₁
 	x\_i   xᵢ
 
-_Bindings for [Agda mode](
-http://agda.readthedocs.io/en/latest/tools/emacs-mode.html
-)_
+Also see [here](
+https://github.com/agda/agda/blob/master/src/data/emacs-mode/agda-input.el#L194
+).
+
+## Bindings for Agda mode
 
     ?            create hole
     {!...!}      create holde
     C-c C-l      reload
     C-c C-c x    split on variable x 
     C-c C-space  fill in hole
-    
+
+
+Also see [here](
+http://agda.readthedocs.io/en/latest/tools/emacs-mode.html
+).
+
diff --git a/index.md b/index.md
index 0aa92552..750defcf 100644
--- a/index.md
+++ b/index.md
@@ -2,21 +2,18 @@
 title  : Table of Contents
 layout : page
 ---
- 
-This is a rewrite of the text
 
-* [Software Foundations](
-  https://softwarefoundations.cis.upenn.edu/current/index.html
-  )
-
-from Coq to Agda. The authors are
-
-* [Wen Kokke](
-  https://github.com/wenkokke
-  )
-* [Philip Wadler](
-  http://homepages.inf.ed.ac.uk/wadler/
-  )
+This is a rewrite of the text [Software Foundations](
+https://softwarefoundations.cis.upenn.edu/current/index.html
+)
+from Coq to Agda. The authors are 
+[Wen Kokke](
+https://github.com/wenkokke
+)
+and  
+[Philip Wadler](
+http://homepages.inf.ed.ac.uk/wadler/
+).
 
 ## Contents