

Why3 is a tool for automated and interactive proving in first-order
polymorphic logic. It provides a collection of command-line tools, a
graphical interface and an Objective Caml library.

PROJECT HOME
============

https://gforge.inria.fr/projects/why3

DOCUMENTATION
=============

The documentation (a tutorial and a reference manual) is in
the file doc/manual.pdf.

Various examples can be found in the subdirectories theories/
and examples/.

Mailing list (Why3 Club):
  http://lists.gforge.inria.fr/mailman/listinfo/why3-club

Bug Tracking System:
  https://gforge.inria.fr/tracker/?atid=10293&group_id=2990&func=browse

COPYRIGHT
=========

This program is distributed under the GNU LGPL 2.1. See the enclosed
file LICENSE.

The files src/util/stdlib.ml{i} are derived from the sources of
OCaml 3.12 standard library, and are distributed under the GNU
LGPL version 2 (see file OCAML-LICENSE).

INSTALLATION
============

See the file INSTALL.
