doc-src/TutorialI/Inductive/ROOT.ML
changeset 13198 3e40f48a500f
parent 10762 cd1a2bee5549