src/HOL/Tools/recdef_package.ML
changeset 19402 742b7934ccfc
parent 18891 9923269dcf06
child 19564 d3e2f532459a