doc-src/TutorialI/Inductive/AB.thy
changeset 10395 7ef380745743
parent 10287 9ab1671398a6
child 10396 5ab08609e6c8