tweak README

1 files changed, 26 insertions, 38 deletions

diff --git a/README.md b/README.md
index 5315026..2836ff6 100644
--- a/README.md
+++ b/README.md
@@ -5,10 +5,17 @@ This repository contains a model of the RISCV architecture written in
 [Sail](https://www.cl.cam.ac.uk/~pes20/sail/). It used to be contained
 in the [Sail repository](https://github.com/rems-project/sail).
 
-It currently implements enough of RV32IMAC and RV64IMAC to boot a
+It currently defines enough of RV32IMAC and RV64IMAC to boot a
 conventional OS with a terminal output device.  The model specifies
 assembly language formats of the instructions, the corresponding
 encoders and decoders, and the instruction semantics.
+The current status of its
+coverage of the prose RISC-V specification is summarized
+[here](doc/Status.md).
+A [reading guide](doc/ReadingGuide.md) to the model is provided in the
+[doc/](doc/) subdirectory, along with a guide on [how to
+extend](doc/ExtendingGuide.md) the model. 
+
 
 This is one of [several formal models](https://github.com/riscv/ISA_Formal_Spec_Public_Review/blob/master/comparison_table.md) compared within the 
 [RISC-V ISA Formal Spec Public Review](https://github.com/riscv/ISA_Formal_Spec_Public_Review).
@@ -19,48 +26,29 @@ Directory Structure
 
 ```
 sail-riscv
-|
-+---- model                   // Sail specification modules
-|
-+---- generated_definitions   // Files generated by Sail, in RV32 and RV64 subdirectories
-|     |
-|     +---- c
-|     +---- ocaml
-|     +---- lem
-|     +---- isabelle
-|     +---- coq
-|     +---- hol4
-|     +---- latex
-|
-+---- prover_snapshots        // Snapshots of generated theorem prover definitions
-|
-|---- handwritten_support     // Prover support files
-|
-+---- c_emulator              // supporting platform files for C emulator
-+---- ocaml_emulator          // supporting platform files for OCaml emulator
-|
-+---- doc                     // documentation, including a reading-guide
-|
-+---- test                    // test files
-|     |
-|     +---- riscv-tests       // snapshot of tests from the riscv/riscv-tests github repo
-|
-+---- os-boot                 // information and sample files for booting OS images
+- model                   // Sail specification modules
+- generated_definitions   // files generated by Sail, in RV32 and RV64 subdirectories
+  -  c
+  -  ocaml
+  -  lem
+  -  isabelle
+  -  coq
+  -  hol4
+  -  latex
+- prover_snapshots        // snapshots of generated theorem prover definitions
+- handwritten_support     // prover support files
+- c_emulator              // supporting platform files for C emulator
+- ocaml_emulator          // supporting platform files for OCaml emulator
+- doc                     // documentation, including a reading guide
+- test                    // test files
+  - riscv-tests           // snapshot of tests from the riscv/riscv-tests github repo
+- os-boot                 // information and sample files for booting OS images
 ```
 
-Documentation
--------------
-
-A [reading guide](doc/ReadingGuide.md) to the model is provided in the
-[doc/](doc/) subdirectory, along with a guide on [how to
-extend](doc/ExtendingGuide.md) the model.  The current status of the
-coverage of the prose RISC-V specification is summarized
-[here](doc/Status.md).
-
 Simulators
 ----------
 
-The files in the OCaml and C simulators implement ELF-loading and the
+The files in the OCaml and C emulator directories implement ELF loading and the
 platform devices, define the physical memory map, and use command-line
 options to select implementation-specific ISA choices.