This directory contains the prover files for Joanna Guild's proof that every
real number has a square root, which is supporting work for her Master's thesis.

This file tells you how to run the proof.

You need Moscow ML.

You need the old version of the theorem prover (marcelsequent.sml) and the new
version (marcel.sml).  Compile these in Moscow ML.
Use the versions of these files found in this directory, not the versions on the main web page, which may reflect updates which will break these proofs.

Under the old prover,

use "background.txt";
use "guildproofs.txt";
use "SQRT33.txt";

You will need to hit return to get past messages and displays generated by
these files.  Some of these messages look like error messages, but there
are no essential errors in the files; ignore these messages.

At this point if working from scratch you would run

savetheory "JoannaFinal";

I provide the theory files generated by this command (JoannaFinal with
various extensions).

Now open the new prover (best done in a new Moscow ML window).

loadtheory "JoannaFinal";
use "SQRT.txt";

completes the process.