src/HOL/Recdef.thy
changeset 7320 e89fd7d0a624
parent 6438 e55a1869ed38
child 7357 d0e16da40ea2
equal deleted inserted replaced
7319:3907d597cae6 7320:e89fd7d0a624