Merge remote-tracking branch 'fdedden/develop-fix-nonexisting-readme'. Close #452.

**Description**

`copilot-theorem`'s README mentions a file `Driver.hs` that is not part
of the library:
```
As an example, the following prover is used in Driver.hs:
```
and later
```
Some examples are in the examples folder. The Driver.hs contains the
main function to run any example.
```

It also says that there are two provers: one based on `Kind2`, and one
called `lightProver`. The latter no longer exists, but we do have a
`What4` module now.

These mentions should be adjusted or removed.

**Type**

- Bug: incorrect documentation.

**Additional context**

None.

**Requester**

- Max Fan (NASA)

**Method to check presence of bug**

Running a search through the tree brings up several mentions:
```
$ grep -nIHre 'Driver.hs'
copilot-theorem/README.md:205:As an example, the following prover is used in `Driver.hs`:
copilot-theorem/README.md:254:Some examples are in the *examples* folder. The `Driver.hs` contains the `main`
copilot-theorem/README.md:257:by changing one *import* directive in `Driver.hs`.
```

```
$ grep -nIHre 'lightProver'
copilot-theorem/README.md:79:prove (lightProver def) (check "gt0") spec
copilot-theorem/README.md:82:where `lightProver def` stands for the *light prover* with default
copilot-theorem/README.md:150:`lightProver :: Options -> Prover` function which builds a prover from a record
copilot-theorem/README.md:209:  lightProver def {onlyBmc = True, kTimeout = 5}
```

```
$ grep -nIHre '\<Light\>' | grep -ve 'XML'
copilot-theorem/README.md:71:  the `Copilot.Theorem.Light` and `Copilot.Theorem.Kind2` module.
copilot-theorem/README.md:123:Two provers are provided by default: `Light` and `Kind2`.
copilot-theorem/README.md:149:The *light prover* is defined in `Copilot.Theorem.Light`. This module exports the
copilot-theorem/README.md:399:#### The Light prover
copilot-theorem/README.md:402:basic *k-induction* algorithm [1]. The `Light` directory contains three files:
```

**Expected result**

The output of the above `grep` commands is empty, indicating that that
inexisting file/modules/functions are not mentioned.

**Solution implemented**

The README has been adjusted to match the current interface.
Specifically, the references above have been fixed, and any code
examples updated to use currently supported APIs.

**Further notes**

None.

Author: ivanperez-keera

copilot-theorem/CHANGELOG

@@ -1,5 +1,6 @@
-2024-05-05
+2024-05-07
         * Fix handling of unsatisfiable properties with Kind2. (#495)
+        * Remove outdated details from README. (#452)
 
 2024-03-07
         * Version bump (3.19). (#504)