src/HOL/Tools/functor.ML
changeset 81089 8042869c2072
parent 80634 a90ab1ea6458
child 81513 d11ed1bf0ad2
equal deleted inserted replaced
81019:dd59daa3c37a 81089:8042869c2072