src/HOL/Tools/Nitpick/nitpick.ML
changeset 76219 cf7db6353322
parent 74844 90242c744a1a
child 76501 7956b822f239
equal deleted inserted replaced
76218:728f38b016c0 76219:cf7db6353322