Specware has a base library that is implicitly imported by every spec. Unfortunately, the axioms in this library are not necessarily written to be useful by Snark. Instead of having Snark use these libraries we have created a separate base library for Snark. This library is located at /Library/ProverBase/. For each spec in /Library/Base/ there is a corresponding prover spec that shadows it. This prover base spec imports the 'op and 'type declarations from the corresponding base spec, and substitututes for the original definitions and axioms, axioms that are more appropriate for sending to Snark. The axioms in these specs are automatically sent to Snark as part of any proof.