src/HOL/Tools/function_package/mutual.ML
changeset 24434 c588ec4cf194
parent 24171 25381ce95316
child 24977 9f98751c9628