# HG changeset patch
# User nipkow
# Date 1291275263 -3600
# Node ID ff53be5021337485e07b64c5d4bfc40a9d2da3b4
# Parent  ed30aeccf9491ad9ee9dd5e67007ecf5a943f962
coercions

diff -r ed30aeccf949 -r ff53be502133 NEWS
--- 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)).