--- a/doc-src/TutorialI/Misc/case_splits.thy Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/case_splits.thy Sun Aug 06 15:26:53 2000 +0200
@@ -63,7 +63,7 @@
locally as above, or by giving it the \isa{split} attribute globally:
*}
-theorems [split] = list.split;
+lemmas [split] = list.split;
text{*\noindent
The \isa{split} attribute can be removed with the \isa{del} modifier,
@@ -79,7 +79,7 @@
text{*\noindent
or globally:
*}
-theorems [split del] = list.split;
+lemmas [split del] = list.split;
(*<*)
end