src/HOL/Tools/Nitpick/nitpick_commands.ML
changeset 82845 d4da7d857bb7
parent 80910 406a85a25189
equal deleted inserted replaced
82844:ebfb0e011c95 82845:d4da7d857bb7