src/HOL/blastdata.ML
changeset 21180 f27f12bcafb8
parent 21009 0eae3fb48936
equal deleted inserted replaced
21179:99f546731724 21180:f27f12bcafb8