src/HOL/Tools/Nitpick/nitpick_scope.ML
changeset 33982 1ae222745c4a
parent 33957 e9afca2118d4
child 34121 5e831d805118
equal deleted inserted replaced
33981:ca1621556a14 33982:1ae222745c4a
     1 (*  Title:      HOL/Nitpick/Tools/nitpick_scope.ML
     1 (*  Title:      HOL/Tools/Nitpick/nitpick_scope.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2008, 2009
     3     Copyright   2008, 2009
     4 
     4 
     5 Scope enumerator for Nitpick.
     5 Scope enumerator for Nitpick.
     6 *)
     6 *)