doc-src/TutorialI/Fun/ROOT.ML
author haftmann
Wed, 01 Sep 2010 16:08:31 +0200
changeset 39022 ac7774a35bcf
parent 38324 749a3e6eb0f4
permissions -rw-r--r--
explicit modify_stmt parameter

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