src/HOL/Tools/Nitpick/nitpick.ML
changeset 80987 e7a926b5b5be
parent 80910 406a85a25189
child 81729 560a069a537f
equal deleted inserted replaced
80986:6e3e1e4a804d 80987:e7a926b5b5be