NameDateSize

..25-Jul-201969

floatScript.smlH A D01-Mar-202050.7 KiB

ieeeScript.smlH A D25-Jul-201922.9 KiB

READMEH A D25-Jul-2019544

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