1 files changed, 2 insertions, 1 deletions
diff --git a/README.org b/README.org
index 702319a..cba18aa 100644
--- a/README.org
+++ b/README.org
@@ -1,4 +1,5 @@
 #+title: BitEQ
 #+author: Yann Herklotz
 
-Reasoning about bit equality
+Reasoning about bit equality for various rewrites.  This is based on [[file:resources/samc.lisp][proofs]] done in ACL2, and uses
+the =bbv= library to convert the proofs into Coq.