doc-src/TutorialI/Inductive/ROOT.ML
author wenzelm
Wed, 13 Aug 2008 20:57:39 +0200
changeset 27862 8f727f7c8c1d
parent 10762 cd1a2bee5549
permissions -rw-r--r--
removed obsolete verbatim_source, results, chapter, section etc.; removed obsolete results, theorems(s); moved theorem result hook to proof_display.ML;

use "../settings.ML";
use_thy "Even";
use_thy "Mutual";
use_thy "Star";
use_thy "AB";
use_thy "Advanced";