* ML/Pure/General: improved join interface for tables;
authorwenzelm
Sun, 12 Feb 2006 21:34:28 +0100
changeset 19034 db16746a5604
parent 19033 24e251657e56
child 19035 678ef6658a0e
* ML/Pure/General: improved join interface for tables;
NEWS
--- a/NEWS	Sun Feb 12 21:34:27 2006 +0100
+++ b/NEWS	Sun Feb 12 21:34:28 2006 +0100
@@ -363,8 +363,8 @@
 * Pure/General/rat.ML implements rational numbers.
 
 * Pure/General/table.ML: the join operations now works via exceptions
-DUP/SAME instead of type option.  This is simpler in simple cases, and
-admits slightly more efficient complex applications.
+DUP/SAME instead of type option.  This is both simpler and admits
+slightly more efficient complex applications.
 
 * Pure: datatype Context.generic joins theory/Proof.context and
 provides some facilities for code that works in either kind of