doc-src/TutorialI/Inductive/ROOT.ML
changeset 12916 4ac388e02b74
parent 10762 cd1a2bee5549