src/HOL/Recdef.thy
changeset 35266 07a56610c00b
parent 32462 c33faa289520
child 35416 d8d7d1b785af
equal deleted inserted replaced
35265:3fd8c3edf639 35266:07a56610c00b