Fetching latest commit…
Cannot retrieve the latest commit at this time
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.