changeset 17436 4e603046e539
parent 17425 67c84a7d29f7
child 17442 c0f0b92c198c
--- a/NEWS	Fri Sep 16 11:39:09 2005 +0200
+++ b/NEWS	Fri Sep 16 14:44:52 2005 +0200
@@ -256,7 +256,8 @@
 that are active already do not occur in proof obligations, neither are
 instantiated theorems stored in duplicate.  Use 'print_interps' to
 inspect active interpretations of a particular locale.  For details,
-see the Isar Reference manual.
+see the Isar Reference manual.  Examples can be found in
+HOL/Finite_Set.thy and HOL/Algebra/UnivPoly.thy.
 INCOMPATIBILITY: former 'instantiate' has been withdrawn, use
 'interpret' instead.