src/HOL/Recdef.thy
changeset 33566 1c62ac4ef6d1
parent 32462 c33faa289520
child 35416 d8d7d1b785af
equal deleted inserted replaced
33300:939ca97f5a11 33566:1c62ac4ef6d1