doc-src/Tutorial/Recdef/Sep2.thy
changeset 14830 faa4865ba1ce
parent 6100 40d66bc3e83f
equal deleted inserted replaced
14829:cfa5fe01a7b7 14830:faa4865ba1ce