doc-src/TutorialI/Recdef/termination.thy
changeset 10498 777d6bde7b47
parent 10186 499637e8f2c6
child 10522 ed3964d1f1a4
equal deleted inserted replaced
10497:7c6985b4de40 10498:777d6bde7b47