doc-src/TutorialI/Recdef/termination.thy
changeset 12333 ef43a3d6e962
parent 12332 aea72a834c85
child 12473 f41e477576b9