doc-src/TutorialI/Misc/let_rewr.thy

added state: 'a * 'b -> 'a * ('a * 'b);

(*<*)
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 \isa{let}s one could even add \isa{Let_def} permanently:
*}
theorems [simp] = Let_def;
(*<*)
end
(*>*)