doc-src/TutorialI/Fun/ROOT.ML
author haftmann
Thu, 02 Sep 2010 16:41:42 +0200
changeset 39065 16a2ed09217a
parent 38324 749a3e6eb0f4
permissions -rw-r--r--
set depth to 1

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