src/HOL/Tools/record_package.ML
changeset 19402 742b7934ccfc
parent 19343 91c348f05f1a
child 19748 5d05d091eecb
equal deleted inserted replaced
19401:259e2bbba43c 19402:742b7934ccfc