doc-src/TutorialI/ToyList2/ROOT.ML
author haftmann
Wed, 21 Sep 2005 17:25:32 +0200
changeset 17565 7322f37d3344
parent 8745 13b32661dde4
permissions -rw-r--r--
introduces update_warn instead of overwrite_warn

use_thy "ToyList";