Finish IEEE Range Validator to show range to be 0, denormal or normal

hol4/FPRangeValidatorScript.sml

@@ -37,8 +37,8 @@ val FPRangeValidator_def = Define `
         in
             if (validValue (IVhi iv_e_float) m /\
                 validValue (IVlo iv_e_float) m)
-            then (normal (IVlo iv_e_float) m) \/ ((IVlo iv_e_float) = 0) \/
-                 normal (IVhi iv_e_float) m \/ (IVhi iv_e_float) = 0
+            then ((normal (IVlo iv_e_float) m) \/ ((IVlo iv_e_float) = 0) \/
+                 normal (IVhi iv_e_float) m \/ (IVhi iv_e_float) = 0) /\ recRes
             else
                 F
       | NONE => F`;

hol4/Infra/MachineTypeScript.sml

@@ -180,7 +180,7 @@ val normal_def = Define `
 
 val denormal_def = Define `
   denormal (v:real) (m:mType) =
-    ((abs v) <= (minValue m) /\ v <> 0)`;
+    ((abs v) < (minValue m) /\ v <> 0)`;
 
 val validValue_def = Define `
   validValue (v:real) (m:mType) =