doc-src/TutorialI/Misc/let_rewr.thy
changeset 9541 d17c0b34d5c8
parent 9458 c613cd06d5cf
child 9792 bbefb6ce5cb2
--- a/doc-src/TutorialI/Misc/let_rewr.thy	Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/Misc/let_rewr.thy	Sun Aug 06 15:26:53 2000 +0200
@@ -8,7 +8,7 @@
 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;
+lemmas [simp] = Let_def;
 (*<*)
 end
 (*>*)