src/Pure/General/secure.ML
changeset 23596 f8381a95c49c
parent 22567 1565d476a9e2
child 23922 707639e9497d
equal deleted inserted replaced
23595:7ca68a2c8575 23596:f8381a95c49c