src/HOL/Tools/recdef.ML
changeset 42961 f30ae82cb62e
parent 42795 66fcc9882784
child 43278 1fbdcebb364b