doc-src/TutorialI/Misc/def_rewr.thy
changeset 9742 98d3ca2c18f7
parent 9723 a977245dfc8a