| changeset 39795 | 9e59b4c11039 |
| parent 39128 | 93a7365fb4ee |
| child 41413 | 64cd30d6b0b8 |
--- 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}