src/HOL/Tools/record_package.ML
changeset 27697 bcf941cc3324
parent 27691 ce171cbd4b93
child 28370 37f56e6e702d
equal deleted inserted replaced
27696:15b65db66751 27697:bcf941cc3324