diff -r cc8aa63bdad6 -r 8016321c7de1 doc-src/TutorialI/Misc/let_rewr.thy
--- a/doc-src/TutorialI/Misc/let_rewr.thy	Tue Sep 05 13:12:00 2000 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-(*<*)
-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 @{text"let"}s one could even add @{thm[source]Let_def} permanently:
-*}
-lemmas [simp] = Let_def;
-(*<*)
-end
-(*>*)