src/HOL/thy_data.ML
changeset 4932 c90411dde8e8
parent 4876 1c502a82bcde
child 5001 9de7fda0a6df