Fixes to README, et cetera

Author: didriklundberg

INSTALL.md

@@ -96,7 +96,7 @@ First, navigate to the directory where you want to put the source code of Poly/M
 	Finally, do
 
 		cd ..
-		make hol
+		Holmake
 		
 	This will build the HOL4 theories and associated libraries.
 
@@ -106,7 +106,7 @@ First, navigate to the directory where you want to put the source code of Poly/M
 		opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
 		opam pin add ott dev -k version
 		
-	This will allow you to re-export the HOL4 definitions in `hol/p4Script.sml` as well as the documentation in `docs/semantics/p4_defs.tex` from the Ott files in the `ott` directory.
+	This will allow you to re-export the HOL4 definitions in `hol/p4Script.sml` as well as the documentation in `docs/semantics/p4_defs.tex` from the Ott files in the `ott` directory using `make hol`.
 
 You may need to repeat `eval $(opam env)` depending on your choice in step 4 in order to use `ott` in the terminal.
 

README.md

@@ -8,8 +8,8 @@ HOL4P4 is a small-step, heapless formalisation and a type system of the P4 langu
   * [Expression](ott/p4_sem.ott#L2494-L2847) 
   * [Statement](ott/p4_sem.ott#L2858-L2986) 
   * [P4 state](ott/p4_sem.ott#L2994-L3026) 
-  * [Architecture-Level](ott/p4_sem.ott#L3033-L3102) 
-  * [Concurrent Architecture-Level](ott/p4_sem.ott#L3116-L3132) 
+  * [Architecture-level](ott/p4_sem.ott#L3033-L3102) 
+  * [Concurrent architecture-level](ott/p4_sem.ott#L3116-L3132) 
 
 * [Proof of determinism for the semantics](hol/p4_deterScript.sml)
 
@@ -66,9 +66,9 @@ To set up the development environment, follow the instructions in [INSTALL.md](I
 
 ## Papers
 
-A. Alshnakat, D. Lundberg, R. Guanciale, M. Dam and K. Palmskog, "HOL4P4: Semantics for a Verified Data Plane", in P4 Workshop in Europe (EuroP4 '22), 2022.
+A. Alshnakat, D. Lundberg, R. Guanciale, M. Dam and K. Palmskog, "HOL4P4: Semantics for a Verified Data Plane" (EuroP4 '22).
 
-A. Alshnakat, D. Lundberg, R. Guanciale, and M. Dam "HOL4P4: Mechanized Small-Step Semantics for P4", to appear in (OOPSLA '24).
+A. Alshnakat, D. Lundberg, R. Guanciale, and M. Dam "HOL4P4: Mechanized Small-Step Semantics for P4" (OOPSLA '24).
 
 ## License
 

hol/p4Script.sml

@@ -1,4 +1,4 @@
-(* generated by Ott 0.33 from: ../ott/p4_types.ott ../ott/p4_sem.ott ../ott/p4.ott *)
+(* generated by Ott 0.34 from: ../ott/p4_types.ott ../ott/p4_sem.ott ../ott/p4.ott *)
 (* to compile: Holmake p4Theory.uo   *)
 (* for interactive use:
   app load ["pred_setTheory","finite_mapTheory","stringTheory","containerTheory","ottLib"];