doc-src/TutorialI/Inductive/AB.thy
changeset 23655 d2d1138e0ddc
parent 23380 15f7a6745cce
child 23733 3f8ad7418e55