src/HOL/Tools/recdef_package.ML
changeset 8942 6aad5381ba83
parent 8734 b456aba346a6
child 9640 8c6cf4f01644
equal deleted inserted replaced
8941:df06883c1dcf 8942:6aad5381ba83