src/HOL/Tools/recdef.ML
changeset 35064 1bdef0c013d3
parent 34956 fac9d0311725
child 35690 863bee3a9153