doc-src/Tutorial/Misc/ConstDefs.thy
changeset 8798 d289a68e74ea
parent 5377 efb799c5ed3c