src/HOL/Recdef.thy
changeset 19136 00ade10f611d
parent 18336 1a2e30b37ed3
child 19564 d3e2f532459a
equal deleted inserted replaced
19135:2de31ba562d7 19136:00ade10f611d