doc-src/TutorialI/Overview/Ind.thy
changeset 13250 efd5db7dc7cc
parent 13249 4b3de6370184
--- a/doc-src/TutorialI/Overview/Ind.thy	Wed Jun 26 11:07:14 2002 +0200
+++ b/doc-src/TutorialI/Overview/Ind.thy	Wed Jun 26 12:17:21 2002 +0200
@@ -22,8 +22,7 @@
 subsubsection{*Rule Induction*}
 
 text{* Rule induction for set @{term even}, @{thm[source]even.induct}:
-@{thm[display] even.induct[no_vars]}
-*}
+@{thm[display] even.induct[no_vars]}*}
 (*<*)thm even.induct[no_vars](*>*)
 
 lemma even_imp_dvd: "n \<in> even \<Longrightarrow> 2 dvd n"
@@ -83,8 +82,7 @@
 \begin{exercise}
 Show that the converse of @{thm[source]rtc_step} also holds:
 @{prop[display]"[| (x,y) : r*; (y,z) : r |] ==> (x,z) : r*"}
-\end{exercise}
-*}
+\end{exercise}*}
 
 subsection{*The accessible part of a relation*}