src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 82845 d4da7d857bb7
parent 80874 9af593e9e454
equal deleted inserted replaced
82844:ebfb0e011c95 82845:d4da7d857bb7