src/Pure/Tools/find_consts.ML
changeset 78823 893049a842b5
parent 74555 3ba399ecdfaf
child 80873 e71cb37c7395
equal deleted inserted replaced
78822:09b5113e5c9d 78823:893049a842b5