src/HOL/Tools/recdef.ML
changeset 58223 ba7a2d19880c
parent 58048 aa6296d09e0e
child 58825 2065f49da190