doc-src/TutorialI/Inductive/AB.thy
changeset 12587 3f3d2ffb5df5
parent 12332 aea72a834c85
child 12815 1f073030b97a