doc-src/TutorialI/ToyList/ROOT.ML
author berghofe
Fri, 03 Apr 2009 10:08:47 +0200
changeset 30860 e5f9477aed50
parent 9834 109b11c4e77e
permissions -rw-r--r--
Added check whether argument types of inductive set agree with types of declared parameters to avoid low-level error messages.

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