doc-src/TutorialI/ToyList/ROOT.ML
author blanchet
Thu, 05 May 2011 00:22:37 +0200
changeset 42688 097a61baeca9
parent 9834 109b11c4e77e
permissions -rw-r--r--
smoother handling of ! and ? in type system names

use "../settings.ML";
use_thy "ToyList";