src/HOL/Recdef.thy
changeset 10246 d8c968e6329a
parent 10212 33fe2d701ddd
child 10653 55f33da63366
equal deleted inserted replaced
10245:87771e2f49fe 10246:d8c968e6329a