From fb7e820e4ddb5c91321dd3a7f01c1128257c2328 Mon Sep 17 00:00:00 2001
From: Hannes Mehnert <hannes@mehnert.org>
Date: Sun, 17 Sep 2017 00:25:21 +0100
Subject: [PATCH] .

---
 Technology | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Technology b/Technology
index 2c2e94c..cb76142 100644
--- a/Technology
+++ b/Technology
@@ -142,8 +142,7 @@ module interface.
 ### Verification
 
 A large subset of the OCaml semantics has been
-[mechanized](http://www.cl.cam.ac.uk/~so294/ocaml/) in a theorem prover, and
-this metatheory is verified.
+[mechanically proven sound](http://www.cl.cam.ac.uk/~so294/ocaml/) in a theorem prover.
 
 OCaml is the implementation language of the well-known proof assistant
 [Coq](https://coq.inria.fr).  Development in Coq can be extracted to OCaml code,