Style tweaks to last commit

See also Github PR #1008. Change to use modern syntax, and remove redundant calls to `simp`.
HOL-Theorem-Prover · Jan 11, 2023 · 21546e9 · 21546e9
1 parent 02db589
commit 21546e9
Showing 1 changed file with 5 additions and 7 deletions.
diff --git a/src/floating-point/binary_ieeeScript.sml b/src/floating-point/binary_ieeeScript.sml
@@ -4166,16 +4166,14 @@ val float_div_minus_infinity_finite = Q.store_thm(
 
 (* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -  *)
 
-val float_is_nan_impl = Q.store_thm(
-   "float_is_nan_impl",
-   `!x. float_is_nan x <=> ~float_equal x x`,
+Theorem float_is_nan_impl:
+  !x. float_is_nan x <=> ~float_equal x x
+Proof
    simp[float_is_nan_def, float_equal_def, float_compare_def]
-   \\ STRIP_TAC
+   \\ strip_tac
    \\ Cases_on `float_value x`
    \\ simp[]
-   \\ simp[]
-   \\ simp[]
-   )
+QED
 
 (* ------------------------------------------------------------------------ *)