src/HOL/Tools/functor.ML
changeset 61448 25e40e78f6d4
parent 60488 fa31b5d36beb
child 61841 4d3527b94f2a