src/HOL/Tools/recdef_package.ML
changeset 21745 a1d8806b5267
parent 21505 13d4dba99337
child 22101 6d13239d5f52