src/HOL/Tools/recdef.ML
changeset 35437 fe196f61b970
parent 34956 fac9d0311725
child 35690 863bee3a9153