| changeset 15905 | 0a4cc9b113c7 |
| parent 13439 | 2f98365f57a8 |
| child 21324 | a5089fc012b5 |
--- 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](*>*)