src/Doc/Tutorial/Recdef/examples.thy
changeset 78750 f229090cb8a3
parent 69505 cc2d676d5395
equal deleted inserted replaced
78749:23215f71ab69 78750:f229090cb8a3