src/Pure/zterm.ML
changeset 80443 ab0dd21dd0ca
parent 80294 eec06d39e5fa
child 80560 960b866b1117
equal deleted inserted replaced
80442:7b70c5bb2807 80443:ab0dd21dd0ca