src/Doc/Tutorial/Recdef/examples.thy
changeset 81627 079dee3b117c
parent 69505 cc2d676d5395
equal deleted inserted replaced
81622:91a7e5719b2b 81627:079dee3b117c