Prove IEEE connection without cheats

2f1758d1 · Heiko Becker · 81536828 · 2f1758d1 · 2f1758d1
Commit 2f1758d1 authored Sep 27, 2017 by Heiko Becker
Expand all Hide whitespace changes
Inline Side-by-side

Showing with 212 additions and 192 deletions

hol4/IEEE_connectionScript.sml hol4/IEEE_connectionScript.sml +212 -190

hol4/Infra/MachineTypeScript.sml hol4/Infra/MachineTypeScript.sml +0 -2

No files found.
--- a/hol4/IEEE_connectionScript.sml
+++ b/hol4/IEEE_connectionScript.sml
--- a/hol4/Infra/MachineTypeScript.sml
+++ b/hol4/Infra/MachineTypeScript.sml
@@ -161,8 +161,6 @@ which simplifies to 2^(e_max) for base 2
 val maxValue_def = Define `
  maxValue (m:mType) = (&(2n ** (maxExponent m))):real`;

-(** Using the sign bit, the very same number is representable as a negative number,
-  thus just apply negation here **)
 val minValue_def = Define `
 minValue (m:mType) = inv (&(2n ** (minExponentPos m)))`;