src/HOL/Tools/Function/function_context_tree.ML
changeset 59556 aa2deef7cf47
parent 58816 aab139c0003f
child 59580 cbc38731d42f
equal deleted inserted replaced
59555:05573e5504a9 59556:aa2deef7cf47