doc-src/TutorialI/Inductive/ROOT.ML
changeset 23686 9d5671f61b31
parent 10762 cd1a2bee5549