src/HOL/Tools/recdef.ML
changeset 47213 eb5f812d15e2
parent 47067 4ef29b0c568f
child 47815 43f677b3ae91