src/HOL/Tools/recdef_package.ML
changeset 25835 5dac4855a080
parent 24927 48e08f37ce92
child 26336 a0e2b706ce73