src/HOL/Recdef.thy
changeset 6554 5be3f13193d7
parent 6438 e55a1869ed38
child 7357 d0e16da40ea2