diff -r 22fa8b16c3ae -r 13b32661dde4 doc-src/TutorialI/Misc/let_rewr.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/let_rewr.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,14 @@
+(*<*)
+theory let_rewr = Main:;
+(*>*)
+lemma "(let xs = [] in xs@ys@xs) = ys";
+apply(simp add: Let_def).;
+
+text{*
+If, in a particular context, there is no danger of a combinatorial explosion
+of nested \texttt{let}s one could even add \texttt{Let_def} permanently:
+*}
+theorems [simp] = Let_def;
+(*<*)
+end
+(*>*)