doc-src/Tutorial/Recdef/Sep1.thy
changeset 11491 085a0d2857e8
parent 6100 40d66bc3e83f
equal deleted inserted replaced
11490:f9ae28f55178 11491:085a0d2857e8