src/HOL/Library/old_recdef.ML
changeset 80145 0eff7d113549
parent 79971 033f90dc441d
equal deleted inserted replaced
80144:cfe18c31725c 80145:0eff7d113549