src/HOL/Recdef.thy
changeset 23000 6f158bba99e4
parent 22622 25693088396b
child 23150 073a65f0bc40
equal deleted inserted replaced
22999:c1ce129e6f9c 23000:6f158bba99e4