src/HOL/Recdef.thy
changeset 7143 9c02848c5404
parent 6438 e55a1869ed38
child 7357 d0e16da40ea2
equal deleted inserted replaced
7142:89e0ff71d113 7143:9c02848c5404