summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Thu, 17 May 2001 11:31:08 +0200 | |

changeset 11303 | f0661da2f6ae |

parent 11302 | 9e0708bb15f7 |

child 11304 | 0db2a02bff99 |

typo, etc.

--- a/doc-src/TutorialI/Trie/Trie.thy Thu May 17 11:29:04 2001 +0200 +++ b/doc-src/TutorialI/Trie/Trie.thy Thu May 17 11:31:08 2001 +0200 @@ -137,10 +137,10 @@ \begin{exercise} Modify @{term update} (and its type) such that it allows both insertion and - deletion of entries with a single function. Prove (a modified version of) - the main theorem above. - Optimize you function such that it shrinks tries after - deletion, if possible. + deletion of entries with a single function. Prove the corresponding version + of the main theorem above. + Optimize your function such that it shrinks tries after + deletion if possible. \end{exercise} \begin{exercise}