src/HOL/Tools/Nitpick/nitpick_commands.ML
changeset 72471 aca85e8d873d
parent 69593 3dda49e08b9d
child 74508 3315c551fe6e
equal deleted inserted replaced
72470:e2e9ef9aa2df 72471:aca85e8d873d