Document fix to issue #225 (constructor names for theorems)

HOL-Theorem-Prover · Feb 8, 2015 · e08c29e · e08c29e
1 parent 37d61e3
commit e08c29e
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/doc/next-release.md b/doc/next-release.md
@@ -25,6 +25,8 @@ Bugs fixed:
 
 - An embarrassing infinite loop bug in the integration of the integer decision procedures (the Omega test, Cooper’s algorithm) into the simplifier was fixed.
 
+- Theorems can now have names that are the same as SML constructor names (*e.g.*, `Empty`).  ([Github issue](http://github.com/HOL-Theorem-Prover/HOL/issues/225))
+
 New theories:
 -------------