src/HOL/Tools/recdef_package.ML
changeset 18052 004515accc10
parent 17920 5c3e9415c653
child 18377 0e1d025d57b3