diff -r a6fb4ddc05c7 -r 0a4cc9b113c7 doc-src/TutorialI/Overview/LNCS/Ind.thy --- a/doc-src/TutorialI/Overview/LNCS/Ind.thy Mon May 02 10:56:13 2005 +0200 +++ b/doc-src/TutorialI/Overview/LNCS/Ind.thy Mon May 02 11:03:27 2005 +0200 @@ -21,7 +21,7 @@ subsubsection{*Rule Induction*} -text{* Rule induction for set @{term even}, @{thm[source]even.induct}: +text{* Rule induction for set @{const even}, @{thm[source]even.induct}: @{thm[display] even.induct[no_vars]}*} (*<*)thm even.induct[no_vars](*>*)