src/HOL/Recdef.thy
changeset 6977 4781c0673e83
parent 6438 e55a1869ed38
child 7357 d0e16da40ea2