src/HOL/Tools/functor.ML
changeset 81336 40af19b10f8a
parent 80634 a90ab1ea6458
child 81513 d11ed1bf0ad2