doc-src/Tutorial/Recdef/Sep2.thy
changeset 14336 8f731d3cd65b
parent 6100 40d66bc3e83f
equal deleted inserted replaced
14335:9c0b5e081037 14336:8f731d3cd65b