src/HOL/Tools/functor.ML
changeset 80642 318b1b75a4b8
parent 80634 a90ab1ea6458
child 81513 d11ed1bf0ad2