doc-src/TutorialI/Inductive/AB.thy
changeset 31795 be3e1cc5005c
parent 27167 a99747ccba87