src/HOL/ex/Rewrite_Examples.thy
changeset 74913 c2a2be496f35
parent 74395 5399dfe9141c