src/HOL/ex/Recdefs.thy
changeset 11337 9d6d6a8966b9
parent 11024 23bf8d787b04
child 11626 0dbfb578bf75