doc-src/TutorialI/Inductive/AB.thy
changeset 12124 c4fcdb80c93e
parent 11870 181bd2050cf4
child 12332 aea72a834c85