src/Pure/ML-Systems/ml_name_space.ML
changeset 58103 c23bdb4ed2f6
parent 56275 600f432ab556
child 59127 723b11f8ffbf
equal deleted inserted replaced
58102:73f46283c247 58103:c23bdb4ed2f6