src/HOL/thy_data.ML
changeset 4815 b8a32ef742d9
parent 4808 995bc5bd8319
child 4876 1c502a82bcde