doc-src/TutorialI/Misc/def_rewr.thy
changeset 9843 cc8aa63bdad6
parent 9723 a977245dfc8a