src/Tools/Argo/argo_thy.ML
changeset 80370 119baa9f8cd0
parent 72966 f931a2a68ab8
equal deleted inserted replaced
80369:8c8a2c483fc7 80370:119baa9f8cd0