src/HOL/Tools/recdef_package.ML
changeset 12791 ccc0f45ad2c4
parent 12755 a906a8b364f1
child 12876 a70df1e5bf10