src/HOL/Tools/recdef.ML
changeset 56024 0921c1dc344c
parent 55997 9dc5ce83202c
child 56029 8bedca4bd5a3