doc-src/TutorialI/Inductive/ROOT.ML
author wenzelm
Mon, 23 Oct 2000 22:10:36 +0200
changeset 10309 a7f961fb62c6
parent 10225 b9fd52525b69
child 10341 6eb91805a012
permissions -rw-r--r--
intro_classes by default;

use "../settings.ML";
use_thy "Star";
use_thy "AB";