From a6d01abbdd5350177acbf20732eed398700fd378 Mon Sep 17 00:00:00 2001
From: Nick Smallbone <nick@smallbone.se>
Date: Mon, 11 Sep 2017 19:41:19 +0200
Subject: [PATCH] Update README

---
 README | 26 +++++++++++++++++++-------
 1 file changed, 19 insertions(+), 7 deletions(-)

diff --git a/README b/README
index 49c43fb..60183f6 100644
--- a/README
+++ b/README
@@ -1,10 +1,22 @@
-This is twee, a prover for equational problems.
+This is twee, an equational theorem prover.
 
-To install, run cabal install.
+The version in this git repository is likely to be unstable!
+To install the latest stable version, run:
 
-Afterwards, invoke as twee nameofproblem.p. The problem should be in
-TPTP format (http://www.tptp.org). You can find a few examples in the
-tests directory. All axioms and conjectures must be equations, but you
-can freely use types and quantifiers.
+    cabal install twee
 
-Twee is experimental software, use at your own risk!
+If you have LLVM installed, you can get a slightly faster version by
+running:
+
+    cabal install twee -fllvm
+
+If you really want the latest unstable version, run `cabal install` in
+this repository. You will most likely need the latest git version of
+Jukebox, from https://github.com/nick8325/jukebox, too - and things
+may break from time to time.
+
+Afterwards, run `twee nameofproblem.p`. The problem should be in TPTP
+format (http://www.tptp.org). You can find a few examples in the
+`tests` directory. All axioms and conjectures must be equations, but
+you can freely use quantifiers. If it succeeds in proving your
+problem, twee will print a human-readable proof.