doc-src/TutorialI/ToyList2/ROOT.ML
author paulson
Thu, 30 Nov 2000 17:55:17 +0100
changeset 10546 b0ad1ed24cf6
parent 8745 13b32661dde4
permissions -rw-r--r--
replaced Eps by SOME

use_thy "ToyList";