doc-src/TutorialI/ToyList2/ROOT.ML
author blanchet
Mon, 06 Jun 2011 20:36:35 +0200
changeset 43199 45f33d290615
parent 8745 13b32661dde4
permissions -rw-r--r--
make "metisX"'s default more like old "metis"

use_thy "ToyList";