doc-src/TutorialI/Inductive/AB.thy
changeset 31085 e270f45ac0ec
parent 27167 a99747ccba87