changeset 8771 | 026f37a86ea7 |
parent 8745 | 13b32661dde4 |
child 9458 | c613cd06d5cf |
--- a/doc-src/TutorialI/Misc/let_rewr.thy Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Misc/let_rewr.thy Tue Apr 25 08:09:10 2000 +0200 @@ -6,7 +6,7 @@ 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: +of nested \isa{let}s one could even add \isa{Let_def} permanently: *} theorems [simp] = Let_def; (*<*)