src/HOL/Tools/recdef_package.ML
changeset 19459 2041d472fc17
parent 18891 9923269dcf06
child 19564 d3e2f532459a