# HG changeset patch
# User huffman
# Date 1127408381 -7200
# Node ID 6eab0f1cb0fe705a07edc50888a984d7046e63eb
# Parent  c272b91b619f6364267475db6ef7f11e123a9404
HOLCF theorem naming conventions

diff -r c272b91b619f -r 6eab0f1cb0fe NEWS
--- a/NEWS	Thu Sep 22 14:09:48 2005 +0200
+++ b/NEWS	Thu Sep 22 18:59:41 2005 +0200
@@ -674,6 +674,16 @@
 requirement. The packages generate instances of class cpo or pcpo,
 with continuity and strictness theorems for Rep and Abs.
 
+* HOLCF: Many theorems have been renamed according to a more standard naming
+scheme (INCOMPATIBILITY):
+
+  foo_inject:  "foo$x = foo$y ==> x = y"
+  foo_eq:      "(foo$x = foo$y) = (x = y)"
+  foo_less:    "(foo$x << foo$y) = (x << y)"
+  foo_strict:  "foo$UU = UU"
+  foo_defined: "... ==> foo$x ~= UU"
+  foo_defined_iff: "(foo$x = UU) = (x = UU)"
+
 
 *** ZF ***