src/Pure/General/secure.ML
changeset 43328 10d731b06ed7
parent 42818 128cc195ced3
child 44200 ce0112e26b3b
equal deleted inserted replaced
43327:c835416237b3 43328:10d731b06ed7