src/Doc/Tutorial/Recdef/examples.thy
changeset 60480 459f5e017e77
parent 58860 fee7cfa69c50
child 67406 23307fd33906
equal deleted inserted replaced
60479:db238135f386 60480:459f5e017e77