doc-src/TutorialI/Recdef/termination.thy
changeset 11420 9529d31f39e0
parent 11309 d666f11ca2d4
child 11429 30da2f5eaf57