src/HOL/ex/Rewrite_Examples.thy
changeset 73330 0fb889c361e6
parent 69597 ff784d5a5bfb
child 74395 5399dfe9141c