doc-src/Tutorial/Recdef/Sep2.thy
changeset 8390 e5b618f6824e
parent 6100 40d66bc3e83f
equal deleted inserted replaced
8389:130109a9b8c1 8390:e5b618f6824e