KeY-Version for Schorr-Waite
============================

Support for non-rigid function and predicate symbols with known dependencies
is not yet integrated in KeY 1.0. It will be incorporated in the near time
future. 

A beta version of KeY with support of these symbols and with which
Schorr-Waite has been proven can be found in this directory. The file is
called:
   KeYSystemWithLocationDependantSymbols.tgz

For compilation of the system all steps have to be done as described for the
source code version of KeY 1.0. In particular it requires the libraries
provided with KeY 1.0 (it will NOT work with the libraries of KeY 1.0pre-xyz)
versions.

The directory spec/ contains the proof obligation and the completed proof to
be loaded (schorrWaiteVisitedAndStructurePreserving.(key|proof)). In
addition correctness proofs for all used derived rules have been added. 

The directory "src/" contains the implementation of Schorr-Waite.