--- a/NEWS Wed Dec 01 20:59:40 2010 +0100
+++ b/NEWS Thu Dec 02 08:34:23 2010 +0100
@@ -92,6 +92,22 @@
*** HOL ***
+* Functions can be declared as coercions and type inference will add them
+as necessary upon input of a term. In Complex_Main, real :: nat => real
+and real :: int => real are declared as coercions. A new coercion function
+f is declared like this:
+
+declare [[coercion f]]
+
+To lift coercions through type constructors (eg from nat => real to
+nat list => real list), map functions can be declared, e.g.
+
+declare [[coercion_map map]]
+
+Currently coercion inference is activated only in theories including real
+numbers, i.e. descendants of Complex_Main. In other theories it needs to be
+loaded explicitly: uses "~~/src/Tools/subtyping.ML"
+
* Abandoned locales equiv, congruent and congruent2 for equivalence relations.
INCOMPATIBILITY: use equivI rather than equiv_intro (same for congruent(2)).