From fada2dbdedda2c521d8b35c41f8f882708eedb1a Mon Sep 17 00:00:00 2001
From: Joseph Chan <jhlchan@gmail.com>
Date: Wed, 16 Aug 2023 23:08:08 +1000
Subject: [PATCH] Slight edit of documentation.

---
 examples/fermat/twosq/cornerScript.sml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/examples/fermat/twosq/cornerScript.sml b/examples/fermat/twosq/cornerScript.sml
index f85f00db6b..e9eba52a3c 100644
--- a/examples/fermat/twosq/cornerScript.sml
+++ b/examples/fermat/twosq/cornerScript.sml
@@ -1024,7 +1024,7 @@ QED
     ==> ?q. q IN s                             by MEMBER_NOT_EMPTY
     ==> ?a b. q = (a,a,b,b) /\
               p = a ** 2 + b ** 2 /\ a < b     by corners_less_fix_def
-   Take them and form a pair (a,b).
+   Take these values of a and b.
 *)
 Theorem fermat_two_squares_by_corners:
   !p. tik p /\ prime p ==> ?a b. p = a ** 2 + b ** 2 /\ a < b