doc-src/TutorialI/Inductive/ROOT.ML
changeset 11610 99103cef5f29
parent 10762 cd1a2bee5549