src/HOL/Recdef.thy
changeset 22277 b89dc456dbc6
parent 22264 6a65e9b2ae05
child 22399 80395c2c40cc
equal deleted inserted replaced
22276:96a4db55a0b3 22277:b89dc456dbc6