src/Tools/permanent_interpretation.ML
changeset 57433 7e55bd4f9b0e
parent 57224 2a7a789ed510
child 59936 b8ffc3dc9e24
equal deleted inserted replaced
57432:78d7fbe9b203 57433:7e55bd4f9b0e