doc-src/TutorialI/Inductive/AB.thy
changeset 14610 9c2e31e483b2
parent 12815 1f073030b97a
child 16412 50eab0183aea
equal deleted inserted replaced
14609:663e0e435866 14610:9c2e31e483b2