doc-src/TutorialI/Inductive/AB.thy
changeset 24543 e2332d1ff6c7
parent 23733 3f8ad7418e55
child 25330 15bf0f47a87d