src/HOL/ex/Recdefs.thy
changeset 11587 cf448586f26a
parent 11024 23bf8d787b04
child 11626 0dbfb578bf75
equal deleted inserted replaced
11586:d8a7f6318457 11587:cf448586f26a