doc-src/TutorialI/Inductive/ROOT.ML
changeset 41710 11ae688e4e30
parent 10762 cd1a2bee5549