Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned
authorballarin
Fri, 16 Sep 2005 14:44:52 +0200
changeset 17436 4e603046e539
parent 17435 0eed5a1c00c1
child 17437 9deaf32c83be
tuned
NEWS file | annotate | diff | comparison | revisions
src/FOL/ex/LocaleTest.thy file | annotate | diff | comparison | revisions 
--- 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.
--- 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 *)
isabelle