doc-src/TutorialI/Inductive/ROOT.ML
changeset 30535 db8b10fd51a4
parent 10762 cd1a2bee5549