src/Tools/permanent_interpretation.ML
changeset 59527 edaabc1ab1ed
parent 57224 2a7a789ed510
child 59936 b8ffc3dc9e24