src/HOL/Recdef.thy
changeset 22871 9ffb43b19ec6
parent 22622 25693088396b
child 23150 073a65f0bc40
equal deleted inserted replaced
22870:c37e32bdbea2 22871:9ffb43b19ec6