Update readme.

1 files changed, 12 insertions, 5 deletions

diff --git a/README.md b/README.md
index 0e1b11a..f0e52d0 100644
--- a/README.md
+++ b/README.md
@@ -63,19 +63,26 @@ your environment pointing to its top-level directory.
 ```
 $ make
 ```
-will build the OCaml simulator in `ocaml_emulator/riscv_ocaml_sim`, the C simulator in
-`c_emulator/riscv_sim`, the Isabelle model in `generated_definitions/isabelle/Riscv.thy`, the Coq
-model in `generated_definitions/coq/riscv.v`, and the HOL4 model in
-`generated_definitions/hol4/riscvScript.sml`.
+will build the 64-bit OCaml simulator in
+`ocaml_emulator/riscv_ocaml_sim_RV64`, the C simulator in
+`c_emulator/riscv_sim_RV64`, the Isabelle model in
+`generated_definitions/isabelle/RV64/Riscv.thy`, the Coq model in
+`generated_definitions/coq/RV64/riscv.v`, and the HOL4 model in
+`generated_definitions/hol4/RV64/riscvScript.sml`.
 
 One can build either the RV32 or the RV64 model by specifying
-`ARCH=RV32` or `ARCH=RV64` on the `make` line.  RV64 is built by
+`ARCH=RV32` or `ARCH=RV64` on the `make` line, and using the matching target suffix.  RV64 is built by
 default, but the RV32 model can be built using:
 
 ```
 $ ARCH=RV32 make
 ```
 
+which creates the 32-bit OCaml simulator in
+`ocaml_emulator/riscv_ocaml_sim_RV32`, and the C simulator in
+`c_emulator/riscv_sim_RV32`, and the prover models in the
+corresponding `RV32` subdirectories.
+
 The Makefile targets `riscv_isa_build`, `riscv_coq_build`, and
 `riscv_hol_build` invoke the respective prover to process the definitions.  We
 have tested Isabelle 2018, Coq 8.8.1, and HOL4 Kananaskis-12.