src/HOL/blastdata.ML
changeset 12770 bdd17e7b5bd9
parent 11753 02b257ef0ee2
child 13550 5a176b8dda84
equal deleted inserted replaced
12769:0f70bfe510ee 12770:bdd17e7b5bd9