doc-src/Tutorial/ToyList/ROOT.ML
author paulson
Thu, 28 Jan 1999 18:28:06 +0100
changeset 6160 32c0b8f57bb7
parent 5377 efb799c5ed3c
permissions -rw-r--r--
tidied

use_thy "ToyList";