doc-src/Tutorial/Recdef/Sep2.thy
changeset 8915 80303d9b0d7b
parent 6100 40d66bc3e83f
equal deleted inserted replaced
8914:e1e4b7313063 8915:80303d9b0d7b