# HG changeset patch
# User ballarin
# Date 1126874692 -7200
# Node ID 4e603046e53979829d84593681021d96abc40646
# Parent  0eed5a1c00c10125047530e7ebc8a570e768dbbd
tuned

diff -r 0eed5a1c00c1 -r 4e603046e539 NEWS
--- 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.
diff -r 0eed5a1c00c1 -r 4e603046e539 src/FOL/ex/LocaleTest.thy
--- a/src/FOL/ex/LocaleTest.thy	Fri Sep 16 11:39:09 2005 +0200
+++ b/src/FOL/ex/LocaleTest.thy	Fri Sep 16 14:44:52 2005 +0200
@@ -136,7 +136,7 @@
 
 interpretation i3: ID [X "Y::i"] .
 
-(* duplicate: not registered *)
+(* duplicate: thm not added *)
 
 (* thm i3.a.asm_A *)