Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/TutorialI/Recdef/Nested2.thy
changeset 40878 7695e4de4d86
parent 16417 9bc16273c2d4 
--- a/doc-src/TutorialI/Recdef/Nested2.thy	Thu Dec 02 15:37:32 2010 +0100
+++ b/doc-src/TutorialI/Recdef/Nested2.thy	Thu Dec 02 16:04:22 2010 +0100
@@ -30,7 +30,7 @@
 text{*\noindent
 If the proof of the induction step mystifies you, we recommend that you go through
 the chain of simplification steps in detail; you will probably need the help of
-@{text"trace_simp"}. Theorem @{thm[source]map_cong} is discussed below.
+@{text"simp_trace"}. Theorem @{thm[source]map_cong} is discussed below.
 %\begin{quote}
 %{term[display]"trev(trev(App f ts))"}\\
 %{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
isabelle