doc-src/TutorialI/Misc/let_rewr.thy

--- a/doc-src/TutorialI/Misc/let_rewr.thy	Fri Sep 01 18:29:52 2000 +0200
+++ b/doc-src/TutorialI/Misc/let_rewr.thy	Fri Sep 01 19:09:44 2000 +0200
@@ -1,12 +1,23 @@
 (*<*)
 theory let_rewr = Main:;
 (*>*)
+
+subsubsection{*Simplifying let-expressions*}
+
+text{*\index{simplification!of let-expressions}
+Proving a goal containing \isaindex{let}-expressions almost invariably
+requires the @{text"let"}-con\-structs to be expanded at some point. Since
+@{text"let"}-@{text"in"} is just syntactic sugar for a predefined constant
+(called @{term"Let"}), expanding @{text"let"}-constructs means rewriting with
+@{thm[source]Let_def}:
+*}
+
 lemma "(let xs = [] in xs@ys@xs) = ys";
 by(simp add: Let_def);
 
 text{*
 If, in a particular context, there is no danger of a combinatorial explosion
-of nested \isa{let}s one could even add \isa{Let_def} permanently:
+of nested @{text"let"}s one could even add @{thm[source]Let_def} permanently:
 *}
 lemmas [simp] = Let_def;
 (*<*)