src/HOL/Tools/function_package/mutual.ML
changeset 24761 d762ab297a07
parent 24171 25381ce95316
child 24977 9f98751c9628
equal deleted inserted replaced
24760:3f9aa1e13d16 24761:d762ab297a07