src/HOL/Tools/recdef.ML
changeset 33205 20587741a8d9
parent 33056 791a4655cae3
child 33278 ba9f52f56356