doc-src/Tutorial/Misc/Defs.thy
changeset 13854 91c9ab25fece
parent 5377 efb799c5ed3c