doc-src/Tutorial/Recdef/Sep2.thy
changeset 8811 6ec0c8f9d68d
parent 6100 40d66bc3e83f
equal deleted inserted replaced
8810:d0eae42f6d12 8811:6ec0c8f9d68d