doc-src/Tutorial/Misc/Sep2.thy
changeset 7527 9e2dddd8b81f
parent 5377 efb799c5ed3c