src/HOL/Tools/functor.ML
changeset 63011 301e631666a0
parent 61841 4d3527b94f2a
child 63120 629a4c5e953e