
diff -r 51451d73c3d4 -r 9e59b4c11039 doc-src/TutorialI/Sets/Examples.thy
--- a/doc-src/TutorialI/Sets/Examples.thy	Thu Sep 30 08:50:45 2010 +0200
+++ b/doc-src/TutorialI/Sets/Examples.thy	Thu Sep 30 09:31:07 2010 +0200
@@ -95,8 +95,8 @@
 text{*
 set extensionality
 
-@{thm[display] set_ext[no_vars]}
-\rulename{set_ext}
+@{thm[display] set_eqI[no_vars]}
+\rulename{set_eqI}
 
 @{thm[display] equalityI[no_vars]}
 \rulename{equalityI}




