src/HOL/Tools/recdef.ML
changeset 33064 ba7ff3f9527a
parent 33056 791a4655cae3
child 33278 ba9f52f56356