src/Pure/General/secure.ML
changeset 39314 aecb239a2bbc
parent 38799 712cb964d113
child 40748 591b6778d076
equal deleted inserted replaced
39313:41ce0b56d858 39314:aecb239a2bbc