README
1This is a directory for the floating point theories in Kananaskis-2
2release of HOL-4. Originally developed in HOL Light, by John Harrison,
3University of Cambridge Computer Laboratory, 1998. Ported by Behzad
4Akbarpour, Concordia University, Department of Electrical and Computer
5Engineering, February 2004.
6
7The following is a brief listing of what's available.
8
9 ieeeTheory * Formalization of IEEE-754 standard for binary
10 floating-point arithmetic.
11 floatTheory * Useful properties of floating point numbers.
12
13