# HG changeset patch # User paulson # Date 1006249718 -3600 # Node ID 3dd9aae402bbe0263cec0d61842ecd9208a90ff8 # Parent 179f142ffb03e5791dacb3ce350c401781d428e5 Hyperreal diff -r 179f142ffb03 -r 3dd9aae402bb NEWS --- a/NEWS Mon Nov 19 23:37:01 2001 +0100 +++ b/NEWS Tue Nov 20 10:48:38 2001 +0100 @@ -418,8 +418,9 @@ * HOL: improved concrete syntax for strings (e.g. allows translation rules with string literals); -* HOL-Hyperreal: a new target, extending HOL-Real with the hyperreals -and Fleuriot's mechanization of analysis; +* HOL-Real-Hyperreal: this extends HOL-Real with the hyperreals + and Fleuriot's mechanization of analysis, including the transcendental + functions for the reals; * HOL/Real, HOL/Hyperreal: improved arithmetic simplification;