Fix bug in reduceLib.NOT_CONV

Thanks to someplaceguy for bug report.

Author: mn200

src/num/reduce/src/Boolconv.sml

@@ -46,7 +46,7 @@ fun NOT_CONV tm =
  let val xn = dest_neg tm
  in if aconv xn T then c1 else
     if aconv xn F then c2
-    else let val xn' = dest_neg xn in SPEC xn c3 end
+    else let val xn' = dest_neg xn in SPEC xn' c3 end
  end handle HOL_ERR _ => raise ERR "NOT_CONV" ""
 end;
 

src/num/reduce/src/selftest.sml

@@ -38,5 +38,10 @@ val _ = app (fn (n,c,t) => convtest(n,c,lhs t,rhs t)) [
   ("EVEN_CONV(3)", EVEN_CONV, “EVEN 0 <=> T”),
   ("ODD_CONV(1)", ODD_CONV, “ODD 106 <=> F”),
   ("ODD_CONV(2)", ODD_CONV, “ODD 103 <=> T”),
-  ("ODD_CONV(3)", ODD_CONV, “ODD 0 <=> F”)
+  ("ODD_CONV(3)", ODD_CONV, “ODD 0 <=> F”),
+
+  ("NOT_CONV(1)", NOT_CONV, “~T <=> F”),
+  ("NOT_CONV(2)", NOT_CONV, “~F <=> T”),
+  ("NOT_CONV(3)", NOT_CONV, “~~p <=> p”),
+  ("NOT_CONV(4)", NOT_CONV, “~~~q <=> ~q”)
 ]