1.1 --- a/doc-src/TutorialI/Recdef/Nested2.thy	Fri Sep 01 18:29:52 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Recdef/Nested2.thy	Fri Sep 01 19:09:44 2000 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4  applies it automatically and the above definition of @{term"trev"}
     1.5  succeeds now. As a reward for our effort, we can now prove the desired
     1.6  lemma directly. The key is the fact that we no longer need the verbose
     1.7 -induction schema for type @{name"term"} but the simpler one arising from
     1.8 +induction schema for type @{text"term"} but the simpler one arising from
     1.9  @{term"trev"}:
    1.10  *};
    1.11  
    1.12 @@ -39,7 +39,7 @@
    1.13  text{*\noindent
    1.14  If the proof of the induction step mystifies you, we recommend to go through
    1.15  the chain of simplification steps in detail; you will probably need the help of
    1.16 -@{name"trace_simp"}.
    1.17 +@{text"trace_simp"}.
    1.18  %\begin{quote}
    1.19  %{term[display]"trev(trev(App f ts))"}\\
    1.20  %{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
    1.21 @@ -66,7 +66,7 @@
    1.22  \isacommand{recdef} would try to prove the unprovable @{term"size t < Suc
    1.23  (term_list_size ts)"}, without any assumption about @{term"t"}.  Therefore
    1.24  \isacommand{recdef} has been supplied with the congruence theorem
    1.25 -@{name"map_cong"}:
    1.26 +@{thm[source]map_cong}:
    1.27  \begin{quote}
    1.28  @{thm[display,margin=50]"map_cong"[no_vars]}
    1.29  \end{quote}