src/HOL/ex/Recdefs.thy
changeset 24665 e5bea50b9b89
parent 16417 9bc16273c2d4
child 37456 0a1cc2675958
equal deleted inserted replaced
24664:4195de64fdb1 24665:e5bea50b9b89