src/Doc/Tutorial/Recdef/examples.thy
changeset 73376 96ef620c8b1e
parent 69505 cc2d676d5395
equal deleted inserted replaced
73375:a80fd78c85bd 73376:96ef620c8b1e