doc-src/Tutorial/Misc/Last.thy
changeset 8010 69032a618aa9
parent 5377 efb799c5ed3c