Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
..
Failed to load latest commit information.
README
floatScript.sml
ieeeScript.sml

README

This is a directory for the floating point theories in Kananaskis-2
release of HOL-4. Originally developed in HOL Light, by John Harrison,
University of Cambridge Computer Laboratory, 1998. Ported by Behzad
Akbarpour, Concordia University, Department of Electrical and Computer
Engineering, February 2004.

The following is a brief listing of what's available.

     ieeeTheory    * Formalization of IEEE-754 standard for binary
                     floating-point arithmetic.
     floatTheory   * Useful properties of floating point numbers.