src/HOL/Tools/recdef_package.ML
changeset 29211 ab99da3854af
parent 29006 abe0f11cfa4e
child 29579 cb520b766e00
equal deleted inserted replaced
29210:4025459e3f83 29211:ab99da3854af