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}