src/HOL/ex/Recdefs.thy
changeset 11263 e502756bcb11
parent 11024 23bf8d787b04
child 11626 0dbfb578bf75