src/HOL/Recdef.thy
changeset 6563 128cf997c768
parent 6438 e55a1869ed38
child 7357 d0e16da40ea2