src/HOL/Tools/recdef_package.ML
changeset 23315 df3a7e9ebadb
parent 22846 fb79144af9a3
child 24039 273698405054