src/HOL/Tools/Nitpick/nitpick_scope.ML
changeset 75397 e852c776a455
parent 72195 16f2288b30cf
child 79799 2746dfc9ceae
equal deleted inserted replaced
75396:45641af13418 75397:e852c776a455