src/HOL/Recdef.thy
changeset 19629 c107e7a79559
parent 19564 d3e2f532459a
child 19770 be5c23ebe1eb