doc-src/TutorialI/Recdef/termination.thy
changeset 9016 d61c76716984
parent 8771 026f37a86ea7
child 9458 c613cd06d5cf
equal deleted inserted replaced
9015:8006e9009621 9016:d61c76716984