src/HOL/Tools/Function/function_core.ML
changeset 33448 7f716a975ada
parent 33350 b2b78c5ef771
child 33643 b275f26a638b
equal deleted inserted replaced
33439:f5d95787224f 33448:7f716a975ada