src/HOL/Tools/Function/mutual.ML
changeset 33448 7f716a975ada
parent 33393 2240b0e7fa10
child 33643 b275f26a638b
equal deleted inserted replaced
33439:f5d95787224f 33448:7f716a975ada