src/HOL/Tools/recdef_package.ML
changeset 31378 d1cbf6393964
parent 31243 4c34331a88f9