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 (*>*)