src/HOL/ex/Recdef.ML
changeset 4897 be11be0b6ea1
parent 4686 74a12e86b20b
child 5069 3ea049f7979d