doc-src/TutorialI/Inductive/AB.thy
changeset 43307 1a32a953cef1
parent 27167 a99747ccba87