src/HOL/Tools/recdef_package.ML
changeset 14754 a080eeeaec14
parent 14241 dfae7eb2830c
child 14981 e73f8140af78
equal deleted inserted replaced
14753:f40b45db8cf0 14754:a080eeeaec14