src/HOL/Tools/Nitpick/nitpick_commands.ML
changeset 73616 b0ea03e837b1
parent 69593 3dda49e08b9d
child 74508 3315c551fe6e
equal deleted inserted replaced
73615:e768759ce6c5 73616:b0ea03e837b1